Qiit.conTy

-- INDUCTION-INDUCTION: contexts and types over them, mutually
-- (Foundation's Con/Ty worked example). Ty is a sort INDEXED BY AN
-- ELEMENT OF ANOTHER SORT of the same signature.

data
  Con : U
  Ty : El Con → U
  nil : El Con
  ext : (gamma : El Con) → El (Ty gamma) → El Con
  unit : (gamma : El Con) → El (Ty gamma)
  arr : (gamma : El Con) → El (Ty gamma) → El (Ty gamma) → El (Ty gamma)

-- a context: nil ▷ unit ▷ (unit → unit)
g1 : Con using (Qiit.conTy.Con.unfold)
g1 = ext nil (unit nil)

g2 : Con using (Qiit.conTy.Con.unfold)
g2 = ext g1 (arr g1 (unit g1) (unit g1))

-- mutual elimination: the LENGTH of a context and the SIZE of a type,
-- one elimination problem (both motives, all four methods)
clen : Con → ℕ using (Qiit.conTy.Con.unfold)
clen =
  λg. ConElim (λw. ℕ) (λg w. ℕ) Z (λg ihg A ihA. S ihg) (λg ihg. S Z) (λg ihg A ihA B ihB. S ihA) g

clenG2 : clen g2 ≡ 2
  using (Qiit.conTy.ConElim.eq,
    Qiit.conTy.arr.eq,
    Qiit.conTy.clen.eq,
    Qiit.conTy.ext.eq,
    Qiit.conTy.g1.eq,
    Qiit.conTy.g2.eq,
    Qiit.conTy.nil.eq,
    Qiit.conTy.unit.eq)
clenG2 = ⋆

-- the same elimination problem read at the Ty motive: type size
tsize : (g : Con) → Ty g → ℕ using (Qiit.conTy.Con.unfold, Qiit.conTy.Ty.unfold)
tsize =
  λg t. TyElim
    λw. ℕ
    λg w. ℕ
    Z
    λg ihg A ihA. S ihg
    λg ihg. S Z
    λg ihg A ihA B ihB. S ihA
    g
    t

tsizeArr : tsize g1 (arr g1 (unit g1) (unit g1)) ≡ 2
  using (Qiit.conTy.Con.unfold,
    Qiit.conTy.Ty.unfold,
    Qiit.conTy.TyElim.eq,
    Qiit.conTy.arr.eq,
    Qiit.conTy.ext.eq,
    Qiit.conTy.g1.eq,
    Qiit.conTy.nil.eq,
    Qiit.conTy.tsize.eq,
    Qiit.conTy.unit.eq)
tsizeArr = ⋆