qiitConTy

-- 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)
def g1 : El Con ≔ ext nil (unit nil)
def g2 : El Con ≔ 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)
def clen : El Con → ℕ ≔
  λ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

def clenG2 : clen g2 ≡ S (S Z) ∈ _ ≔ ⋆

-- the same elimination problem read at the Ty motive: type size
def tsize : (g : El Con) → El (Ty g) → ℕ ≔
  λ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

def tsizeArr : tsize g1 (arr g1 (unit g1) (unit g1)) ≡ S (S Z) ∈ _ ≔ ⋆