open import Definition.Typed.Restrictions
open import Graded.Modality
module Definition.Typed.EqualityRelation
{β} {M : Set β}
{π : Modality M}
(R : Type-restrictions π)
where
open Type-restrictions R
open import Definition.Untyped M
open import Definition.Untyped.Neutral M type-variant
open import Definition.Typed R hiding (_,_)
open import Definition.Typed.Weakening R using (_β·_β_)
import Graded.Derived.Erased.Untyped π as Erased
open import Tools.Fin
open import Tools.Function
open import Tools.Level
open import Tools.Nat
open import Tools.Relation
private
variable
p q qβ² r : M
n nβ² : Nat
Ξ : Con Term n
Ξ : Con Term nβ²
Ο : Wk nβ² n
A Aβ Aβ Aβ² B Bβ Bβ Bβ² C : Term n
a aβ² b bβ² e eβ² : Term n
k l m t tβ tβ u uβ uβ v vβ vβ wβ wβ : Term n
s : Strength
bm : BinderMode
record EqRelSet : Set (lsuc β) where
constructor eqRel
field
_β’_β
_ : Con Term n β (A B : Term n) β Set β
_β’_β
_β·_ : Con Term n β (t u A : Term n) β Set β
_β’_~_β·_ : Con Term n β (t u A : Term n) β Set β
~-to-β
β : Ξ β’ k ~ l β· A
β Ξ β’ k β
l β· A
β
-eq : Ξ β’ A β
B
β Ξ β’ A β‘ B
β
β-eq : Ξ β’ t β
u β· A
β Ξ β’ t β‘ u β· A
β
-univ : Ξ β’ A β
B β· U
β Ξ β’ A β
B
β
-sym : Ξ β’ A β
B β Ξ β’ B β
A
β
β-sym : Ξ β’ t β
u β· A β Ξ β’ u β
t β· A
~-sym : Ξ β’ k ~ l β· A β Ξ β’ l ~ k β· A
β
-trans : Ξ β’ A β
B β Ξ β’ B β
C β Ξ β’ A β
C
β
β-trans : Ξ β’ t β
u β· A β Ξ β’ u β
v β· A β Ξ β’ t β
v β· A
~-trans : Ξ β’ k ~ l β· A β Ξ β’ l ~ m β· A β Ξ β’ k ~ m β· A
β
-conv : Ξ β’ t β
u β· A β Ξ β’ A β‘ B β Ξ β’ t β
u β· B
~-conv : Ξ β’ k ~ l β· A β Ξ β’ A β‘ B β Ξ β’ k ~ l β· B
β
-wk : Ο β· Ξ β Ξ
β β’ Ξ
β Ξ β’ A β
B
β Ξ β’ wk Ο A β
wk Ο B
β
β-wk : Ο β· Ξ β Ξ
β β’ Ξ
β Ξ β’ t β
u β· A
β Ξ β’ wk Ο t β
wk Ο u β· wk Ο A
~-wk : Ο β· Ξ β Ξ
β β’ Ξ
β Ξ β’ k ~ l β· A
β Ξ β’ wk Ο k ~ wk Ο l β· wk Ο A
β
-red : Ξ β’ A β Aβ²
β Ξ β’ B β Bβ²
β Ξ β’ Aβ² β
Bβ²
β Ξ β’ A β
B
β
β-red : Ξ β’ A β B
β Ξ β’ a β aβ² β· B
β Ξ β’ b β bβ² β· B
β Ξ β’ aβ² β
bβ² β· B
β Ξ β’ a β
b β· A
β
-Urefl : β’ Ξ β Ξ β’ U β
U
β
β-βrefl : β’ Ξ β Ξ β’ β β
β β· U
β
β-Emptyrefl : β’ Ξ β Ξ β’ Empty β
Empty β· U
β
β-Unitrefl : β’ Ξ β Unit-allowed s β Ξ β’ Unit s β
Unit s β· U
β
β-Ξ·-unit : Ξ β’ e β· Unit s
β Ξ β’ eβ² β· Unit s
β Unit-with-Ξ· s
β Ξ β’ e β
eβ² β· Unit s
β
-Ξ Ξ£-cong : β {F G H E}
β Ξ β’ F
β Ξ β’ F β
H
β Ξ β F β’ G β
E
β Ξ Ξ£-allowed bm p q
β Ξ β’ Ξ Ξ£β¨ bm β© p , q β· F βΉ G β
Ξ Ξ£β¨ bm β© p , q β· H βΉ E
β
β-Ξ Ξ£-cong
: β {F G H E}
β Ξ β’ F
β Ξ β’ F β
H β· U
β Ξ β F β’ G β
E β· U
β Ξ Ξ£-allowed bm p q
β Ξ β’ Ξ Ξ£β¨ bm β© p , q β· F βΉ G β
Ξ Ξ£β¨ bm β© p , q β· H βΉ E β· U
β
β-zerorefl : β’ Ξ β Ξ β’ zero β
zero β· β
β
-suc-cong : β {m n} β Ξ β’ m β
n β· β β Ξ β’ suc m β
suc n β· β
β
-prod-cong : β {F G t tβ² u uβ²}
β Ξ β’ F
β Ξ β F β’ G
β Ξ β’ t β
tβ² β· F
β Ξ β’ u β
uβ² β· G [ t ]β
β Ξ£Κ·-allowed p q
β Ξ β’ prodΚ· p t u β
prodΚ· p tβ² uβ² β· Ξ£Κ· p , q β· F βΉ G
β
-Ξ·-eq : β {f g F G}
β Ξ β’ F
β Ξ β’ f β· Ξ p , q β· F βΉ G
β Ξ β’ g β· Ξ p , q β· F βΉ G
β Function f
β Function g
β Ξ β F β’ wk1 f ββ¨ p β© var x0 β
wk1 g ββ¨ p β© var x0 β· G
β Ξ β’ f β
g β· Ξ p , q β· F βΉ G
β
-Ξ£-Ξ· : β {r s F G}
β Ξ β’ F
β Ξ β F β’ G
β Ξ β’ r β· Ξ£Λ’ p , q β· F βΉ G
β Ξ β’ s β· Ξ£Λ’ p , q β· F βΉ G
β Product r
β Product s
β Ξ β’ fst p r β
fst p s β· F
β Ξ β’ snd p r β
snd p s β· G [ fst p r ]β
β Ξ β’ r β
s β· Ξ£Λ’ p , q β· F βΉ G
~-var : β {x A} β Ξ β’ var x β· A β Ξ β’ var x ~ var x β· A
~-app : β {a b f g F G}
β Ξ β’ f ~ g β· Ξ p , q β· F βΉ G
β Ξ β’ a β
b β· F
β Ξ β’ f ββ¨ p β© a ~ g ββ¨ p β© b β· G [ a ]β
~-fst : β {r s F G}
β Ξ β’ F
β Ξ β F β’ G
β Ξ β’ r ~ s β· Ξ£Λ’ p , q β· F βΉ G
β Ξ β’ fst p r ~ fst p s β· F
~-snd : β {r s F G}
β Ξ β’ F
β Ξ β F β’ G
β Ξ β’ r ~ s β· Ξ£Λ’ p , q β· F βΉ G
β Ξ β’ snd p r ~ snd p s β· G [ fst p r ]β
~-natrec : β {z zβ² s sβ² n nβ² F Fβ²}
β Ξ β β β’ F
β Ξ β β β’ F β
Fβ²
β Ξ β’ z β
zβ² β· F [ zero ]β
β Ξ β β β F β’ s β
sβ² β· F [ suc (var x1) ]βΒ²
β Ξ β’ n ~ nβ² β· β
β Ξ β’ natrec p q r F z s n ~ natrec p q r Fβ² zβ² sβ² nβ² β· F [ n ]β
~-prodrec : β {F G A Aβ² t tβ² u uβ²}
β Ξ β’ F
β Ξ β F β’ G
β Ξ β (Ξ£Κ· p , q β· F βΉ G) β’ A β
Aβ²
β Ξ β’ t ~ tβ² β· Ξ£Κ· p , q β· F βΉ G
β Ξ β F β G β’ u β
uβ² β· A [ prodΚ· p (var x1) (var x0) ]βΒ²
β Ξ£Κ·-allowed p q
β Ξ β’ prodrec r p qβ² A t u ~ prodrec r p qβ² Aβ² tβ² uβ² β· A [ t ]β
~-emptyrec : β {n nβ² F Fβ²}
β Ξ β’ F β
Fβ²
β Ξ β’ n ~ nβ² β· Empty
β Ξ β’ emptyrec p F n ~ emptyrec p Fβ² nβ² β· F
~-unitrec : β {A Aβ² t tβ² u uβ²}
β Ξ β UnitΚ· β’ A β
Aβ²
β Ξ β’ t ~ tβ² β· UnitΚ·
β Ξ β’ u β
uβ² β· A [ starΚ· ]β
β UnitΚ·-allowed
β Β¬ UnitΚ·-Ξ·
β Ξ β’ unitrec p q A t u ~ unitrec p q Aβ² tβ² uβ² β· A [ t ]β
β
β-starrefl : β’ Ξ β Unit-allowed s β Ξ β’ star s β
star s β· Unit s
β
-Id-cong
: Ξ β’ Aβ β
Aβ
β Ξ β’ tβ β
tβ β· Aβ
β Ξ β’ uβ β
uβ β· Aβ
β Ξ β’ Id Aβ tβ uβ β
Id Aβ tβ uβ
β
β-Id-cong
: Ξ β’ Aβ β
Aβ β· U
β Ξ β’ tβ β
tβ β· Aβ
β Ξ β’ uβ β
uβ β· Aβ
β Ξ β’ Id Aβ tβ uβ β
Id Aβ tβ uβ β· U
β
β-rflrefl : Ξ β’ t β· A β Ξ β’ rfl β
rfl β· Id A t t
~-J
: Ξ β’ Aβ
β Ξ β’ Aβ β
Aβ
β Ξ β’ tβ β· Aβ
β Ξ β’ tβ β
tβ β· Aβ
β Ξ β Aβ β Id (wk1 Aβ) (wk1 tβ) (var x0) β’ Bβ β
Bβ
β Ξ β’ uβ β
uβ β· Bβ [ tβ , rfl ]ββ
β Ξ β’ vβ β
vβ β· Aβ
β Ξ β’ wβ ~ wβ β· Id Aβ tβ vβ
β Ξ β’ J p q Aβ tβ Bβ uβ vβ wβ ~ J p q Aβ tβ Bβ uβ vβ wβ β·
Bβ [ vβ , wβ ]ββ
~-K
: Ξ β’ Aβ β
Aβ
β Ξ β’ tβ β· Aβ
β Ξ β’ tβ β
tβ β· Aβ
β Ξ β Id Aβ tβ tβ β’ Bβ β
Bβ
β Ξ β’ uβ β
uβ β· Bβ [ rfl ]β
β Ξ β’ vβ ~ vβ β· Id Aβ tβ tβ
β K-allowed
β Ξ β’ K p Aβ tβ Bβ uβ vβ ~ K p Aβ tβ Bβ uβ vβ β· Bβ [ vβ ]β
~-[]-cong
: Ξ β’ Aβ β
Aβ
β Ξ β’ tβ β
tβ β· Aβ
β Ξ β’ uβ β
uβ β· Aβ
β Ξ β’ vβ ~ vβ β· Id Aβ tβ uβ
β []-cong-allowed s
β let open Erased s in
Ξ β’ []-cong s Aβ tβ uβ vβ ~ []-cong s Aβ tβ uβ vβ β·
Id (Erased Aβ) ([ tβ ]) ([ uβ ])
~-to-β
: β {k l} β Ξ β’ k ~ l β· U β Ξ β’ k β
l
~-to-β
k~l = β
-univ (~-to-β
β k~l)
opaque
β
-βrefl : β’ Ξ β Ξ β’ β β
β
β
-βrefl = β
-univ ββ β
β-βrefl
opaque
β
-Emptyrefl : β’ Ξ β Ξ β’ Empty β
Empty
β
-Emptyrefl = β
-univ ββ β
β-Emptyrefl
opaque
β
-Unitrefl : β’ Ξ β Unit-allowed s β Ξ β’ Unit s β
Unit s
β
-Unitrefl β’Ξ ok = β
-univ (β
β-Unitrefl β’Ξ ok)