TT in TT using only induction-induction

SetoidTTinTT.agda

{-# OPTIONS --without-K #-}

-- version 1, conversion is indexed over conversion
module IndexedConv where

  data Con  : Set
  data Ty   : Con → Set
  data Sub  : Con → Con → Set
  data Tm   : ∀ Γ → Ty Γ → Set
  data Con~ : Con → Con → Set
  data Ty~  : ∀ {Γ₀ Γ₁} → Con~ Γ₀ Γ₁ → Ty Γ₀ → Ty Γ₁ → Set
  data Sub~ : ∀ {Γ₀ Γ₁ Δ₀ Δ₁} → Con~ Γ₀ Γ₁ → Con~ Δ₀ Δ₁ → Sub Γ₀ Δ₀ → Sub Γ₁ Δ₁ → Set
  data Tm~  : ∀ {Γ₀ Γ₁ A₀ A₁}(Γ₂ : Con~ Γ₀ Γ₁) → Ty~ Γ₂ A₀ A₁ → Tm Γ₀ A₀ → Tm Γ₁ A₁ → Set

  variable
    Γ Δ Γ₀ Γ₁ Δ₀ Δ₁ θ θ₀ θ₁ : Con
    A B C A₀ A₁ B₀ B₁       : Ty _
    t u v t₀ t₁ u₀ u₁       : Tm _ _
    σ δ ν σ₀ σ₁ δ₀ δ₁ ν₀ ν₁ : Sub _ _
    Γ₂                      : Con~ Γ₀ Γ₁
    Δ₂                      : Con~ Δ₀ Δ₁
    θ₂                      : Con~ θ₀ θ₁
    A₂                      : Ty~ _ A₀ A₁
    B₂                      : Ty~ _ B₀ B₁

  infixl 4 _,_
  infixr 5 _∘_
  infix 5 _[_]

  data Con where
    ∙   : Con
    _,_ : ∀ Γ → Ty Γ → Con

  data Ty where
    coe  : Con~ Γ₀ Γ₁ → Ty Γ₀ → Ty Γ₁

    ------------------------------------------------------------
    _[_] : Ty Δ → Sub Γ Δ → Ty Γ
    U    : Ty Γ
    Π    : (A : Ty Γ) → Ty (Γ , A) → Ty Γ
    El   : Tm Γ U → Ty Γ

  data Sub where
    coe : Con~ Γ₀ Γ₁ → Con~ Δ₀ Δ₁ → Sub Γ₀ Δ₀ → Sub Γ₁ Δ₁

    ------------------------------------------------------------
    id  : Sub Γ Γ
    _∘_ : Sub Δ θ → Sub Γ Δ → Sub Γ θ
    ε   : Sub Γ ∙
    p   : Sub (Γ , A) Γ
    _,_ : (σ : Sub Γ Δ) → Tm Γ (A [ σ ]) → Sub Γ (Δ , A)

  data Tm where
    coe  : ∀ Γ₂ → Ty~ Γ₂ A₀ A₁ → Tm Γ₀ A₀ → Tm Γ₁ A₁

    ------------------------------------------------------------
    _[_] : Tm Δ A → (σ : Sub Γ Δ) → Tm Γ (A [ σ ])
    q    : Tm (Γ , A) (A [ p ])
    lam  : Tm (Γ , A) B → Tm Γ (Π A B)
    app  : Tm Γ (Π A B) → Tm (Γ , A) B

  data Con~ where
    rfl : Con~ Γ Γ
    sym : Con~ Γ Δ → Con~ Δ Γ
    trs : Con~ Γ Δ → Con~ Δ θ → Con~ Γ θ

    ------------------------------------------------------------
    ∙   : Con~ ∙ ∙
    _,_ : ∀ Γ₂ → Ty~ Γ₂ A₀ A₁ → Con~ (Γ₀ , A₀) (Γ₁ , A₁)

  data Ty~ where
    rfl  : Ty~ rfl A A
    sym  : ∀ {Γ₀₁} → Ty~ Γ₀₁ A B → Ty~ (sym Γ₀₁) B A
    trs  : ∀ {Γ₀₁ Γ₁₂} → Ty~ Γ₀₁ A B → Ty~ Γ₁₂ B C → Ty~ (trs Γ₀₁ Γ₁₂) A C
    coh  : ∀ Γ₂ A → Ty~ {Γ₀}{Γ₁} Γ₂ A (coe Γ₂ A)
    reix : ∀ {Γ₂'} → Ty~ Γ₂ A₀ A₁ → Ty~ Γ₂' A₀ A₁

    ------------------------------------------------------------
    _[_] : Ty~ Δ₂ A₀ A₁ → Sub~ Γ₂ Δ₂ σ₀ σ₁ → Ty~ Γ₂ (A₀ [ σ₀ ]) (A₁ [ σ₁ ])
    U    : Ty~ Γ₂ U U
    Π    : (A₂ : Ty~ Γ₂ A₀ A₁) → Ty~ (Γ₂ , A₂) B₀ B₁ → Ty~ Γ₂ (Π A₀ B₀) (Π A₁ B₁)
    El   : Tm~ Γ₂ U t₀ t₁ → Ty~ Γ₂ (El t₀) (El t₁)

    ------------------------------------------------------------
    [id] : Ty~ rfl (A [ id ]) A
    [∘]  : Ty~ rfl (A [ σ ∘ δ ]) (A [ σ ] [ δ ])
    U[]  : Ty~ rfl (U [ σ ]) U
    Π[]  : Ty~ rfl (Π A B [ σ ]) (Π (A [ σ ]) (B [ σ ∘ p , coe (sym rfl) (sym [∘]) q ]))
    El[] : Ty~ rfl (El t [ σ ]) (El (coe rfl U[] (t [ σ ])))

  data Sub~ where
    rfl  : Sub~ rfl rfl σ σ
    sym  : ∀ {Γ₀₁ Δ₀₁} → Sub~ Γ₀₁ Δ₀₁ σ δ → Sub~ (sym Γ₀₁) (sym Δ₀₁) δ σ
    trs  : ∀ {Γ₀₁ Δ₀₁ Γ₁₂ Δ₁₂} → Sub~ Γ₀₁ Δ₀₁ σ δ → Sub~ Γ₁₂ Δ₁₂ δ ν → Sub~ (trs Γ₀₁ Γ₁₂) (trs Δ₀₁ Δ₁₂) σ ν
    coh  : ∀ Γ₂ Δ₂ σ → Sub~ {Γ₀}{Γ₁} {Δ₀}{Δ₁} Γ₂ Δ₂ σ (coe Γ₂ Δ₂ σ)
    reix : ∀ {Γ₂' Δ₂'} → Sub~ Γ₂ Δ₂ σ₀ σ₁ → Sub~ Γ₂' Δ₂' σ₀ σ₁

    ------------------------------------------------------------
    id  : Sub~ Γ₂ Γ₂ id id
    _∘_ : Sub~ Δ₂ θ₂ σ₀ σ₁ → Sub~ Γ₂ Δ₂ δ₀ δ₁ → Sub~ Γ₂ θ₂ (σ₀ ∘ δ₀) (σ₁ ∘ δ₁)
    ε   : Sub~ Γ₂ ∙ ε ε
    p   : Sub~ (Γ₂ , A₂) Γ₂ p p
    _,_ : (σ₂ : Sub~ Γ₂ Δ₂ σ₀ σ₁) → Tm~ Γ₂ (A₂ [ σ₂ ]) t₀ t₁ → Sub~ Γ₂ (Δ₂ , A₂) (σ₀ , t₀) (σ₁ , t₁)

    ------------------------------------------------------------
    εη  : Sub~ rfl rfl σ ε
    idl : Sub~ rfl rfl (id ∘ σ) σ
    idr : Sub~ rfl rfl (σ ∘ id) σ
    ass : Sub~ rfl rfl (σ ∘ δ ∘ ν) ((σ ∘ δ) ∘ ν)
    p∘  : Sub~ rfl rfl (p ∘ (σ , t)) σ
    pq  : Sub~ rfl rfl (p , q) (id {Γ , A})
    ,∘  : Sub~ rfl rfl ((σ , t) ∘ δ) (σ ∘ δ , coe (sym rfl) (sym [∘]) (t [ δ ]))

  data Tm~ where
    rfl  : Tm~ rfl rfl t t
    sym  : ∀ {Γ₀₁ A₀₁} → Tm~ Γ₀₁ A₀₁ t u → Tm~ (sym Γ₀₁) (sym A₀₁) u t
    trs  : ∀ {Γ₀₁ A₀₁ Γ₁₂ A₁₂} → Tm~ Γ₀₁ A₀₁ t u → Tm~ Γ₁₂ A₁₂ u v → Tm~ (trs Γ₀₁ Γ₁₂) (trs A₀₁ A₁₂) t v
    coh  : ∀ Γ₂ A₂ t → Tm~ {Γ₀}{Γ₁} {A₀}{A₁} Γ₂ A₂ t (coe Γ₂ A₂ t)
    reix : ∀ {Γ₂' A₂'} → Tm~ Γ₂ A₂ t₀ t₁ → Tm~ Γ₂' A₂' t₀ t₁

    ------------------------------------------------------------
    _[_] : Tm~ Δ₂ A₂ t₀ t₁ → (σ₂ : Sub~ Γ₂ Δ₂ σ₀ σ₁) → Tm~ Γ₂ (A₂ [ σ₂ ]) (t₀ [ σ₀ ]) (t₁ [ σ₁ ])
    q    : Tm~ (Γ₂ , A₂) (A₂ [ p {A₂ = A₂} ]) q q
    lam  : Tm~ (Γ₂ , A₂) B₂ t₀ t₁ → Tm~ Γ₂ (Π A₂ B₂) (lam t₀) (lam t₁)
    app  : Tm~ Γ₂ (Π A₂ B₂) t₀ t₁ → Tm~ (Γ₂ , A₂) B₂ (app t₀) (app t₁)

    ------------------------------------------------------------
    q[]   : Tm~ (trs (sym rfl) rfl) (trs (sym [∘]) (rfl [ p∘ ])) (q [ σ , t ]) t
    lam[] : Tm~ rfl Π[] (lam t [ σ ]) (lam (t [ σ ∘ p , coe (sym rfl) (sym [∘]) q ]))
    Πβ    : Tm~ rfl rfl (app (lam t)) t
    Πη    : Tm~ rfl rfl (lam (app t)) t
    
-- version 2: conversion is "John Major" style, it stands for a bundle of conversions in the base type and the dependent type
module JMConv where

  data Con  : Set
  data Ty   : Con → Set
  data Sub  : Con → Con → Set
  data Tm   : ∀ Γ → Ty Γ → Set
  data Con~ : Con → Con → Set
  data Ty~  : ∀ {Γ₀ Γ₁} → Ty Γ₀ → Ty Γ₁ → Set
  data Sub~ : ∀ {Γ₀ Γ₁ Δ₀ Δ₁} → Sub Γ₀ Δ₀ → Sub Γ₁ Δ₁ → Set
  data Tm~  : ∀ {Γ₀ Γ₁ A₀ A₁} → Tm Γ₀ A₀ → Tm Γ₁ A₁ → Set

  variable
    Γ Δ Γ₀ Γ₁ Δ₀ Δ₁ θ θ₀ θ₁ : Con
    A B C A₀ A₁ B₀ B₁       : Ty _
    t u v t₀ t₁ u₀ u₁       : Tm _ _
    σ δ ν σ₀ σ₁ δ₀ δ₁ ν₀ ν₁ : Sub _ _
    Γ₂                      : Con~ Γ₀ Γ₁
    Δ₂                      : Con~ Δ₀ Δ₁
    θ₂                      : Con~ θ₀ θ₁
    A₂                      : Ty~ A₀ A₁
    B₂                      : Ty~ B₀ B₁

  HTy~ : Ty Γ → Ty Γ → Set
  HTy~ = Ty~

  HSub~ : Sub Γ Δ → Sub Γ Δ → Set
  HSub~ = Sub~

  HTm~ : Tm Γ A → Tm Γ A → Set
  HTm~ = Tm~

  infixl 4 _,_
  infixr 5 _∘_
  infix 5 _[_]

  data Con where
    ∙   : Con
    _,_ : ∀ Γ → Ty Γ → Con

  data Ty where
    coe  : Con~ Γ₀ Γ₁ → Ty Γ₀ → Ty Γ₁

    ------------------------------------------------------------
    _[_] : Ty Δ → Sub Γ Δ → Ty Γ
    U    : Ty Γ
    Π    : (A : Ty Γ) → Ty (Γ , A) → Ty Γ
    El   : Tm Γ U → Ty Γ

  data Sub where
    coe : Con~ Γ₀ Γ₁ → Con~ Δ₀ Δ₁ → Sub Γ₀ Δ₀ → Sub Γ₁ Δ₁

    ------------------------------------------------------------
    id  : Sub Γ Γ
    _∘_ : Sub Δ θ → Sub Γ Δ → Sub Γ θ
    ε   : Sub Γ ∙
    p   : Sub (Γ , A) Γ
    _,_ : (σ : Sub Γ Δ) → Tm Γ (A [ σ ]) → Sub Γ (Δ , A)

  data Tm where
    coe  : Ty~ A₀ A₁ → Tm Γ₀ A₀ → Tm Γ₁ A₁

    ------------------------------------------------------------
    _[_] : Tm Δ A → (σ : Sub Γ Δ) → Tm Γ (A [ σ ])
    q    : Tm (Γ , A) (A [ p ])
    lam  : Tm (Γ , A) B → Tm Γ (Π A B)
    app  : Tm Γ (Π A B) → Tm (Γ , A) B

  data Con~ where
    rfl   : Con~ Γ Γ
    sym   : Con~ Γ Δ → Con~ Δ Γ
    trs   : Con~ Γ Δ → Con~ Δ θ → Con~ Γ θ
    Ty~₀  : Ty~ {Γ₀}{Γ₁} A B → Con~ Γ₀ Γ₁
    Sub~₀ : Sub~ {Γ₀}{Γ₁}{Δ₀}{Δ₁} σ₀ σ₁ → Con~ Γ₀ Γ₁
    Sub~₁ : Sub~ {Γ₀}{Γ₁}{Δ₀}{Δ₁} σ₀ σ₁ → Con~ Δ₀ Δ₁

    ------------------------------------------------------------
    ∙   : Con~ ∙ ∙
    _,_ : Ty~ A₀ A₁ → Con~ (Γ₀ , A₀) (Γ₁ , A₁)

  data Ty~ where
    rfl  : Ty~ A A
    sym  : Ty~ A B → Ty~ B A
    trs  : Ty~ A B → Ty~ B C → Ty~ A C
    coh  : ∀ (Γ₂ : Con~ Γ₀ Γ₁) A → Ty~ A (coe Γ₂ A)
    Tm~₁ : Tm~ {Γ₀}{Γ₁}{A₀}{A₁} t₀ t₁ → Ty~ A₀ A₁

    ------------------------------------------------------------
    _[_] : Ty~ A₀ A₁ → Sub~ σ₀ σ₁ → Ty~ (A₀ [ σ₀ ]) (A₁ [ σ₁ ])
    U    : Con~ Γ₀ Γ₁ → Ty~ (U{Γ₀}) (U{Γ₁})
    Π    : (A₂ : Ty~ A₀ A₁) → Ty~ B₀ B₁ → Ty~ (Π A₀ B₀) (Π A₁ B₁)
    El   : Tm~ t₀ t₁ → Ty~ (El t₀) (El t₁)

    ------------------------------------------------------------
    [id] : HTy~ (A [ id ]) A
    [∘]  : HTy~ (A [ σ ∘ δ ]) (A [ σ ] [ δ ])
    U[]  : HTy~ (U [ σ ]) U
    Π[]  : HTy~ (Π A B [ σ ]) (Π (A [ σ ]) (B [ σ ∘ p , coe (sym [∘]) Tm.q ]))
    El[] : HTy~ (El t [ σ ]) (El (coe U[] (t [ σ ])))

  data Sub~ where
    rfl  : Sub~ σ σ
    sym  : Sub~ σ δ → Sub~ δ σ
    trs  : Sub~ σ δ → Sub~ δ ν → Sub~ σ ν
    coh  : ∀ Γ₂ Δ₂ σ → Sub~ {Γ₀}{Γ₁} {Δ₀}{Δ₁} σ (coe Γ₂ Δ₂ σ)

    id  : Con~ Γ₀ Γ₁ → Sub~ (id {Γ₀}) (id {Γ₁})
    _∘_ : Sub~ σ₀ σ₁ → Sub~ δ₀ δ₁ → Sub~ (σ₀ ∘ δ₀) (σ₁ ∘ δ₁)
    ε   : Con~ Γ₀ Γ₁ → Sub~ (ε{Γ₀}) (ε{Γ₁})
    p   : Ty~ A₀ A₁ → Sub~ (p {Γ₀}{A₀}) (p {Γ₁}{A₁})
    _,_ : (σ₂ : Sub~ σ₀ σ₁) → Tm~ t₀ t₁ → Sub~ (σ₀ , t₀) (σ₁ , t₁)

    ------------------------------------------------------------
    εη  : HSub~ σ ε
    idl : HSub~ (id ∘ σ) σ
    idr : HSub~ (σ ∘ id) σ
    ass : HSub~ (σ ∘ δ ∘ ν) ((σ ∘ δ) ∘ ν)
    p∘  : HSub~ (p ∘ (σ , t)) σ
    pq  : HSub~ (p , q) (id {Γ , A})
    ,∘  : HSub~ ((σ , t) ∘ δ) (σ ∘ δ , coe (sym [∘]) (t [ δ ]))

  data Tm~ where
    rfl  : Tm~ t t
    sym  : Tm~ t u → Tm~ u t
    trs  : Tm~ t u → Tm~ u v → Tm~ t v
    coh  : ∀ A₂ t → Tm~ {Γ₀}{Γ₁} {A₀}{A₁} t (coe A₂ t)

    ------------------------------------------------------------
    _[_] : Tm~ t₀ t₁ → (σ₂ : Sub~ σ₀ σ₁) → Tm~ (t₀ [ σ₀ ]) (t₁ [ σ₁ ])
    q    : Ty~ A₀ A₁ → Tm~ (q{Γ₀}{A₀}) (q{Γ₁}{A₁})
    lam  : Tm~ t₀ t₁ → Tm~ (lam t₀) (lam t₁)
    app  : Tm~ t₀ t₁ → Tm~ (app t₀) (app t₁)

    ------------------------------------------------------------
    q[]   : Tm~ (q [ σ , t ]) t
    lam[] : Tm~ (lam t [ σ ]) (lam (t [ σ ∘ p , coe (sym [∘]) q ]))
    Πβ    : HTm~ (app (lam t)) t
    Πη    : HTm~ (lam (app t)) t