open import Definition.Typed.EqualityRelation
open import Definition.Typed.Restrictions
open import Graded.Modality
module Definition.LogicalRelation.Substitution
{a} {M : Set a}
{π : Modality M}
(R : Type-restrictions π)
β¦ eqrel : EqRelSet R β¦
where
open EqRelSet eqrel
open Type-restrictions R
open import Definition.LogicalRelation R
open import Definition.LogicalRelation.Hidden R
open import Definition.LogicalRelation.Properties R
open import Definition.Typed R
open import Definition.Typed.Properties R
open import Definition.Typed.Weakening R as TW using (_β·_β_)
open import Definition.Untyped M
open import Definition.Untyped.Neutral M
open import Definition.Untyped.Properties M
open import Tools.Fin
open import Tools.Function
open import Tools.Level
open import Tools.Nat using (Nat)
open import Tools.Product as Ξ£
import Tools.PropositionalEquality as PE
open import Tools.Reasoning.PropositionalEquality
open import Tools.Unit
private variable
m n : Nat
Ξ Ξ Ξ : Con Term _
A Aβ Aβ B Bβ Bβ C Cβ Cβ D E t tβ tβ u uβ uβ v vβ vβ w : Term _
Ο Οβ Οβ Οβ : Subst _ _
Ο : Wk _ _
l lβ² lβ³ lβ΄ : TypeLevel
opaque mutual
infix 4 β©α΅_
β©α΅_ : Con Term n β Set a
β©α΅ Ξ΅ = Lift _ β€
β©α΅ (Ξ β A) = β Ξ» l β Ξ β©α΅β¨ l β© A
infix 4 _β©α΅β¨_β©_
_β©α΅β¨_β©_ : Con Term n β TypeLevel β Term n β Set a
Ξ β©α΅β¨ l β© A = Ξ β©α΅β¨ l β© A β‘ A
infix 4 _β©α΅β¨_β©_β‘_
_β©α΅β¨_β©_β‘_ : Con Term n β TypeLevel β Term n β Term n β Set a
_β©α΅β¨_β©_β‘_ {n} Ξ l A B =
β©α΅ Ξ Γ
(β {m Ξ} {Οβ Οβ : Subst m n} β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©β¨ l β© A [ Οβ ] β‘ B [ Οβ ])
infix 4 _β©Λ’_β‘_β·_
_β©Λ’_β‘_β·_ : Con Term m β Subst m n β Subst m n β Con Term n β Set a
Ξ β©Λ’ _ β‘ _ β· Ξ΅ = β’ Ξ
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β A =
(β Ξ» l β
(Ξ β©α΅β¨ l β© A) Γ
Ξ β©β¨ l β© head Οβ β‘ head Οβ β· A [ tail Οβ ]) Γ
Ξ β©Λ’ tail Οβ β‘ tail Οβ β· Ξ
opaque
infix 4 _β©Λ’_β·_
_β©Λ’_β·_ : Con Term m β Subst m n β Con Term n β Set a
Ξ β©Λ’ Ο β· Ξ = Ξ β©Λ’ Ο β‘ Ο β· Ξ
opaque
infix 4 _β©α΅β¨_β©_β‘_β·_
_β©α΅β¨_β©_β‘_β·_ :
Con Term n β TypeLevel β Term n β Term n β Term n β Set a
_β©α΅β¨_β©_β‘_β·_ {n} Ξ l t u A =
Ξ β©α΅β¨ l β© A Γ
(β {m Ξ} {Οβ Οβ : Subst m n} β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β Ξ β©β¨ l β© t [ Οβ ] β‘ u [ Οβ ] β· A [ Οβ ])
opaque
infix 4 _β©α΅β¨_β©_β·_
_β©α΅β¨_β©_β·_ : Con Term n β TypeLevel β Term n β Term n β Set a
Ξ β©α΅β¨ l β© t β· A = Ξ β©α΅β¨ l β© t β‘ t β· A
opaque
unfolding β©α΅_
β©α΅Ξ΅β : β©α΅ Ξ΅ β β€
β©α΅Ξ΅β = _
opaque
unfolding β©α΅_
β©α΅ββ : β©α΅ Ξ β A β β Ξ» l β Ξ β©α΅β¨ l β© A
β©α΅ββ = idβ
opaque
unfolding _β©α΅β¨_β©_
β©α΅ββ©α΅β‘ : (Ξ β©α΅β¨ l β© A) β Ξ β©α΅β¨ l β© A β‘ A
β©α΅ββ©α΅β‘ = idβ
opaque
unfolding _β©α΅β¨_β©_ _β©α΅β¨_β©_β‘_
β©α΅β :
Ξ β©α΅β¨ l β© A β
(β©α΅ Ξ Γ
(β {m Ξ} {Οβ Οβ : Subst m n} β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β Ξ β©β¨ l β© A [ Οβ ] β‘ A [ Οβ ]))
β©α΅β = idβ
opaque
unfolding _β©α΅β¨_β©_β‘_
β©α΅β‘β :
Ξ β©α΅β¨ l β© A β‘ B β
(β©α΅ Ξ Γ
(β {m Ξ} {Οβ Οβ : Subst m n} β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β Ξ β©β¨ l β© A [ Οβ ] β‘ B [ Οβ ]))
β©α΅β‘β = idβ
opaque
unfolding _β©α΅β¨_β©_β·_
β©α΅β·ββ©α΅β‘β· : Ξ β©α΅β¨ l β© t β· A β Ξ β©α΅β¨ l β© t β‘ t β· A
β©α΅β·ββ©α΅β‘β· = idβ
opaque
unfolding _β©α΅β¨_β©_β·_ _β©α΅β¨_β©_β‘_β·_
β©α΅β·β :
Ξ β©α΅β¨ l β© t β· A β
(Ξ β©α΅β¨ l β© A Γ
(β {m Ξ} {Οβ Οβ : Subst m n} β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©β¨ l β© t [ Οβ ] β‘ t [ Οβ ] β· A [ Οβ ]))
β©α΅β·β = idβ
opaque
unfolding _β©α΅β¨_β©_β‘_β·_
β©α΅β‘β·β :
Ξ β©α΅β¨ l β© t β‘ u β· A β
(Ξ β©α΅β¨ l β© A Γ
(β {m Ξ} {Οβ Οβ : Subst m n} β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©β¨ l β© t [ Οβ ] β‘ u [ Οβ ] β· A [ Οβ ]))
β©α΅β‘β·β = idβ
opaque
unfolding _β©Λ’_β‘_β·_
β©Λ’β‘β·Ξ΅β : Ξ β©Λ’ Οβ β‘ Οβ β· Ξ΅ β β’ Ξ
β©Λ’β‘β·Ξ΅β = idβ
opaque
unfolding _β©Λ’_β‘_β·_
β©Λ’β‘β·ββ :
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β A β
((β Ξ» l β
(Ξ β©α΅β¨ l β© A) Γ
Ξ β©β¨ l β© head Οβ β‘ head Οβ β· A [ tail Οβ ]) Γ
Ξ β©Λ’ tail Οβ β‘ tail Οβ β· Ξ)
β©Λ’β‘β·ββ = idβ
opaque
unfolding _β©Λ’_β·_
β©Λ’β·ββ©Λ’β‘β· : Ξ β©Λ’ Ο β· Ξ β Ξ β©Λ’ Ο β‘ Ο β· Ξ
β©Λ’β·ββ©Λ’β‘β· = idβ
opaque
β©Λ’β·Ξ΅β : Ξ β©Λ’ Ο β· Ξ΅ β β’ Ξ
β©Λ’β·Ξ΅β {Ξ} {Ο} =
Ξ β©Λ’ Ο β· Ξ΅ ββ¨ β©Λ’β·ββ©Λ’β‘β· β©
Ξ β©Λ’ Ο β‘ Ο β· Ξ΅ ββ¨ β©Λ’β‘β·Ξ΅β β©
β’ Ξ β‘β
opaque
β©Λ’β·ββ :
Ξ β©Λ’ Ο β· Ξ β A β
((β Ξ» l β (Ξ β©α΅β¨ l β© A) Γ Ξ β©β¨ l β© head Ο β· A [ tail Ο ]) Γ
Ξ β©Λ’ tail Ο β· Ξ)
β©Λ’β·ββ {Ξ} {Ο} {Ξ} {A} =
Ξ β©Λ’ Ο β· Ξ β A ββ¨ β©Λ’β·ββ©Λ’β‘β· β©
Ξ β©Λ’ Ο β‘ Ο β· Ξ β A ββ¨ β©Λ’β‘β·ββ β©
(β Ξ» l β
(Ξ β©α΅β¨ l β© A) Γ
Ξ β©β¨ l β© head Ο β‘ head Ο β· A [ tail Ο ]) Γ
Ξ β©Λ’ tail Ο β‘ tail Ο β· Ξ βΛβ¨ (Ξ£-cong-β Ξ» _ β Ξ£-cong-β Ξ» _ β β©β·ββ©β‘β·)
Γ-cong-β
β©Λ’β·ββ©Λ’β‘β· β©
(β Ξ» l β (Ξ β©α΅β¨ l β© A) Γ Ξ β©β¨ l β© head Ο β· A [ tail Ο ]) Γ
Ξ β©Λ’ tail Ο β· Ξ β‘β
opaque
β©α΅-β-intro : Ξ β©α΅β¨ l β© A β β©α΅ Ξ β A
β©α΅-β-intro β©A = β©α΅ββ .projβ (_ , β©A)
opaque
refl-β©Λ’β‘β· :
Ξ β©Λ’ Ο β· Ξ β
Ξ β©Λ’ Ο β‘ Ο β· Ξ
refl-β©Λ’β‘β· = β©Λ’β·ββ©Λ’β‘β· .projβ
opaque
refl-β©α΅β‘ :
Ξ β©α΅β¨ l β© A β
Ξ β©α΅β¨ l β© A β‘ A
refl-β©α΅β‘ = β©α΅ββ©α΅β‘ .projβ
opaque
refl-β©α΅β‘β· :
Ξ β©α΅β¨ l β© t β· A β
Ξ β©α΅β¨ l β© t β‘ t β· A
refl-β©α΅β‘β· = β©α΅β·ββ©α΅β‘β· .projβ
opaque
β©α΅ββ©Λ’β·ββ©[] :
Ξ β©α΅β¨ l β© A β
Ξ β©Λ’ Ο β· Ξ β
Ξ β©β¨ l β© A [ Ο ]
β©α΅ββ©Λ’β·ββ©[] β©A =
β©ββ©β‘ .projβ ββ β©α΅β .projβ β©A .projβ ββ refl-β©Λ’β‘β·
opaque
β©α΅β·ββ©Λ’β·ββ©[]β· :
Ξ β©α΅β¨ l β© t β· A β
Ξ β©Λ’ Ο β· Ξ β
Ξ β©β¨ l β© t [ Ο ] β· A [ Ο ]
β©α΅β·ββ©Λ’β·ββ©[]β· β©t =
β©β·ββ©β‘β· .projβ ββ β©α΅β·β .projβ β©t .projβ ββ refl-β©Λ’β‘β·
opaque
sym-β©Λ’β‘β· :
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ
sym-β©Λ’β‘β· {Ξ = Ξ΅} =
β©Λ’β‘β·Ξ΅β .projβ ββ β©Λ’β‘β·Ξ΅β .projβ
sym-β©Λ’β‘β· {Ξ = _ β _} = Ξ» Οββ‘Οβ β
case β©Λ’β‘β·ββ .projβ Οββ‘Οβ of Ξ»
((l , β©A , Οβββ‘Οββ) , Οβββ‘Οββ) β
case conv-β©β‘β· (β©α΅β .projβ β©A .projβ Οβββ‘Οββ) $
sym-β©β‘β· Οβββ‘Οββ of Ξ»
Οβββ‘Οββ β
β©Λ’β‘β·ββ .projβ ((l , β©A , Οβββ‘Οββ) , sym-β©Λ’β‘β· Οβββ‘Οββ)
opaque
sym-β©α΅β‘ :
Ξ β©α΅β¨ l β© A β‘ B β
Ξ β©α΅β¨ l β© B β‘ A
sym-β©α΅β‘ Aβ‘B =
case β©α΅β‘β .projβ Aβ‘B of Ξ»
(β©Ξ , Aβ‘B) β
β©α΅β‘β .projβ (β©Ξ , sym-β©β‘ ββ Aβ‘B ββ sym-β©Λ’β‘β·)
opaque
sym-β©α΅β‘β· :
Ξ β©α΅β¨ l β© t β‘ u β· A β
Ξ β©α΅β¨ l β© u β‘ t β· A
sym-β©α΅β‘β· tβ‘u =
case β©α΅β‘β·β .projβ tβ‘u of Ξ»
(β©A , tβ‘u) β
β©α΅β‘β·β .projβ
( β©A
, Ξ» Οββ‘Οβ β
conv-β©β‘β· (sym-β©β‘ $ β©α΅β .projβ β©A .projβ Οββ‘Οβ) $
sym-β©β‘β· $ tβ‘u $ sym-β©Λ’β‘β· Οββ‘Οβ)
opaque
trans-β©Λ’β‘ :
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ
trans-β©Λ’β‘ {Ξ = Ξ΅} Οββ‘Οβ _ =
β©Λ’β‘β·Ξ΅β .projβ $ β©Λ’β‘β·Ξ΅β .projβ Οββ‘Οβ
trans-β©Λ’β‘ {Ξ = _ β _} Οββ‘Οβ Οββ‘Οβ =
case β©Λ’β‘β·ββ .projβ Οββ‘Οβ of Ξ»
((l , β©A , Οβββ‘Οββ) , Οβββ‘Οββ) β
case β©Λ’β‘β·ββ .projβ Οββ‘Οβ of Ξ»
((l , β©A , Οβββ‘Οββ) , Οβββ‘Οββ) β
case conv-β©β‘β· (β©α΅β .projβ β©A .projβ $ sym-β©Λ’β‘β· Οβββ‘Οββ) Οβββ‘Οββ of Ξ»
Οβββ‘Οββ β
β©Λ’β‘β·ββ .projβ
( (l , β©A , trans-β©β‘β· Οβββ‘Οββ Οβββ‘Οββ)
, trans-β©Λ’β‘ Οβββ‘Οββ Οβββ‘Οββ
)
opaque
wf-β©α΅-β : β©α΅ Ξ β A β β Ξ» l β Ξ β©α΅β¨ l β© A
wf-β©α΅-β = β©α΅ββ .projβ
opaque
wf-β©α΅ : Ξ β©α΅β¨ l β© A β β©α΅ Ξ
wf-β©α΅ = projβ ββ β©α΅β .projβ
opaque
wf-β-β©α΅ :
Ξ β A β©α΅β¨ l β© B β
β Ξ» lβ² β Ξ β©α΅β¨ lβ² β© A
wf-β-β©α΅ = wf-β©α΅-β ββ wf-β©α΅
opaque
wf-β©α΅β· : Ξ β©α΅β¨ l β© t β· A β Ξ β©α΅β¨ l β© A
wf-β©α΅β· = projβ ββ β©α΅β·β .projβ
opaque
wf-β©Λ’β· : Ξ β©Λ’ Ο β· Ξ β β©α΅ Ξ
wf-β©Λ’β· {Ξ = Ξ΅} = Ξ» _ β β©α΅Ξ΅β .projβ _
wf-β©Λ’β· {Ξ = _ β _} =
β©α΅ββ .projβ ββ Ξ£.map idαΆ projβ ββ projβ ββ β©Λ’β·ββ .projβ
opaque
wf-β©Λ’β‘β· : Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β Ξ β©Λ’ Οβ β· Ξ Γ Ξ β©Λ’ Οβ β· Ξ
wf-β©Λ’β‘β· Οββ‘Οβ =
β©Λ’β·ββ©Λ’β‘β· .projβ (trans-β©Λ’β‘ Οββ‘Οβ (sym-β©Λ’β‘β· Οββ‘Οβ))
, β©Λ’β·ββ©Λ’β‘β· .projβ (trans-β©Λ’β‘ (sym-β©Λ’β‘β· Οββ‘Οβ) Οββ‘Οβ)
opaque
level-β©α΅β‘ :
Ξ β©α΅β¨ l β© A β
Ξ β©α΅β¨ l β© B β
Ξ β©α΅β¨ lβ² β© A β‘ B β
Ξ β©α΅β¨ l β© A β‘ B
level-β©α΅β‘ β©A β©B Aβ‘B =
case β©α΅β‘β .projβ Aβ‘B of Ξ»
(β©Ξ , Aβ‘B) β
β©α΅β‘β .projβ
( β©Ξ
, Ξ» Οββ‘Οβ β
case wf-β©Λ’β‘β· Οββ‘Οβ of Ξ»
(β©Οβ , β©Οβ) β
level-β©β‘ (β©α΅ββ©Λ’β·ββ©[] β©A β©Οβ) (β©α΅ββ©Λ’β·ββ©[] β©B β©Οβ) $
Aβ‘B Οββ‘Οβ
)
opaque
level-β©α΅β‘β· :
Ξ β©α΅β¨ l β© A β
Ξ β©α΅β¨ lβ² β© t β‘ u β· A β
Ξ β©α΅β¨ l β© t β‘ u β· A
level-β©α΅β‘β· β©A tβ‘u =
β©α΅β‘β·β .projβ
( β©A
, Ξ» Οββ‘Οβ β
level-β©β‘β· (β©α΅ββ©Λ’β·ββ©[] β©A $ wf-β©Λ’β‘β· Οββ‘Οβ .projβ) $
β©α΅β‘β·β .projβ tβ‘u .projβ Οββ‘Οβ
)
opaque
level-β©α΅β· :
Ξ β©α΅β¨ l β© A β
Ξ β©α΅β¨ lβ² β© t β· A β
Ξ β©α΅β¨ l β© t β· A
level-β©α΅β· β©A =
β©α΅β·ββ©α΅β‘β· .projβ ββ level-β©α΅β‘β· β©A ββ β©α΅β·ββ©α΅β‘β· .projβ
opaque
trans-β©α΅β‘ :
Ξ β©α΅β¨ l β© A β‘ B β
Ξ β©α΅β¨ l β© B β‘ C β
Ξ β©α΅β¨ l β© A β‘ C
trans-β©α΅β‘ {A} {B} {C} Aβ‘B Bβ‘C =
case β©α΅β‘β .projβ Aβ‘B of Ξ»
(β©Ξ , Aβ‘B) β
case β©α΅β‘β .projβ Bβ‘C of Ξ»
(_ , Bβ‘C) β
β©α΅β‘β .projβ
( β©Ξ
, Ξ» {_ _} {Οβ = Οβ} {Οβ = Οβ} Οββ‘Οβ β
A [ Οβ ] β‘β¨ Aβ‘B $ refl-β©Λ’β‘β· (wf-β©Λ’β‘β· Οββ‘Οβ .projβ) β©β©
B [ Οβ ] β‘β¨ Bβ‘C Οββ‘Οβ β©β©β
C [ Οβ ] β
)
opaque
trans-β©α΅β‘β· :
Ξ β©α΅β¨ lβ² β© t β‘ u β· A β
Ξ β©α΅β¨ l β© u β‘ v β· A β
Ξ β©α΅β¨ l β© t β‘ v β· A
trans-β©α΅β‘β· {t} {u} {v} tβ‘u uβ‘v =
case β©α΅β‘β·β .projβ uβ‘v of Ξ»
(β©A , uβ‘v) β
case β©α΅β‘β·β .projβ $ level-β©α΅β‘β· β©A tβ‘u of Ξ»
(_ , tβ‘u) β
β©α΅β‘β·β .projβ
( β©A
, Ξ» {_ _} {Οβ = Οβ} {Οβ = Οβ} Οββ‘Οβ β
t [ Οβ ] β‘β¨ tβ‘u $ refl-β©Λ’β‘β· (wf-β©Λ’β‘β· Οββ‘Οβ .projβ) β©β©β·
u [ Οβ ] β‘β¨ uβ‘v Οββ‘Οβ β©β©β·β
v [ Οβ ] β
)
opaque
wf-β©α΅β‘ : Ξ β©α΅β¨ l β© A β‘ B β Ξ β©α΅β¨ l β© A Γ Ξ β©α΅β¨ l β© B
wf-β©α΅β‘ Aβ‘B =
β©α΅ββ©α΅β‘ .projβ (trans-β©α΅β‘ Aβ‘B (sym-β©α΅β‘ Aβ‘B))
, β©α΅ββ©α΅β‘ .projβ (trans-β©α΅β‘ (sym-β©α΅β‘ Aβ‘B) Aβ‘B)
opaque
wf-β©α΅β‘β· : Ξ β©α΅β¨ l β© t β‘ u β· A β Ξ β©α΅β¨ l β© t β· A Γ Ξ β©α΅β¨ l β© u β· A
wf-β©α΅β‘β· tβ‘u =
β©α΅β·ββ©α΅β‘β· .projβ (trans-β©α΅β‘β· tβ‘u (sym-β©α΅β‘β· tβ‘u))
, β©α΅β·ββ©α΅β‘β· .projβ (trans-β©α΅β‘β· (sym-β©α΅β‘β· tβ‘u) tβ‘u)
opaque
β©α΅β‘ββ² :
Ξ β©α΅β¨ l β© A β‘ B β
(Ξ β©α΅β¨ l β© A Γ
Ξ β©α΅β¨ l β© B Γ
(β {m Ξ} {Ο : Subst m n} β
Ξ β©Λ’ Ο β· Ξ β
Ξ β©β¨ l β© A [ Ο ] β‘ B [ Ο ]))
β©α΅β‘ββ² {A} {B} =
(Ξ» Aβ‘B β
case wf-β©α΅β‘ Aβ‘B of Ξ»
(β©A , β©B) β
β©A , β©B , Ξ» {_ _ _} β β©α΅β‘β .projβ Aβ‘B .projβ ββ refl-β©Λ’β‘β·)
, (Ξ» (β©A , _ , Aβ‘B) β
β©α΅β‘β .projβ
( wf-β©α΅ β©A
, Ξ» {_ _} {Οβ = Οβ} {Οβ = Οβ} Οββ‘Οβ β
A [ Οβ ] β‘β¨ β©α΅β .projβ β©A .projβ Οββ‘Οβ β©β©
A [ Οβ ] β‘β¨ Aβ‘B $ wf-β©Λ’β‘β· Οββ‘Οβ .projβ β©β©β
B [ Οβ ] β
))
opaque
β©α΅β‘ββ³ :
Ξ β©α΅β¨ l β© A β‘ B β
(Ξ β©α΅β¨ l β© A Γ
Ξ β©α΅β¨ l β© B Γ
(β {m Ξ} {Οβ Οβ : Subst m n} β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©β¨ l β© A [ Οβ ] β‘ B [ Οβ ]))
β©α΅β‘ββ³ =
(Ξ» Aβ‘B β
case wf-β©α΅β‘ Aβ‘B of Ξ»
(β©A , β©B) β
β©A , β©B , Ξ» {_ _ _ _} β β©α΅β‘β .projβ Aβ‘B .projβ)
, (Ξ» (β©A , _ , Aβ‘B) β
β©α΅β‘β .projβ (wf-β©α΅ β©A , Aβ‘B))
opaque
β©α΅β‘β·ββ² :
Ξ β©α΅β¨ l β© t β‘ u β· A β
(Ξ β©α΅β¨ l β© t β· A Γ
Ξ β©α΅β¨ l β© u β· A Γ
(β {m Ξ} {Ο : Subst m n} β
Ξ β©Λ’ Ο β· Ξ β
Ξ β©β¨ l β© t [ Ο ] β‘ u [ Ο ] β· A [ Ο ]))
β©α΅β‘β·ββ² {t} {u} =
(Ξ» tβ‘u β
case wf-β©α΅β‘β· tβ‘u of Ξ»
(β©t , β©u) β
β©t , β©u , Ξ» {_ _ _} β β©α΅β‘β·β .projβ tβ‘u .projβ ββ refl-β©Λ’β‘β·)
, (Ξ» (_ , β©u , tβ‘u) β
β©α΅β‘β·β .projβ
( wf-β©α΅β· β©u
, Ξ» {_ _} {Οβ = Οβ} {Οβ = Οβ} Οββ‘Οβ β
t [ Οβ ] β‘β¨ tβ‘u $ wf-β©Λ’β‘β· Οββ‘Οβ .projβ β©β©β·
u [ Οβ ] β‘β¨ β©α΅β·β .projβ β©u .projβ Οββ‘Οβ β©β©β·β
u [ Οβ ] β
))
opaque
β©α΅β‘β·ββ³ :
Ξ β©α΅β¨ l β© t β‘ u β· A β
(Ξ β©α΅β¨ l β© t β· A Γ
Ξ β©α΅β¨ l β© u β· A Γ
(β {m Ξ} {Οβ Οβ : Subst m n} β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©β¨ l β© t [ Οβ ] β‘ u [ Οβ ] β· A [ Οβ ]))
β©α΅β‘β·ββ³ =
(Ξ» tβ‘u β
case wf-β©α΅β‘β· tβ‘u of Ξ»
(β©t , β©u) β
β©t , β©u , Ξ» {_ _ _ _} β β©α΅β‘β·β .projβ tβ‘u .projβ)
, (Ξ» (β©t , _ , tβ‘u) β
β©α΅β‘β·β .projβ (wf-β©α΅β· β©t , tβ‘u))
opaque
β©Λ’β·βββ² :
Ξ β©Λ’ Ο β· Ξ β A β
((β Ξ» l β Ξ β©α΅β¨ l β© A) Γ
(β Ξ» l β Ξ β©β¨ l β© head Ο β· A [ tail Ο ]) Γ
Ξ β©Λ’ tail Ο β· Ξ)
β©Λ’β·βββ² {Ξ} {Ο} {Ξ} {A} =
Ξ β©Λ’ Ο β· Ξ β A ββ¨ β©Λ’β·ββ β©
(β Ξ» l β (Ξ β©α΅β¨ l β© A) Γ Ξ β©β¨ l β© head Ο β· A [ tail Ο ]) Γ
Ξ β©Λ’ tail Ο β· Ξ
ββ¨ (Ξ» ((l , β©A , β©head) , β©tail) β
(l , β©A) , (l , β©head) , β©tail)
, (Ξ» ((lβ , β©A) , (_ , β©head) , β©tail) β
(lβ , β©A , level-β©β· (β©α΅ββ©Λ’β·ββ©[] β©A β©tail) β©head) , β©tail)
β©
(β Ξ» l β Ξ β©α΅β¨ l β© A) Γ
(β Ξ» l β Ξ β©β¨ l β© head Ο β· A [ tail Ο ]) Γ
Ξ β©Λ’ tail Ο β· Ξ β‘β
opaque
β©Λ’β‘β·βββ² :
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β A β
((β Ξ» l β Ξ β©α΅β¨ l β© A) Γ
(β Ξ» l β Ξ β©β¨ l β© head Οβ β‘ head Οβ β· A [ tail Οβ ]) Γ
Ξ β©Λ’ tail Οβ β‘ tail Οβ β· Ξ)
β©Λ’β‘β·βββ² {Ξ} {Οβ} {Οβ} {Ξ} {A} =
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β A ββ¨ β©Λ’β‘β·ββ β©
(β Ξ» l β
(Ξ β©α΅β¨ l β© A) Γ Ξ β©β¨ l β© head Οβ β‘ head Οβ β· A [ tail Οβ ]) Γ
Ξ β©Λ’ tail Οβ β‘ tail Οβ β· Ξ ββ¨ (Ξ» ((l , β©A , headβ‘head) , tailβ‘tail) β
(l , β©A) , (l , headβ‘head) , tailβ‘tail)
, (Ξ» ((lβ , β©A) , (_ , headβ‘head) , tailβ‘tail) β
( lβ , β©A
, level-β©β‘β· (β©α΅ββ©Λ’β·ββ©[] β©A (wf-β©Λ’β‘β· tailβ‘tail .projβ))
headβ‘head
)
, tailβ‘tail)
β©
(β Ξ» l β Ξ β©α΅β¨ l β© A) Γ
(β Ξ» l β Ξ β©β¨ l β© head Οβ β‘ head Οβ β· A [ tail Οβ ]) Γ
Ξ β©Λ’ tail Οβ β‘ tail Οβ β· Ξ β‘β
opaque
conv-β©Λ’β‘β·-β :
Ξ β©α΅β¨ l β© A β‘ B β Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β A β Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β B
conv-β©Λ’β‘β·-β {Ξ} {A} {B} {Ξ} {Οβ} {Οβ} Aβ‘B =
case β©α΅β‘ββ² .projβ Aβ‘B of Ξ»
(_ , β©B , Aβ‘B) β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β A ββ¨ β©Λ’β‘β·ββ β©β
(β Ξ» l β
(Ξ β©α΅β¨ l β© A) Γ Ξ β©β¨ l β© head Οβ β‘ head Οβ β· A [ tail Οβ ]) Γ
Ξ β©Λ’ tail Οβ β‘ tail Οβ β· Ξ ββ¨ (Ξ» ((_ , β©A , Οβββ‘Οββ) , Οβββ‘Οββ) β
(_ , β©B , conv-β©β‘β· (Aβ‘B $ wf-β©Λ’β‘β· Οβββ‘Οββ .projβ) Οβββ‘Οββ)
, Οβββ‘Οββ) β©
(β Ξ» l β
(Ξ β©α΅β¨ l β© B) Γ Ξ β©β¨ l β© head Οβ β‘ head Οβ β· B [ tail Οβ ]) Γ
Ξ β©Λ’ tail Οβ β‘ tail Οβ β· Ξ βΛβ¨ β©Λ’β‘β·ββ β©β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β B β‘
opaque
conv-β©Λ’β·-β : Ξ β©α΅β¨ l β© A β‘ B β Ξ β©Λ’ Ο β· Ξ β A β Ξ β©Λ’ Ο β· Ξ β B
conv-β©Λ’β·-β Aβ‘B =
β©Λ’β·ββ©Λ’β‘β· .projβ ββ conv-β©Λ’β‘β·-β Aβ‘B ββ β©Λ’β·ββ©Λ’β‘β· .projβ
opaque
conv-β-β©α΅ :
Ξ β©α΅β¨ lβ² β© A β‘ B β
Ξ β A β©α΅β¨ l β© C β
Ξ β B β©α΅β¨ l β© C
conv-β-β©α΅ {Ξ} {A} {B} {l} {C} Aβ‘B β©C =
case β©α΅β‘ββ² .projβ Aβ‘B of Ξ»
(β©A , β©B , Aβ‘B) β
β©α΅β .projβ
( β©α΅-β-intro β©B
, Ξ» {_} {Ξ = Ξ} {Οβ = Οβ} {Οβ = Οβ} β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β B ββ¨ β©Λ’β‘β·ββ β©β
(β Ξ» l β
(Ξ β©α΅β¨ l β© B) Γ
Ξ β©β¨ l β© head Οβ β‘ head Οβ β· B [ tail Οβ ]) Γ
Ξ β©Λ’ tail Οβ β‘ tail Οβ β· Ξ ββ¨ (Ξ» ((_ , _ , Οβββ‘Οββ) , Οβββ‘Οββ) β
(_ , β©A , conv-β©β‘β· (sym-β©β‘ $ Aβ‘B $ wf-β©Λ’β‘β· Οβββ‘Οββ .projβ) Οβββ‘Οββ)
, Οβββ‘Οββ) β©
(β Ξ» l β
(Ξ β©α΅β¨ l β© A) Γ
Ξ β©β¨ l β© head Οβ β‘ head Οβ β· A [ tail Οβ ]) Γ
Ξ β©Λ’ tail Οβ β‘ tail Οβ β· Ξ βΛβ¨ β©Λ’β‘β·ββ β©β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β A ββ¨ β©α΅β .projβ β©C .projβ β©
Ξ β©β¨ l β© C [ Οβ ] β‘ C [ Οβ ] β‘
)
opaque
conv-ββ-β©α΅ :
Ξ β©α΅β¨ lβ² β© Aβ β‘ Aβ β
Ξ β Aβ β©α΅β¨ lβ³ β© Bβ β‘ Bβ β
Ξ β Aβ β Bβ β©α΅β¨ l β© C β
Ξ β Aβ β Bβ β©α΅β¨ l β© C
conv-ββ-β©α΅ {Ξ} {Aβ} {Aβ} {Bβ} {Bβ} {l} {C} Aββ‘Aβ Bββ‘Bβ β©C =
case sym-β©α΅β‘ Aββ‘Aβ of Ξ»
Aββ‘Aβ β
case β©α΅β‘ββ² .projβ Bββ‘Bβ of Ξ»
(β©Bβ , β©Bβ , Bββ‘Bβ) β
β©α΅β .projβ
( β©α΅-β-intro (conv-β-β©α΅ Aββ‘Aβ β©Bβ)
, Ξ» {_} {Ξ = Ξ} {Οβ = Οβ} {Οβ = Οβ} β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β Aβ β Bβ ββ¨ β©Λ’β‘β·ββ β©β
(β Ξ» l β
(Ξ β Aβ β©α΅β¨ l β© Bβ) Γ
Ξ β©β¨ l β© head Οβ β‘ head Οβ β· Bβ [ tail Οβ ]) Γ
Ξ β©Λ’ tail Οβ β‘ tail Οβ β· Ξ β Aβ ββ¨ ((Ξ» ((_ , _ , Οβββ‘Οββ) , Οβββ‘Οββ) β
( _ , β©Bβ
, conv-β©β‘β·
(sym-β©β‘ $ Bββ‘Bβ $
conv-β©Λ’β·-β Aββ‘Aβ $ wf-β©Λ’β‘β· Οβββ‘Οββ .projβ)
Οβββ‘Οββ
)
, conv-β©Λ’β‘β·-β Aββ‘Aβ Οβββ‘Οββ)) β©
(β Ξ» l β
(Ξ β Aβ β©α΅β¨ l β© Bβ) Γ
Ξ β©β¨ l β© head Οβ β‘ head Οβ β· Bβ [ tail Οβ ]) Γ
Ξ β©Λ’ tail Οβ β‘ tail Οβ β· Ξ β Aβ βΛβ¨ β©Λ’β‘β·ββ β©β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β Aβ β Bβ ββ¨ β©α΅β .projβ β©C .projβ β©
Ξ β©β¨ l β© C [ Οβ ] β‘ C [ Οβ ] β‘
)
opaque
conv-β©α΅β‘β· :
Ξ β©α΅β¨ l β© A β‘ B β
Ξ β©α΅β¨ lβ² β© t β‘ u β· A β
Ξ β©α΅β¨ l β© t β‘ u β· B
conv-β©α΅β‘β· Aβ‘B tβ‘u =
case β©α΅β‘ββ² .projβ Aβ‘B of Ξ»
(_ , β©B , Aβ‘B) β
β©α΅β‘β·β .projβ
( β©B
, Ξ» Οββ‘Οβ β
conv-β©β‘β· (Aβ‘B $ wf-β©Λ’β‘β· Οββ‘Οβ .projβ) $
β©α΅β‘β·β .projβ tβ‘u .projβ Οββ‘Οβ
)
opaque
conv-β©α΅β· :
Ξ β©α΅β¨ l β© A β‘ B β
Ξ β©α΅β¨ lβ² β© t β· A β
Ξ β©α΅β¨ l β© t β· B
conv-β©α΅β· Aβ‘B =
β©α΅β·ββ©α΅β‘β· .projβ ββ conv-β©α΅β‘β· Aβ‘B ββ β©α΅β·ββ©α΅β‘β· .projβ
opaque
conv-β-β©α΅β· :
Ξ β©α΅β¨ lβ² β© A β‘ B β
Ξ β A β©α΅β¨ l β© t β· C β
Ξ β B β©α΅β¨ l β© t β· C
conv-β-β©α΅β· Aβ‘B β©t =
case β©α΅β·β .projβ β©t of Ξ»
(β©C , tβ‘t) β
β©α΅β·β .projβ
( conv-β-β©α΅ Aβ‘B β©C
, tβ‘t ββ conv-β©Λ’β‘β·-β (sym-β©α΅β‘ Aβ‘B)
)
opaque
β©α΅β·-β :
(β {m Ξ} {Ο : Subst m n} β
Ξ β©Λ’ Ο β· Ξ β
Ξ β’ t [ Ο ] β u [ Ο ] β· A [ Ο ]) β
Ξ β©α΅β¨ l β© u β· A β
Ξ β©α΅β¨ l β© t β‘ u β· A
β©α΅β·-β {t} {u} tβu β©u =
case β©α΅β·β .projβ β©u of Ξ»
(β©A , uβ‘u) β
β©α΅β‘β·β .projβ
( β©A
, Ξ» {_ _} {Οβ = Οβ} {Οβ = Οβ} Οββ‘Οβ β
case wf-β©Λ’β‘β· Οββ‘Οβ of Ξ»
(β©Οβ , _) β
case β©α΅β·ββ©Λ’β·ββ©[]β· β©u β©Οβ of Ξ»
β©u[Οβ] β
t [ Οβ ] β‘β¨ β©β·-β* (tβu β©Οβ β¨ id (escape-β©β· β©u[Οβ])) β©u[Οβ] β©β©β·
u [ Οβ ] β‘β¨ uβ‘u Οββ‘Οβ β©β©β·β
u [ Οβ ] β
)
opaque
cast-β©Λ’β· :
((x : Fin n) β Οβ x PE.β‘ Οβ x) β
Ξ β©Λ’ Οβ β· Ξ β Ξ β©Λ’ Οβ β· Ξ
cast-β©Λ’β· {Ξ = Ξ΅} _ β©Οβ =
β©Λ’β·Ξ΅β .projβ $ β©Λ’β·Ξ΅β .projβ β©Οβ
cast-β©Λ’β· {Ξ = _ β A} Οββ‘Οβ β©Οβ =
case β©Λ’β·ββ .projβ β©Οβ of Ξ»
((_ , β©A , β©Οββ) , β©Οββ) β
case Οββ‘Οβ ββ (_+1) of Ξ»
Οβββ‘Οββ β
β©Λ’β·ββ .projβ
( ( _ , β©A
, PE.substβ (_β©β¨_β©_β·_ _ _) (Οββ‘Οβ x0)
(substVar-to-subst Οβββ‘Οββ A) β©Οββ
)
, cast-β©Λ’β· Οβββ‘Οββ β©Οββ
)
opaque
β©Λ’β‘β·-β’β :
β’ Ξ β
Ο β· Ξ β Ξ β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©Λ’ Ο β’β Οβ β‘ Ο β’β Οβ β· Ξ
β©Λ’β‘β·-β’β {Ξ = Ξ΅} β’Ξ _ _ =
β©Λ’β‘β·Ξ΅β .projβ β’Ξ
β©Λ’β‘β·-β’β {Ξ = _ β A} β’Ξ Οβ Οββ‘Οβ =
case β©Λ’β‘β·ββ .projβ Οββ‘Οβ of Ξ»
((_ , β©A , Οβββ‘Οββ) , Οβββ‘Οββ) β
β©Λ’β‘β·ββ .projβ
( ( _ , β©A
, PE.subst (_β©β¨_β©_β‘_β·_ _ _ _ _) (wk-subst A)
(wk-β©β‘β· Οβ β’Ξ Οβββ‘Οββ)
)
, β©Λ’β‘β·-β’β β’Ξ Οβ Οβββ‘Οββ
)
opaque
β©Λ’β·-β’β :
β’ Ξ β
Ο β· Ξ β Ξ β
Ξ β©Λ’ Ο β· Ξ β
Ξ β©Λ’ Ο β’β Ο β· Ξ
β©Λ’β·-β’β β’Ξ Οβ =
β©Λ’β·ββ©Λ’β‘β· .projβ ββ β©Λ’β‘β·-β’β β’Ξ Οβ ββ β©Λ’β·ββ©Λ’β‘β· .projβ
opaque
β©Λ’β‘β·-ββ’ :
Ο β· Ξ β Ξ β β©α΅ Ξ β Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©Λ’ Οβ ββ’ Ο β‘ Οβ ββ’ Ο β· Ξ
β©Λ’β‘β·-ββ’ TW.id _ Οββ‘Οβ =
Οββ‘Οβ
β©Λ’β‘β·-ββ’ (TW.step Οβ) β©Ξ Οββ‘Οβ =
case β©Λ’β‘β·ββ .projβ Οββ‘Οβ of Ξ»
((_ , β©A , headβ‘head) , tailβ‘tail) β
β©Λ’β‘β·-ββ’ Οβ β©Ξ tailβ‘tail
β©Λ’β‘β·-ββ’ (TW.lift {A} Οβ) β©ΞβA Οββ‘Οβ =
case wf-β©α΅-β β©ΞβA of Ξ»
(_ , β©A) β
case β©Λ’β‘β·ββ .projβ Οββ‘Οβ of Ξ»
((_ , _ , headβ‘head) , tailβ‘tail) β
β©Λ’β‘β·βββ² .projβ
( (_ , β©A)
, (_ , PE.subst (_β©β¨_β©_β‘_β·_ _ _ _ _) (subst-wk A) headβ‘head)
, β©Λ’β‘β·-ββ’ Οβ (wf-β©α΅ β©A) tailβ‘tail
)
opaque
β©Λ’β·-ββ’ : Ο β· Ξ β Ξ β β©α΅ Ξ β Ξ β©Λ’ Ο β· Ξ β Ξ β©Λ’ Ο ββ’ Ο β· Ξ
β©Λ’β·-ββ’ Οβ β©Ξ =
β©Λ’β·ββ©Λ’β‘β· .projβ ββ β©Λ’β‘β·-ββ’ Οβ β©Ξ ββ β©Λ’β·ββ©Λ’β‘β· .projβ
opaque
β©Λ’β‘β·-wk1Subst :
Ξ β’ A β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β A β©Λ’ wk1Subst Οβ β‘ wk1Subst Οβ β· Ξ
β©Λ’β‘β·-wk1Subst β’A = β©Λ’β‘β·-β’β (β’ββ’β β’A) (TW.step TW.id)
opaque
β©Λ’β·-wk1Subst :
Ξ β’ A β
Ξ β©Λ’ Ο β· Ξ β
Ξ β A β©Λ’ wk1Subst Ο β· Ξ
β©Λ’β·-wk1Subst β’A =
β©Λ’β·ββ©Λ’β‘β· .projβ ββ β©Λ’β‘β·-wk1Subst β’A ββ β©Λ’β·ββ©Λ’β‘β· .projβ
opaque
β©Λ’β‘β·-liftSubst :
Ξ β©α΅β¨ l β© A β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β A [ Οβ ] β©Λ’ liftSubst Οβ β‘ liftSubst Οβ β· Ξ β A
β©Λ’β‘β·-liftSubst {A} β©A Οββ‘Οβ =
case escape-β© $ β©α΅ββ©Λ’β·ββ©[] β©A (wf-β©Λ’β‘β· Οββ‘Οβ .projβ) of Ξ»
β’A[Οβ] β
case β©Λ’β‘β·-wk1Subst β’A[Οβ] Οββ‘Οβ of Ξ»
Οββββ‘Οβββ β
case var (β’ββ’β β’A[Οβ])
(PE.substβ (_β·_β_ _) (PE.sym $ wk1Subst-wk1 A) PE.refl
here) of Ξ»
β’0 β
β©Λ’β‘β·ββ .projβ
( ( _ , β©A
, neutral-β©β‘β· (β©α΅ββ©Λ’β·ββ©[] β©A $ wf-β©Λ’β‘β· Οββββ‘Οβββ .projβ)
(var _) (var _) β’0 β’0 (~-var β’0)
)
, Οββββ‘Οβββ
)
opaque
β©Λ’β·-liftSubst :
Ξ β©α΅β¨ l β© A β
Ξ β©Λ’ Ο β· Ξ β
Ξ β A [ Ο ] β©Λ’ liftSubst Ο β· Ξ β A
β©Λ’β·-liftSubst β©A =
β©Λ’β·ββ©Λ’β‘β· .projβ ββ β©Λ’β‘β·-liftSubst β©A ββ β©Λ’β·ββ©Λ’β‘β· .projβ
opaque
β©Λ’β‘β·-liftSubstβ² :
Ξ β©α΅β¨ l β© Aβ β‘ Aβ β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β Aβ [ Οβ ] β©Λ’ liftSubst Οβ β‘ liftSubst Οβ β· Ξ β Aβ
β©Λ’β‘β·-liftSubstβ² {Aβ} {Aβ} {Οβ} Aββ‘Aβ Οββ‘Οβ =
conv-β©Λ’β‘β·-β Aββ‘Aβ $
β©Λ’β‘β·-liftSubst (wf-β©α΅β‘ Aββ‘Aβ .projβ) Οββ‘Οβ
opaque
β©Λ’β·-liftSubstβ² :
Ξ β©α΅β¨ l β© Aβ β‘ Aβ β
Ξ β©Λ’ Ο β· Ξ β
Ξ β Aβ [ Ο ] β©Λ’ liftSubst Ο β· Ξ β Aβ
β©Λ’β·-liftSubstβ² Aββ‘Aβ =
β©Λ’β·ββ©Λ’β‘β· .projβ ββ β©Λ’β‘β·-liftSubstβ² Aββ‘Aβ ββ β©Λ’β·ββ©Λ’β‘β· .projβ
opaque
β©Λ’β·-idSubst :
β©α΅ Ξ β
Ξ β©Λ’ idSubst β· Ξ
β©Λ’β·-idSubst {Ξ = Ξ΅} _ =
β©Λ’β·Ξ΅β .projβ Ξ΅
β©Λ’β·-idSubst {Ξ = _ β _} β©ΞβA =
case β©α΅ββ .projβ β©ΞβA .projβ of Ξ»
β©A β
PE.substβ _β©Λ’_β·_ (PE.cong (_β_ _) $ subst-id _) PE.refl PE.refl $
cast-β©Λ’β· subst-lift-id $
β©Λ’β·-liftSubst (β©α΅ββ .projβ β©ΞβA .projβ)
(β©Λ’β·-idSubst (β©α΅β .projβ β©A .projβ))
opaque
β©Λ’β‘β·-sgSubst :
Ξ β©α΅β¨ lβ² β© A β
Ξ β©β¨ l β© t β‘ u β· A β
Ξ β©Λ’ sgSubst t β‘ sgSubst u β· Ξ β A
β©Λ’β‘β·-sgSubst β©A tβ‘u =
β©Λ’β‘β·βββ² .projβ
( (_ , β©A)
, (_ , PE.subst (_β©β¨_β©_β‘_β·_ _ _ _ _) (PE.sym $ subst-id _) tβ‘u)
, refl-β©Λ’β‘β· (β©Λ’β·-idSubst (wf-β©α΅ β©A))
)
opaque
β©Λ’β·-sgSubst :
Ξ β©α΅β¨ lβ² β© A β
Ξ β©β¨ l β© t β· A β
Ξ β©Λ’ sgSubst t β· Ξ β A
β©Λ’β·-sgSubst β©A =
β©Λ’β·ββ©Λ’β‘β· .projβ ββ β©Λ’β‘β·-sgSubst β©A ββ β©β·ββ©β‘β· .projβ
opaque
β©α΅β‘ββ©β‘ : Ξ β©α΅β¨ l β© A β‘ B β Ξ β©β¨ l β© A β‘ B
β©α΅β‘ββ©β‘ {Ξ} {l} {A} {B} =
Ξ β©α΅β¨ l β© A β‘ B ββ¨ β©α΅β‘ββ² β©β
(Ξ β©α΅β¨ l β© A) Γ
(Ξ β©α΅β¨ l β© B) Γ
(β {m} {Ξ : Con Term m} {Ο} β
Ξ β©Λ’ Ο β· Ξ β Ξ β©β¨ l β© A [ Ο ] β‘ B [ Ο ]) ββ¨ (Ξ» (β©A , _ , Aβ‘B) β Aβ‘B $ β©Λ’β·-idSubst $ wf-β©α΅ β©A) β©
Ξ β©β¨ l β© A [ idSubst ] β‘ B [ idSubst ] β‘β¨ PE.congβ (_β©β¨_β©_β‘_ _ _) (subst-id _) (subst-id _) β©β
Ξ β©β¨ l β© A β‘ B β‘
opaque
β©α΅ββ© : Ξ β©α΅β¨ l β© A β Ξ β©β¨ l β© A
β©α΅ββ© = β©ββ©β‘ .projβ ββ β©α΅β‘ββ©β‘ ββ β©α΅ββ©α΅β‘ .projβ
opaque
β©α΅β‘β·ββ©β‘β· : Ξ β©α΅β¨ l β© t β‘ u β· A β Ξ β©β¨ l β© t β‘ u β· A
β©α΅β‘β·ββ©β‘β· {Ξ} {l} {t} {u} {A} =
Ξ β©α΅β¨ l β© t β‘ u β· A ββ¨ β©α΅β‘β·ββ² β©β
(Ξ β©α΅β¨ l β© t β· A) Γ
(Ξ β©α΅β¨ l β© u β· A) Γ
(β {m} {Ξ : Con Term m} {Ο} β
Ξ β©Λ’ Ο β· Ξ β Ξ β©β¨ l β© t [ Ο ] β‘ u [ Ο ] β· A [ Ο ]) ββ¨ (Ξ» (β©t , _ , tβ‘u) β tβ‘u $ β©Λ’β·-idSubst $ wf-β©α΅ $ wf-β©α΅β· β©t) β©
Ξ β©β¨ l β© t [ idSubst ] β‘ u [ idSubst ] β· A [ idSubst ] β‘β¨ PE.congβ (_β©β¨_β©_β‘_β·_ _ _)
(subst-id _) (subst-id _) (subst-id _) β©β
Ξ β©β¨ l β© t β‘ u β· A β‘
opaque
β©α΅β·ββ©β· : Ξ β©α΅β¨ l β© t β· A β Ξ β©β¨ l β© t β· A
β©α΅β·ββ©β· = β©β·ββ©β‘β· .projβ ββ β©α΅β‘β·ββ©β‘β· ββ β©α΅β·ββ©α΅β‘β· .projβ
opaque
escape-β©α΅ : Ξ β©α΅β¨ l β© A β Ξ β’ A
escape-β©α΅ = escape-β© ββ β©α΅ββ©
opaque
escape-β©α΅β² : β©α΅ Ξ β β’ Ξ
escape-β©α΅β² {Ξ = Ξ΅} = Ξ» _ β Ξ΅
escape-β©α΅β² {Ξ = _ β _} = β’ββ’β ββ escape-β©α΅ ββ projβ ββ β©α΅ββ .projβ
opaque
escape-β©α΅β‘ : Ξ β©α΅β¨ l β© A β‘ B β Ξ β’ A β
B
escape-β©α΅β‘ = escape-β©β‘ ββ β©α΅β‘ββ©β‘
opaque
escape-β©α΅β· : Ξ β©α΅β¨ l β© t β· A β Ξ β’ t β· A
escape-β©α΅β· = escape-β©β· ββ β©α΅β·ββ©β·
opaque
escape-β©α΅β‘β· : Ξ β©α΅β¨ l β© t β‘ u β· A β Ξ β’ t β
u β· A
escape-β©α΅β‘β· = escape-β©β‘β· ββ β©α΅β‘β·ββ©β‘β·
opaque
escape-β©Λ’β· : Ξ β©Λ’ Ο β· Ξ β β’ Ξ Γ Ξ β’Λ’ Ο β· Ξ
escape-β©Λ’β· {Ξ} {Ο} {Ξ = Ξ΅} =
Ξ β©Λ’ Ο β· Ξ΅ ββ¨ β©Λ’β·Ξ΅β β©β
β’ Ξ ββ¨ _, id β©
β’ Ξ Γ Ξ β’Λ’ Ο β· Ξ΅ β‘
escape-β©Λ’β· {Ξ} {Ο} {Ξ = Ξ β A} =
Ξ β©Λ’ Ο β· Ξ β A ββ¨ β©Λ’β·ββ β©β
(β Ξ» l β (Ξ β©α΅β¨ l β© A) Γ Ξ β©β¨ l β© head Ο β· A [ tail Ο ]) Γ
Ξ β©Λ’ tail Ο β· Ξ ββ¨ (Ξ» ((_ , _ , β©Οβ) , β©Οβ) β
escape-β©β· β©Οβ , escape-β©Λ’β· β©Οβ) β©
Ξ β’ head Ο β· A [ tail Ο ] Γ β’ Ξ Γ Ξ β’Λ’ tail Ο β· Ξ ββ¨ (Ξ» (β’Οβ , β’Ξ , β’Οβ) β β’Ξ , (β’Οβ , β’Οβ)) β©
β’ Ξ Γ Ξ β’Λ’ Ο β· Ξ β A β‘
opaque
escape-β©Λ’β‘β· : Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β β’ Ξ Γ Ξ β’Λ’ Οβ β‘ Οβ β· Ξ
escape-β©Λ’β‘β· {Ξ} {Οβ} {Οβ} {Ξ = Ξ΅} =
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ΅ ββ¨ β©Λ’β‘β·Ξ΅β β©β
β’ Ξ ββ¨ _, id β©
β’ Ξ Γ Ξ β’Λ’ Οβ β‘ Οβ β· Ξ΅ β‘
escape-β©Λ’β‘β· {Ξ} {Οβ} {Οβ} {Ξ = Ξ β A} =
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β A ββ¨ β©Λ’β‘β·ββ β©β
(β Ξ» l β
(Ξ β©α΅β¨ l β© A) Γ Ξ β©β¨ l β© head Οβ β‘ head Οβ β· A [ tail Οβ ]) Γ
Ξ β©Λ’ tail Οβ β‘ tail Οβ β· Ξ ββ¨ (Ξ» ((_ , _ , Οβββ‘Οββ) , Οβββ‘Οββ) β
β
β-eq (escape-β©β‘β· Οβββ‘Οββ) , escape-β©Λ’β‘β· Οβββ‘Οββ) β©
Ξ β’ head Οβ β‘ head Οβ β· A [ tail Οβ ] Γ
β’ Ξ Γ Ξ β’Λ’ tail Οβ β‘ tail Οβ β· Ξ ββ¨ (Ξ» (Οβββ‘Οββ , β’Ξ , Οβββ‘Οββ) β β’Ξ , (Οβββ‘Οββ , Οβββ‘Οββ)) β©
β’ Ξ Γ Ξ β’Λ’ Οβ β‘ Οβ β· Ξ β A β‘
opaque
emb-β©α΅ :
l β€ lβ² β
Ξ β©α΅β¨ l β© A β
Ξ β©α΅β¨ lβ² β© A
emb-β©α΅ lβ€lβ² β©A =
case β©α΅β .projβ β©A of Ξ»
(β©Ξ , Aβ‘A) β
β©α΅β .projβ (β©Ξ , emb-β©β‘ lβ€lβ² ββ Aβ‘A)
opaque
emb-β©α΅β· :
l β€ lβ² β
Ξ β©α΅β¨ l β© t β· A β
Ξ β©α΅β¨ lβ² β© t β· A
emb-β©α΅β· lβ€lβ² β©t =
level-β©α΅β· (emb-β©α΅ lβ€lβ² (wf-β©α΅β· β©t)) β©t
opaque
wk-β©α΅β‘ :
Ο β· Ξ β Ξ β β©α΅ Ξ β Ξ β©α΅β¨ l β© A β‘ B β Ξ β©α΅β¨ l β© wk Ο A β‘ wk Ο B
wk-β©α΅β‘ {Ο} {A} {B} Οβ β©Ξ Aβ‘B =
case β©α΅β‘β .projβ Aβ‘B of Ξ»
(β©Ξ , Aβ‘B) β
β©α΅β‘β .projβ
( β©Ξ
, Ξ» {_ _} {Οβ = Οβ} {Οβ = Οβ} Οββ‘Οβ β
wk Ο A [ Οβ ] β‘β¨ subst-wk A β©β©β‘
A [ Οβ ββ’ Ο ] β‘β¨ Aβ‘B $ β©Λ’β‘β·-ββ’ Οβ β©Ξ Οββ‘Οβ β©β©ββ‘
B [ Οβ ββ’ Ο ] β‘Λβ¨ subst-wk B β©
wk Ο B [ Οβ ] β
)
opaque
wk1-β©α΅β‘ : Ξ β©α΅β¨ lβ² β© C β Ξ β©α΅β¨ l β© A β‘ B β Ξ β C β©α΅β¨ l β© wk1 A β‘ wk1 B
wk1-β©α΅β‘ β©C =
wk-β©α΅β‘ (TW.step TW.id) (β©α΅-β-intro β©C)
opaque
wk-β©α΅ : Ο β· Ξ β Ξ β β©α΅ Ξ β Ξ β©α΅β¨ l β© A β Ξ β©α΅β¨ l β© wk Ο A
wk-β©α΅ Οβ β©Ξ =
β©α΅ββ©α΅β‘ .projβ ββ wk-β©α΅β‘ Οβ β©Ξ ββ β©α΅ββ©α΅β‘ .projβ
opaque
wk1-β©α΅ : Ξ β©α΅β¨ lβ² β© B β Ξ β©α΅β¨ l β© A β Ξ β B β©α΅β¨ l β© wk1 A
wk1-β©α΅ β©B =
wk-β©α΅ (TW.step TW.id) (β©α΅-β-intro β©B)
opaque
wk-β©α΅β‘β· :
Ο β· Ξ β Ξ β β©α΅ Ξ β Ξ β©α΅β¨ l β© t β‘ u β· A β
Ξ β©α΅β¨ l β© wk Ο t β‘ wk Ο u β· wk Ο A
wk-β©α΅β‘β· {Ο} {t} {u} {A} Οβ β©Ξ tβ‘u =
case wf-β©α΅β· $ wf-β©α΅β‘β· tβ‘u .projβ of Ξ»
β©A β
β©α΅β‘β·β .projβ
( wk-β©α΅ Οβ β©Ξ β©A
, Ξ» {_ _} {Οβ = Οβ} {Οβ = Οβ} Οββ‘Οβ β
wk Ο t [ Οβ ] β· wk Ο A [ Οβ ] β‘β¨ subst-wk t β©β©β·β·β‘
β¨ subst-wk A β©β©β·β‘
t [ Οβ ββ’ Ο ] β· A [ Οβ ββ’ Ο ] β‘β¨ β©α΅β‘β·β .projβ tβ‘u .projβ $
β©Λ’β‘β·-ββ’ Οβ (wf-β©α΅ β©A) Οββ‘Οβ β©β©β·ββ·β‘
u [ Οβ ββ’ Ο ] β‘Λβ¨ subst-wk u β©
wk Ο u [ Οβ ] β
)
opaque
wk1-β©α΅β‘β· :
Ξ β©α΅β¨ lβ² β© B β Ξ β©α΅β¨ l β© t β‘ u β· A β
Ξ β B β©α΅β¨ l β© wk1 t β‘ wk1 u β· wk1 A
wk1-β©α΅β‘β· β©B =
wk-β©α΅β‘β· (TW.step TW.id) (β©α΅-β-intro β©B)
opaque
wk-β©α΅β· :
Ο β· Ξ β Ξ β β©α΅ Ξ β Ξ β©α΅β¨ l β© t β· A β Ξ β©α΅β¨ l β© wk Ο t β· wk Ο A
wk-β©α΅β· Οβ β©Ξ =
β©α΅β·ββ©α΅β‘β· .projβ ββ wk-β©α΅β‘β· Οβ β©Ξ ββ β©α΅β·ββ©α΅β‘β· .projβ
opaque
wk1-β©α΅β· : Ξ β©α΅β¨ lβ² β© B β Ξ β©α΅β¨ l β© t β· A β Ξ β B β©α΅β¨ l β© wk1 t β· wk1 A
wk1-β©α΅β· β©B =
wk-β©α΅β· (TW.step TW.id) (β©α΅-β-intro β©B)
opaque
β©α΅β‘ββ©α΅β‘β·ββ©α΅[]ββ‘[]β :
Ξ β A β©α΅β¨ l β© B β‘ C β
Ξ β©α΅β¨ lβ² β© t β‘ u β· A β
Ξ β©α΅β¨ l β© B [ t ]β β‘ C [ u ]β
β©α΅β‘ββ©α΅β‘β·ββ©α΅[]ββ‘[]β {B} {C} Bβ‘C tβ‘u =
case β©α΅β‘β·β .projβ tβ‘u of Ξ»
(β©A , tβ‘u) β
β©α΅β‘β .projβ
( wf-β©α΅ β©A
, Ξ» Οββ‘Οβ β
PE.substβ (_β©β¨_β©_β‘_ _ _) (substConsId B) (substConsId C) $
β©α΅β‘β .projβ Bβ‘C .projβ $
β©Λ’β‘β·ββ .projβ ((_ , β©A , tβ‘u Οββ‘Οβ) , Οββ‘Οβ)
)
opaque
β©α΅ββ©α΅β·ββ©α΅[]β :
Ξ β A β©α΅β¨ l β© B β
Ξ β©α΅β¨ lβ² β© t β· A β
Ξ β©α΅β¨ l β© B [ t ]β
β©α΅ββ©α΅β·ββ©α΅[]β β©B β©t =
β©α΅ββ©α΅β‘ .projβ $ β©α΅β‘ββ©α΅β‘β·ββ©α΅[]ββ‘[]β (refl-β©α΅β‘ β©B) (refl-β©α΅β‘β· β©t)
opaque
β©α΅β·ββ©α΅β·ββ©α΅[]ββ· :
Ξ β A β©α΅β¨ l β© t β· B β
Ξ β©α΅β¨ lβ² β© u β· A β
Ξ β©α΅β¨ l β© t [ u ]β β· B [ u ]β
β©α΅β·ββ©α΅β·ββ©α΅[]ββ· {t} {B} β©t β©u =
case β©α΅β·β .projβ β©t of Ξ»
(β©B , tβ‘t) β
β©α΅β·β .projβ
( β©α΅ββ©α΅β·ββ©α΅[]β β©B β©u
, Ξ» Οββ‘Οβ β
PE.substβ (_β©β¨_β©_β‘_β·_ _ _)
(substConsId t) (substConsId t) (substConsId B) $
tβ‘t $
β©Λ’β‘β·βββ² .projβ
( wf-β-β©α΅ β©B
, (_ , β©α΅β·β .projβ β©u .projβ Οββ‘Οβ)
, Οββ‘Οβ
)
)
opaque
β©α΅β‘ββ©α΅β‘β·ββ©α΅β‘β·ββ©α΅[]βββ‘[]ββ :
Ξ β A β B β©α΅β¨ l β© Cβ β‘ Cβ β
Ξ β©α΅β¨ lβ³ β© tβ β‘ tβ β· A β
Ξ β©α΅β¨ lβ΄ β© uβ β‘ uβ β· B [ tβ ]β β
Ξ β©α΅β¨ l β© Cβ [ tβ , uβ ]ββ β‘ Cβ [ tβ , uβ ]ββ
β©α΅β‘ββ©α΅β‘β·ββ©α΅β‘β·ββ©α΅[]βββ‘[]ββ {B} {Cβ} {Cβ} Cββ‘Cβ tββ‘tβ uββ‘uβ =
case β©α΅β‘β .projβ Cββ‘Cβ of Ξ»
(β©ΞβAβB , Cββ‘Cβ) β
case wf-β©α΅-β β©ΞβAβB of Ξ»
(_ , β©B) β
case wf-β-β©α΅ β©B of Ξ»
(_ , β©A) β
β©α΅β‘β .projβ
( wf-β©α΅ β©A
, Ξ» Οββ‘Οβ β
PE.substβ (_β©β¨_β©_β‘_ _ _)
(PE.sym $ [,]-[]-fusion Cβ) (PE.sym $ [,]-[]-fusion Cβ) $
Cββ‘Cβ $
β©Λ’β‘β·βββ² .projβ
( (_ , β©B)
, ( _
, PE.subst (_β©β¨_β©_β‘_β·_ _ _ _ _) (PE.sym $ substConsId B)
(β©α΅β‘β·β .projβ uββ‘uβ .projβ Οββ‘Οβ)
)
, β©Λ’β‘β·βββ² .projβ
( (_ , β©A)
, (_ , β©α΅β‘β·β .projβ tββ‘tβ .projβ Οββ‘Οβ)
, Οββ‘Οβ
)
)
)
opaque
β©α΅ββ©α΅β·ββ©α΅β·ββ©α΅[]ββ :
Ξ β A β B β©α΅β¨ l β© C β
Ξ β©α΅β¨ lβ³ β© t β· A β
Ξ β©α΅β¨ lβ΄ β© u β· B [ t ]β β
Ξ β©α΅β¨ l β© C [ t , u ]ββ
β©α΅ββ©α΅β·ββ©α΅β·ββ©α΅[]ββ β©C β©t β©u =
β©α΅ββ©α΅β‘ .projβ $
β©α΅β‘ββ©α΅β‘β·ββ©α΅β‘β·ββ©α΅[]βββ‘[]ββ
(refl-β©α΅β‘ β©C) (refl-β©α΅β‘β· β©t) (refl-β©α΅β‘β· β©u)
opaque
β©α΅β‘β·ββ©α΅β‘β·ββ©α΅β‘β·ββ©α΅[]βββ‘[]βββ· :
Ξ β A β B β©α΅β¨ l β© tβ β‘ tβ β· C β
Ξ β©α΅β¨ lβ³ β© uβ β‘ uβ β· A β
Ξ β©α΅β¨ lβ΄ β© vβ β‘ vβ β· B [ uβ ]β β
Ξ β©α΅β¨ l β© tβ [ uβ , vβ ]ββ β‘ tβ [ uβ , vβ ]ββ β· C [ uβ , vβ ]ββ
β©α΅β‘β·ββ©α΅β‘β·ββ©α΅β‘β·ββ©α΅[]βββ‘[]βββ· {B} {tβ} {tβ} {C} tββ‘tβ uββ‘uβ vββ‘vβ =
case wf-β©α΅β· $ wf-β©α΅β‘β· tββ‘tβ .projβ of Ξ»
β©C β
case wf-β-β©α΅ β©C of Ξ»
(_ , β©B) β
β©α΅β‘β·β .projβ
( β©α΅ββ©α΅β·ββ©α΅β·ββ©α΅[]ββ
β©C (wf-β©α΅β‘β· uββ‘uβ .projβ) (wf-β©α΅β‘β· vββ‘vβ .projβ)
, Ξ» Οββ‘Οβ β
PE.substβ (_β©β¨_β©_β‘_β·_ _ _) (PE.sym $ [,]-[]-fusion tβ)
(PE.sym $ [,]-[]-fusion tβ) (PE.sym $ [,]-[]-fusion C) $
β©α΅β‘β·β .projβ tββ‘tβ .projβ $
β©Λ’β‘β·βββ² .projβ
( (_ , β©B)
, ( _
, (PE.subst (_β©β¨_β©_β‘_β·_ _ _ _ _)
(PE.sym $ substConsId B) $
β©α΅β‘β·β .projβ vββ‘vβ .projβ Οββ‘Οβ)
)
, β©Λ’β‘β·βββ² .projβ
( wf-β-β©α΅ β©B
, (_ , β©α΅β‘β·β .projβ uββ‘uβ .projβ Οββ‘Οβ)
, Οββ‘Οβ
)
)
)
opaque
β©α΅β·ββ©α΅β·ββ©α΅β·ββ©α΅[]βββ· :
Ξ β A β B β©α΅β¨ l β© t β· C β
Ξ β©α΅β¨ lβ² β© u β· A β
Ξ β©α΅β¨ lβ³ β© v β· B [ u ]β β
Ξ β©α΅β¨ l β© t [ u , v ]ββ β· C [ u , v ]ββ
β©α΅β·ββ©α΅β·ββ©α΅β·ββ©α΅[]βββ· β©t β©u β©v =
β©α΅β·ββ©α΅β‘β· .projβ $
β©α΅β‘β·ββ©α΅β‘β·ββ©α΅β‘β·ββ©α΅[]βββ‘[]βββ·
(refl-β©α΅β‘β· β©t) (refl-β©α΅β‘β· β©u) (refl-β©α΅β‘β· β©v)
opaque
β©α΅β‘ββ©α΅β·ββ©α΅[]βΒ²β‘[]βΒ² :
Ξ β A β©α΅β¨ l β© D β‘ E β
Ξ β B β C β©α΅β¨ lβ² β© t β· wk2 A β
Ξ β B β C β©α΅β¨ l β© D [ t ]βΒ² β‘ E [ t ]βΒ²
β©α΅β‘ββ©α΅β·ββ©α΅[]βΒ²β‘[]βΒ² {A} {D} {E} Dβ‘E β©t =
case β©α΅β‘β .projβ Dβ‘E of Ξ»
(β©ΞβA , Dβ‘E) β
β©α΅β‘β .projβ
( wf-β©α΅ (wf-β©α΅β· β©t)
, Ξ» Οββ‘Οβ β
PE.substβ (_β©β¨_β©_β‘_ _ _) (substCompβΒ² D _) (substCompβΒ² E _) $
Dβ‘E $
β©Λ’β‘β·βββ² .projβ
( wf-β©α΅-β β©ΞβA
, ( _
, PE.subst (_β©β¨_β©_β‘_β·_ _ _ _ _) (wk2-tail A)
(β©α΅β·β .projβ β©t .projβ Οββ‘Οβ)
)
, β©Λ’β‘β·ββ .projβ (β©Λ’β‘β·ββ .projβ Οββ‘Οβ .projβ) .projβ
)
)
opaque
β©α΅ββ©α΅β·ββ©α΅[]βΒ² :
Ξ β A β©α΅β¨ l β© D β
Ξ β B β C β©α΅β¨ lβ² β© t β· wk2 A β
Ξ β B β C β©α΅β¨ l β© D [ t ]βΒ²
β©α΅ββ©α΅β·ββ©α΅[]βΒ² β©D β©t =
β©α΅ββ©α΅β‘ .projβ $ β©α΅β‘ββ©α΅β·ββ©α΅[]βΒ²β‘[]βΒ² (refl-β©α΅β‘ β©D) β©t
opaque
β©α΅β‘β·ββ©α΅β·ββ©α΅[]βΒ²β‘[]βΒ²β· :
Ξ β A β©α΅β¨ l β© t β‘ u β· D β
Ξ β B β C β©α΅β¨ lβ² β© v β· wk2 A β
Ξ β B β C β©α΅β¨ l β© t [ v ]βΒ² β‘ u [ v ]βΒ² β· D [ v ]βΒ²
β©α΅β‘β·ββ©α΅β·ββ©α΅[]βΒ²β‘[]βΒ²β· {A} {t} {u} {D} tβ‘u β©v =
case wf-β©α΅β· (wf-β©α΅β‘β· tβ‘u .projβ) of Ξ»
β©D β
β©α΅β‘β·β .projβ
( β©α΅ββ©α΅β·ββ©α΅[]βΒ² β©D β©v
, Ξ» Οββ‘Οβ β
PE.substβ (_β©β¨_β©_β‘_β·_ _ _) (substCompβΒ² t _) (substCompβΒ² u _)
(substCompβΒ² D _) $
β©α΅β‘β·β .projβ tβ‘u .projβ $
β©Λ’β‘β·βββ² .projβ
( wf-β-β©α΅ β©D
, ( _
, PE.subst (_β©β¨_β©_β‘_β·_ _ _ _ _) (wk2-tail A)
(β©α΅β·β .projβ β©v .projβ Οββ‘Οβ)
)
, β©Λ’β‘β·ββ .projβ (β©Λ’β‘β·ββ .projβ Οββ‘Οβ .projβ) .projβ
)
)
opaque
β©α΅β·ββ©α΅β·ββ©α΅[]βΒ²β· :
Ξ β A β©α΅β¨ l β© t β· D β
Ξ β B β C β©α΅β¨ lβ² β© u β· wk2 A β
Ξ β B β C β©α΅β¨ l β© t [ u ]βΒ² β· D [ u ]βΒ²
β©α΅β·ββ©α΅β·ββ©α΅[]βΒ²β· β©t β©u =
β©α΅β·ββ©α΅β‘β· .projβ $ β©α΅β‘β·ββ©α΅β·ββ©α΅[]βΒ²β‘[]βΒ²β· (refl-β©α΅β‘β· β©t) β©u
opaque
β©α΅β‘ββ©β‘β·ββ©[]ββ‘[]β :
Ξ β A β©α΅β¨ l β© B β‘ C β
Ξ β©β¨ lβ² β© t β‘ u β· A β
Ξ β©β¨ l β© B [ t ]β β‘ C [ u ]β
β©α΅β‘ββ©β‘β·ββ©[]ββ‘[]β Bβ‘C tβ‘u =
case wf-β-β©α΅ (wf-β©α΅β‘ Bβ‘C .projβ) of Ξ»
(_ , β©A) β
β©α΅β‘β .projβ Bβ‘C .projβ $
β©Λ’β‘β·-sgSubst β©A (level-β©β‘β· (β©α΅ββ© β©A) tβ‘u)
opaque
β©α΅ββ©β·ββ©[]β :
Ξ β A β©α΅β¨ l β© B β
Ξ β©β¨ lβ² β© t β· A β
Ξ β©β¨ l β© B [ t ]β
β©α΅ββ©β·ββ©[]β β©B β©t =
β©ββ©β‘ .projβ $ β©α΅β‘ββ©β‘β·ββ©[]ββ‘[]β (refl-β©α΅β‘ β©B) (refl-β©β‘β· β©t)
opaque
β©α΅β‘β·ββ©β‘β·ββ©[]ββ‘[]ββ· :
Ξ β A β©α΅β¨ l β© t β‘ u β· B β
Ξ β©β¨ lβ² β© v β‘ w β· A β
Ξ β©β¨ l β© t [ v ]β β‘ u [ w ]β β· B [ v ]β
β©α΅β‘β·ββ©β‘β·ββ©[]ββ‘[]ββ· tβ‘u vβ‘w =
case wf-β-β©α΅ (wf-β©α΅β· (wf-β©α΅β‘β· tβ‘u .projβ)) of Ξ»
(_ , β©A) β
β©α΅β‘β·β .projβ tβ‘u .projβ $
β©Λ’β‘β·-sgSubst β©A (level-β©β‘β· (β©α΅ββ© β©A) vβ‘w)
opaque
β©α΅β·ββ©β·ββ©[]ββ· :
Ξ β A β©α΅β¨ l β© t β· B β
Ξ β©β¨ lβ² β© u β· A β
Ξ β©β¨ l β© t [ u ]β β· B [ u ]β
β©α΅β·ββ©β·ββ©[]ββ· β©t β©u =
β©β·ββ©β‘β· .projβ $ β©α΅β‘β·ββ©β‘β·ββ©[]ββ‘[]ββ· (refl-β©α΅β‘β· β©t) (refl-β©β‘β· β©u)
opaque
β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©[,]β‘[,] :
Ξ β A β©α΅β¨ l β© Bβ β‘ Bβ β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©β¨ lβ² β© tβ β‘ tβ β· A [ Οβ ] β
Ξ β©β¨ l β© Bβ [ consSubst Οβ tβ ] β‘ Bβ [ consSubst Οβ tβ ]
β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©[,]β‘[,] Bββ‘Bβ Οββ‘Οβ tββ‘tβ =
β©α΅β‘β .projβ Bββ‘Bβ .projβ $
β©Λ’β‘β·βββ² .projβ (wf-β-β©α΅ (wf-β©α΅β‘ Bββ‘Bβ .projβ) , (_ , tββ‘tβ) , Οββ‘Οβ)
opaque
β©α΅ββ©Λ’β·ββ©β·ββ©[,] :
Ξ β A β©α΅β¨ l β© B β
Ξ β©Λ’ Ο β· Ξ β
Ξ β©β¨ lβ² β© t β· A [ Ο ] β
Ξ β©β¨ l β© B [ consSubst Ο t ]
β©α΅ββ©Λ’β·ββ©β·ββ©[,] β©B β©Ο β©t =
β©ββ©β‘ .projβ $
β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©[,]β‘[,] (refl-β©α΅β‘ β©B) (refl-β©Λ’β‘β· β©Ο) (refl-β©β‘β· β©t)
opaque
β©α΅β‘β·ββ©Λ’β‘β·ββ©β‘β·ββ©[,]β‘[,]β· :
Ξ β A β©α΅β¨ l β© tβ β‘ tβ β· B β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©β¨ lβ² β© uβ β‘ uβ β· A [ Οβ ] β
Ξ β©β¨ l β© tβ [ consSubst Οβ uβ ] β‘ tβ [ consSubst Οβ uβ ] β·
B [ consSubst Οβ uβ ]
β©α΅β‘β·ββ©Λ’β‘β·ββ©β‘β·ββ©[,]β‘[,]β· tββ‘tβ Οββ‘Οβ uββ‘uβ =
β©α΅β‘β·β .projβ tββ‘tβ .projβ $
β©Λ’β‘β·βββ² .projβ
(wf-β-β©α΅ (wf-β©α΅β· $ wf-β©α΅β‘β· tββ‘tβ .projβ) , (_ , uββ‘uβ) , Οββ‘Οβ)
opaque
β©α΅β·ββ©Λ’β·ββ©β·ββ©[,]β· :
Ξ β A β©α΅β¨ l β© t β· B β
Ξ β©Λ’ Ο β· Ξ β
Ξ β©β¨ lβ² β© u β· A [ Ο ] β
Ξ β©β¨ l β© t [ consSubst Ο u ] β· B [ consSubst Ο u ]
β©α΅β·ββ©Λ’β·ββ©β·ββ©[,]β· β©t β©Ο β©u =
β©β·ββ©β‘β· .projβ $
β©α΅β‘β·ββ©Λ’β‘β·ββ©β‘β·ββ©[,]β‘[,]β· (refl-β©α΅β‘β· β©t) (refl-β©Λ’β‘β· β©Ο) (refl-β©β‘β· β©u)
opaque
β©α΅β‘ββ©Λ’β‘β·ββ©[β]β‘[β] :
Ξ β A β©α΅β¨ l β© Bβ β‘ Bβ β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β A [ Οβ ] β©β¨ l β© Bβ [ Οβ β ] β‘ Bβ [ Οβ β ]
β©α΅β‘ββ©Λ’β‘β·ββ©[β]β‘[β] Bββ‘Bβ Οββ‘Οβ =
β©α΅β‘β .projβ Bββ‘Bβ .projβ $
β©Λ’β‘β·-liftSubst (wf-β-β©α΅ (wf-β©α΅β‘ Bββ‘Bβ .projβ) .projβ) Οββ‘Οβ
opaque
β©α΅ββ©Λ’β·ββ©[β] :
Ξ β A β©α΅β¨ l β© B β
Ξ β©Λ’ Ο β· Ξ β
Ξ β A [ Ο ] β©β¨ l β© B [ Ο β ]
β©α΅ββ©Λ’β·ββ©[β] β©B β©Ο =
β©ββ©β‘ .projβ $ β©α΅β‘ββ©Λ’β‘β·ββ©[β]β‘[β] (refl-β©α΅β‘ β©B) (refl-β©Λ’β‘β· β©Ο)
opaque
β©α΅β‘β·ββ©Λ’β‘β·ββ©[β]β‘[β]β· :
Ξ β A β©α΅β¨ l β© tβ β‘ tβ β· B β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β A [ Οβ ] β©β¨ l β© tβ [ Οβ β ] β‘ tβ [ Οβ β ] β· B [ Οβ β ]
β©α΅β‘β·ββ©Λ’β‘β·ββ©[β]β‘[β]β· tββ‘tβ Οββ‘Οβ =
β©α΅β‘β·β .projβ tββ‘tβ .projβ $
β©Λ’β‘β·-liftSubst (wf-β-β©α΅ (wf-β©α΅β· (wf-β©α΅β‘β· tββ‘tβ .projβ)) .projβ)
Οββ‘Οβ
opaque
β©α΅β·ββ©Λ’β·ββ©[β]β· :
Ξ β A β©α΅β¨ l β© t β· B β
Ξ β©Λ’ Ο β· Ξ β
Ξ β A [ Ο ] β©β¨ l β© t [ Ο β ] β· B [ Ο β ]
β©α΅β·ββ©Λ’β·ββ©[β]β· β©t β©Ο =
β©β·ββ©β‘β· .projβ $ β©α΅β‘β·ββ©Λ’β‘β·ββ©[β]β‘[β]β· (refl-β©α΅β‘β· β©t) (refl-β©Λ’β‘β· β©Ο)
opaque
β©α΅β‘ββ©Λ’β‘β·ββ©[ββ]β‘[ββ] :
Ξ β A β B β©α΅β¨ l β© Cβ β‘ Cβ β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β A [ Οβ ] β B [ Οβ β ] β©β¨ l β© Cβ [ Οβ β β ] β‘ Cβ [ Οβ β β ]
β©α΅β‘ββ©Λ’β‘β·ββ©[ββ]β‘[ββ] Cββ‘Cβ Οββ‘Οβ =
case wf-β-β©α΅ (wf-β©α΅β‘ Cββ‘Cβ .projβ) of Ξ»
(_ , β©B) β
β©α΅β‘β .projβ Cββ‘Cβ .projβ $
β©Λ’β‘β·-liftSubst β©B $ β©Λ’β‘β·-liftSubst (wf-β-β©α΅ β©B .projβ) Οββ‘Οβ
opaque
β©α΅ββ©Λ’β·ββ©[ββ] :
Ξ β A β B β©α΅β¨ l β© C β
Ξ β©Λ’ Ο β· Ξ β
Ξ β A [ Ο ] β B [ Ο β ] β©β¨ l β© C [ Ο β β ]
β©α΅ββ©Λ’β·ββ©[ββ] β©C β©Ο =
β©ββ©β‘ .projβ $ β©α΅β‘ββ©Λ’β‘β·ββ©[ββ]β‘[ββ] (refl-β©α΅β‘ β©C) (refl-β©Λ’β‘β· β©Ο)
opaque
β©α΅β‘β·ββ©Λ’β‘β·ββ©[ββ]β‘[ββ]β· :
Ξ β A β B β©α΅β¨ l β© tβ β‘ tβ β· C β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β A [ Οβ ] β B [ Οβ β ] β©β¨ l β© tβ [ Οβ β β ] β‘ tβ [ Οβ β β ] β·
C [ Οβ β β ]
β©α΅β‘β·ββ©Λ’β‘β·ββ©[ββ]β‘[ββ]β· tββ‘tβ Οββ‘Οβ =
case wf-β-β©α΅ (wf-β©α΅β· (wf-β©α΅β‘β· tββ‘tβ .projβ)) of Ξ»
(_ , β©B) β
β©α΅β‘β·β .projβ tββ‘tβ .projβ $
β©Λ’β‘β·-liftSubst β©B $ β©Λ’β‘β·-liftSubst (wf-β-β©α΅ β©B .projβ) Οββ‘Οβ
opaque
β©α΅β·ββ©Λ’β·ββ©[ββ]β· :
Ξ β A β B β©α΅β¨ l β© t β· C β
Ξ β©Λ’ Ο β· Ξ β
Ξ β A [ Ο ] β B [ Ο β ] β©β¨ l β© t [ Ο β β ] β· C [ Ο β β ]
β©α΅β·ββ©Λ’β·ββ©[ββ]β· β©t β©Ο =
β©β·ββ©β‘β· .projβ $ β©α΅β‘β·ββ©Λ’β‘β·ββ©[ββ]β‘[ββ]β· (refl-β©α΅β‘β· β©t) (refl-β©Λ’β‘β· β©Ο)
opaque
β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©[β][]ββ‘[β][]β :
Ξ β A β©α΅β¨ l β© Bβ β‘ Bβ β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©β¨ lβ² β© tβ β‘ tβ β· A [ Οβ ] β
Ξ β©β¨ l β© Bβ [ Οβ β ] [ tβ ]β β‘ Bβ [ Οβ β ] [ tβ ]β
β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©[β][]ββ‘[β][]β {Bβ} {Bβ} Bββ‘Bβ Οββ‘Οβ tββ‘tβ =
PE.substβ (_β©β¨_β©_β‘_ _ _)
(PE.sym $ singleSubstComp _ _ Bβ)
(PE.sym $ singleSubstComp _ _ Bβ) $
β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©[,]β‘[,] Bββ‘Bβ Οββ‘Οβ tββ‘tβ
opaque
β©α΅ββ©Λ’β·ββ©β·ββ©[β][]β :
Ξ β A β©α΅β¨ l β© B β
Ξ β©Λ’ Ο β· Ξ β
Ξ β©β¨ lβ² β© t β· A [ Ο ] β
Ξ β©β¨ l β© B [ Ο β ] [ t ]β
β©α΅ββ©Λ’β·ββ©β·ββ©[β][]β β©B β©Ο β©t =
β©ββ©β‘ .projβ $
β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©[β][]ββ‘[β][]β (refl-β©α΅β‘ β©B) (refl-β©Λ’β‘β· β©Ο)
(refl-β©β‘β· β©t)
opaque
β©α΅β‘β·ββ©Λ’β‘β·ββ©β‘β·ββ©[β][]ββ‘[β][]ββ· :
Ξ β A β©α΅β¨ l β© tβ β‘ tβ β· B β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©β¨ lβ² β© uβ β‘ uβ β· A [ Οβ ] β
Ξ β©β¨ l β© tβ [ Οβ β ] [ uβ ]β β‘ tβ [ Οβ β ] [ uβ ]β β·
B [ Οβ β ] [ uβ ]β
β©α΅β‘β·ββ©Λ’β‘β·ββ©β‘β·ββ©[β][]ββ‘[β][]ββ· {tβ} {tβ} {B} tββ‘tβ Οββ‘Οβ uββ‘uβ =
PE.substβ (_β©β¨_β©_β‘_β·_ _ _)
(PE.sym $ singleSubstComp _ _ tβ)
(PE.sym $ singleSubstComp _ _ tβ)
(PE.sym $ singleSubstComp _ _ B) $
β©α΅β‘β·ββ©Λ’β‘β·ββ©β‘β·ββ©[,]β‘[,]β· tββ‘tβ Οββ‘Οβ uββ‘uβ
opaque
β©α΅β·ββ©Λ’β·ββ©β·ββ©[β][]ββ· :
Ξ β A β©α΅β¨ l β© t β· B β
Ξ β©Λ’ Ο β· Ξ β
Ξ β©β¨ lβ² β© u β· A [ Ο ] β
Ξ β©β¨ l β© t [ Ο β ] [ u ]β β· B [ Ο β ] [ u ]β
β©α΅β·ββ©Λ’β·ββ©β·ββ©[β][]ββ· β©t β©Ο β©u =
β©β·ββ©β‘β· .projβ $
β©α΅β‘β·ββ©Λ’β‘β·ββ©β‘β·ββ©[β][]ββ‘[β][]ββ· (refl-β©α΅β‘β· β©t) (refl-β©Λ’β‘β· β©Ο)
(refl-β©β‘β· β©u)
opaque
β©α΅β‘ββ©β‘β·ββ©Λ’β‘β·ββ©[]β[]β‘[]β[] :
Ξ β A β©α΅β¨ l β© Bβ β‘ Bβ β
Ξ β©β¨ lβ² β© tβ [ Οβ ] β‘ tβ [ Οβ ] β· A [ Οβ ] β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©β¨ l β© Bβ [ tβ ]β [ Οβ ] β‘ Bβ [ tβ ]β [ Οβ ]
β©α΅β‘ββ©β‘β·ββ©Λ’β‘β·ββ©[]β[]β‘[]β[] {Bβ} {Bβ} Bββ‘Bβ tβ[Οβ]β‘tβ[Οβ] Οββ‘Οβ =
PE.substβ (_β©β¨_β©_β‘_ _ _)
(PE.sym $ singleSubstLift Bβ _)
(PE.sym $ singleSubstLift Bβ _) $
β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©[β][]ββ‘[β][]β Bββ‘Bβ Οββ‘Οβ tβ[Οβ]β‘tβ[Οβ]
opaque
β©α΅ββ©β·ββ©Λ’β·ββ©[]β[] :
Ξ β A β©α΅β¨ l β© B β
Ξ β©β¨ lβ² β© t [ Ο ] β· A [ Ο ] β
Ξ β©Λ’ Ο β· Ξ β
Ξ β©β¨ l β© B [ t ]β [ Ο ]
β©α΅ββ©β·ββ©Λ’β·ββ©[]β[] {t} β©B β©t[Ο] β©Ο =
β©ββ©β‘ .projβ $
β©α΅β‘ββ©β‘β·ββ©Λ’β‘β·ββ©[]β[]β‘[]β[] {tβ = t} (refl-β©α΅β‘ β©B) (refl-β©β‘β· β©t[Ο])
(refl-β©Λ’β‘β· β©Ο)
opaque
β©α΅β‘β·ββ©β‘β·ββ©Λ’β‘β·ββ©[]β[]β‘[]β[]β· :
Ξ β A β©α΅β¨ l β© tβ β‘ tβ β· B β
Ξ β©β¨ lβ² β© uβ [ Οβ ] β‘ uβ [ Οβ ] β· A [ Οβ ] β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©β¨ l β© tβ [ uβ ]β [ Οβ ] β‘ tβ [ uβ ]β [ Οβ ] β· B [ uβ ]β [ Οβ ]
β©α΅β‘β·ββ©β‘β·ββ©Λ’β‘β·ββ©[]β[]β‘[]β[]β· {tβ} {tβ} {B} tββ‘tβ Οββ‘Οβ uβ[Οβ]β‘uβ[Οβ] =
PE.substβ (_β©β¨_β©_β‘_β·_ _ _) (PE.sym $ singleSubstLift tβ _)
(PE.sym $ singleSubstLift tβ _) (PE.sym $ singleSubstLift B _) $
β©α΅β‘β·ββ©Λ’β‘β·ββ©β‘β·ββ©[β][]ββ‘[β][]ββ· tββ‘tβ uβ[Οβ]β‘uβ[Οβ] Οββ‘Οβ
opaque
β©α΅β·ββ©β·ββ©Λ’β·ββ©[]β[]β· :
Ξ β A β©α΅β¨ l β© t β· B β
Ξ β©β¨ lβ² β© u [ Ο ] β· A [ Ο ] β
Ξ β©Λ’ Ο β· Ξ β
Ξ β©β¨ l β© t [ u ]β [ Ο ] β· B [ u ]β [ Ο ]
β©α΅β·ββ©β·ββ©Λ’β·ββ©[]β[]β· {u} β©t β©u[Ο] β©Ο =
β©β·ββ©β‘β· .projβ $
β©α΅β‘β·ββ©β‘β·ββ©Λ’β‘β·ββ©[]β[]β‘[]β[]β· {uβ = u} (refl-β©α΅β‘β· β©t) (refl-β©β‘β· β©u[Ο])
(refl-β©Λ’β‘β· β©Ο)
opaque
β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©β‘β·ββ©[ββ][]βββ‘[ββ][]ββ :
Ξ β A β B β©α΅β¨ l β© Cβ β‘ Cβ β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©β¨ lβ² β© tβ β‘ tβ β· A [ Οβ ] β
Ξ β©β¨ lβ³ β© uβ β‘ uβ β· B [ Οβ β ] [ tβ ]β β
Ξ β©β¨ l β© Cβ [ Οβ β β ] [ tβ , uβ ]ββ β‘ Cβ [ Οβ β β ] [ tβ , uβ ]ββ
β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©β‘β·ββ©[ββ][]βββ‘[ββ][]ββ
{B} {Cβ} {Cβ} Cββ‘Cβ Οββ‘Οβ tββ‘tβ uββ‘uβ =
PE.substβ (_β©β¨_β©_β‘_ _ _)
(PE.sym $ doubleSubstComp Cβ _ _ _)
(PE.sym $ doubleSubstComp Cβ _ _ _) $
β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©[,]β‘[,] Cββ‘Cβ
(β©Λ’β‘β·βββ² .projβ
( wf-β-β©α΅ (wf-β-β©α΅ (wf-β©α΅β‘ Cββ‘Cβ .projβ) .projβ)
, (_ , tββ‘tβ)
, Οββ‘Οβ
)) $
PE.subst (_β©β¨_β©_β‘_β·_ _ _ _ _) (singleSubstComp _ _ B) uββ‘uβ
opaque
β©α΅ββ©Λ’β·ββ©β·ββ©[ββ][]ββ :
Ξ β A β B β©α΅β¨ l β© C β
Ξ β©Λ’ Ο β· Ξ β
Ξ β©β¨ lβ² β© t β· A [ Ο ] β
Ξ β©β¨ lβ³ β© u β· B [ Ο β ] [ t ]β β
Ξ β©β¨ l β© C [ Ο β β ] [ t , u ]ββ
β©α΅ββ©Λ’β·ββ©β·ββ©[ββ][]ββ β©C β©Ο β©t β©u =
β©ββ©β‘ .projβ $
β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©β‘β·ββ©[ββ][]βββ‘[ββ][]ββ (refl-β©α΅β‘ β©C) (refl-β©Λ’β‘β· β©Ο)
(refl-β©β‘β· β©t) (refl-β©β‘β· β©u)
opaque
β©α΅β‘β·ββ©Λ’β‘β·ββ©β‘β·ββ©β‘β·ββ©[ββ][]βββ‘[ββ][]βββ· :
Ξ β A β B β©α΅β¨ l β© tβ β‘ tβ β· C β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©β¨ lβ² β© uβ β‘ uβ β· A [ Οβ ] β
Ξ β©β¨ lβ³ β© vβ β‘ vβ β· B [ Οβ β ] [ uβ ]β β
Ξ β©β¨ l β© tβ [ Οβ β β ] [ uβ , vβ ]ββ β‘ tβ [ Οβ β β ] [ uβ , vβ ]ββ β·
C [ Οβ β β ] [ uβ , vβ ]ββ
β©α΅β‘β·ββ©Λ’β‘β·ββ©β‘β·ββ©β‘β·ββ©[ββ][]βββ‘[ββ][]βββ·
{B} {tβ} {tβ} {C} tββ‘tβ Οββ‘Οβ uββ‘uβ vββ‘vβ =
case wf-β-β©α΅ (wf-β©α΅β· (wf-β©α΅β‘β· tββ‘tβ .projβ)) of Ξ»
(_ , β©B) β
PE.substβ (_β©β¨_β©_β‘_β·_ _ _)
(PE.sym $ doubleSubstComp tβ _ _ _)
(PE.sym $ doubleSubstComp tβ _ _ _)
(PE.sym $ doubleSubstComp C _ _ _) $
β©α΅β‘β·β .projβ tββ‘tβ .projβ $
β©Λ’β‘β·βββ² .projβ
( (_ , β©B)
, ( _
, PE.subst (_β©β¨_β©_β‘_β·_ _ _ _ _) (singleSubstComp _ _ B) vββ‘vβ
)
, β©Λ’β‘β·βββ² .projβ (wf-β-β©α΅ β©B , (_ , uββ‘uβ) , Οββ‘Οβ)
)
opaque
β©α΅β·ββ©Λ’β·ββ©β·ββ©β·ββ©[ββ][]βββ· :
Ξ β A β B β©α΅β¨ l β© t β· C β
Ξ β©Λ’ Ο β· Ξ β
Ξ β©β¨ lβ² β© u β· A [ Ο ] β
Ξ β©β¨ lβ³ β© v β· B [ Ο β ] [ u ]β β
Ξ β©β¨ l β© t [ Ο β β ] [ u , v ]ββ β· C [ Ο β β ] [ u , v ]ββ
β©α΅β·ββ©Λ’β·ββ©β·ββ©β·ββ©[ββ][]βββ· β©t β©Ο β©u β©v =
β©β·ββ©β‘β· .projβ $
β©α΅β‘β·ββ©Λ’β‘β·ββ©β‘β·ββ©β‘β·ββ©[ββ][]βββ‘[ββ][]βββ· (refl-β©α΅β‘β· β©t) (refl-β©Λ’β‘β· β©Ο)
(refl-β©β‘β· β©u) (refl-β©β‘β· β©v)
opaque
β©α΅β‘ββ©β‘β·ββ©β‘β·ββ©Λ’β‘β·ββ©[]ββ[]β‘[]ββ[] :
Ξ β A β B β©α΅β¨ l β© Cβ β‘ Cβ β
Ξ β©β¨ lβ² β© tβ [ Οβ ] β‘ tβ [ Οβ ] β· A [ Οβ ] β
Ξ β©β¨ lβ³ β© uβ [ Οβ ] β‘ uβ [ Οβ ] β· B [ tβ ]β [ Οβ ] β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©β¨ l β© Cβ [ tβ , uβ ]ββ [ Οβ ] β‘ Cβ [ tβ , uβ ]ββ [ Οβ ]
β©α΅β‘ββ©β‘β·ββ©β‘β·ββ©Λ’β‘β·ββ©[]ββ[]β‘[]ββ[]
{B} {Cβ} {Cβ} Cββ‘Cβ tβ[Οβ]β‘tβ[Οβ] uβ[Οβ]β‘uβ[Οβ] Οββ‘Οβ =
PE.substβ (_β©β¨_β©_β‘_ _ _)
(PE.sym $ [,]-[]-commute Cβ)
(PE.sym $ [,]-[]-commute Cβ) $
β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©β‘β·ββ©[ββ][]βββ‘[ββ][]ββ Cββ‘Cβ Οββ‘Οβ tβ[Οβ]β‘tβ[Οβ]
(PE.subst (_β©β¨_β©_β‘_β·_ _ _ _ _) (singleSubstLift B _)
uβ[Οβ]β‘uβ[Οβ])
opaque
β©α΅ββ©β·ββ©β·ββ©Λ’β·ββ©[]ββ[] :
Ξ β A β B β©α΅β¨ l β© C β
Ξ β©β¨ lβ² β© t [ Ο ] β· A [ Ο ] β
Ξ β©β¨ lβ³ β© u [ Ο ] β· B [ t ]β [ Ο ] β
Ξ β©Λ’ Ο β· Ξ β
Ξ β©β¨ l β© C [ t , u ]ββ [ Ο ]
β©α΅ββ©β·ββ©β·ββ©Λ’β·ββ©[]ββ[] {t} {u} β©C β©t[Ο] β©u[Ο] β©Ο =
β©ββ©β‘ .projβ $
β©α΅β‘ββ©β‘β·ββ©β‘β·ββ©Λ’β‘β·ββ©[]ββ[]β‘[]ββ[] {tβ = t} {uβ = u} (refl-β©α΅β‘ β©C)
(refl-β©β‘β· β©t[Ο]) (refl-β©β‘β· β©u[Ο]) (refl-β©Λ’β‘β· β©Ο)
opaque
β©α΅β‘β·ββ©β‘β·ββ©β‘β·ββ©Λ’β‘β·ββ©[]ββ[]β‘[]ββ[]β· :
Ξ β A β B β©α΅β¨ l β© tβ β‘ tβ β· C β
Ξ β©β¨ lβ² β© uβ [ Οβ ] β‘ uβ [ Οβ ] β· A [ Οβ ] β
Ξ β©β¨ lβ³ β© vβ [ Οβ ] β‘ vβ [ Οβ ] β· B [ uβ ]β [ Οβ ] β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©β¨ l β© tβ [ uβ , vβ ]ββ [ Οβ ] β‘ tβ [ uβ , vβ ]ββ [ Οβ ] β·
C [ uβ , vβ ]ββ [ Οβ ]
β©α΅β‘β·ββ©β‘β·ββ©β‘β·ββ©Λ’β‘β·ββ©[]ββ[]β‘[]ββ[]β·
{B} {tβ} {tβ} {C} tββ‘tβ uβ[Οβ]β‘uβ[Οβ] vβ[Οβ]β‘vβ[Οβ] Οββ‘Οβ =
PE.substβ (_β©β¨_β©_β‘_β·_ _ _) (PE.sym $ [,]-[]-commute tβ)
(PE.sym $ [,]-[]-commute tβ) (PE.sym $ [,]-[]-commute C) $
β©α΅β‘β·ββ©Λ’β‘β·ββ©β‘β·ββ©β‘β·ββ©[ββ][]βββ‘[ββ][]βββ· tββ‘tβ Οββ‘Οβ uβ[Οβ]β‘uβ[Οβ]
(PE.subst (_β©β¨_β©_β‘_β·_ _ _ _ _) (singleSubstLift B _)
vβ[Οβ]β‘vβ[Οβ])
opaque
β©α΅β·ββ©β·ββ©β·ββ©Λ’β·ββ©[]ββ[]β· :
Ξ β A β B β©α΅β¨ l β© t β· C β
Ξ β©β¨ lβ² β© u [ Ο ] β· A [ Ο ] β
Ξ β©β¨ lβ³ β© v [ Ο ] β· B [ u ]β [ Ο ] β
Ξ β©Λ’ Ο β· Ξ β
Ξ β©β¨ l β© t [ u , v ]ββ [ Ο ] β· C [ u , v ]ββ [ Ο ]
β©α΅β·ββ©β·ββ©β·ββ©Λ’β·ββ©[]ββ[]β· {u} {v} β©t β©u[Ο] β©v[Ο] β©Ο =
β©β·ββ©β‘β· .projβ $
β©α΅β‘β·ββ©β‘β·ββ©β‘β·ββ©Λ’β‘β·ββ©[]ββ[]β‘[]ββ[]β· {uβ = u} {vβ = v} (refl-β©α΅β‘β· β©t)
(refl-β©β‘β· β©u[Ο]) (refl-β©β‘β· β©v[Ο]) (refl-β©Λ’β‘β· β©Ο)