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
import Definition.Untyped.Erased π as Erased
open import Definition.Untyped.Neutral M type-variant
open import Definition.Typed R
open import Definition.Typed.Weakening R using (_β·Κ·_β_)
open import Tools.Fin
open import Tools.Function
open import Tools.Level hiding (_β_)
open import Tools.Nat
open import Tools.Product
import Tools.PropositionalEquality as PE
open import Tools.Relation
private
variable
p q qβ² r : M
n nβ² l lβ lβ : 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
m t tβ tβ u uβ uβ v vβ vβ wβ wβ : Term n
s : Strength
bm : BinderMode
record Equality-relations
(_β’_β
_ : β {n} β Con Term n β (_ _ : Term n) β Set β)
(_β’_β
_β·_ : β {n} β Con Term n β (_ _ _ : Term n) β Set β)
(_β’_~_β·_ : β {n} β Con Term n β (t u A : Term n) β Set β)
(Neutrals-included : Set β) :
Set β where
no-eta-equality
_β’β
_ : Con Term n β Term n β Set β
Ξ β’β
A = Ξ β’ A β
A
_β’β
_β·_ : Con Term n β Term n β Term n β Set β
Ξ β’β
t β· A = Ξ β’ t β
t β· A
_β’~_β·_ : Con Term n β Term n β Term n β Set β
Ξ β’~ t β· A = Ξ β’ t ~ t β· A
field
Neutrals-included? : Dec Neutrals-included
Equality-reflection-allowedβΒ¬Neutrals-included :
Equality-reflection β Β¬ Neutrals-included
β’β‘ββ’β
:
Β¬ Neutrals-included β
Ξ β’ A β‘ B β Ξ β’ A β
B
β’β‘β·ββ’β
β· :
Β¬ Neutrals-included β
Ξ β’ t β‘ u β· A β Ξ β’ t β
u β· A
~-to-β
β : Ξ β’ t ~ u β· A
β Ξ β’ t β
u β· A
β
-eq : Ξ β’ A β
B
β Ξ β’ A β‘ B
β
β-eq : Ξ β’ t β
u β· A
β Ξ β’ t β‘ u β· A
β
-univ : Ξ β’ A β
B β· U l
β Ξ β’ A β
B
β
-sym : Ξ β’ A β
B β Ξ β’ B β
A
β
β-sym : Ξ β’ t β
u β· A β Ξ β’ u β
t β· A
~-sym : Ξ β’ t ~ u β· A β Ξ β’ u ~ t β· A
β
-trans : Ξ β’ A β
B β Ξ β’ B β
C β Ξ β’ A β
C
β
β-trans : Ξ β’ t β
u β· A β Ξ β’ u β
v β· A β Ξ β’ t β
v β· A
~-trans : Ξ β’ t ~ u β· A β Ξ β’ u ~ v β· A β Ξ β’ t ~ v β· A
β
-conv : Ξ β’ t β
u β· A β Ξ β’ A β‘ B β Ξ β’ t β
u β· B
~-conv : Ξ β’ t ~ u β· A β Ξ β’ A β‘ B β Ξ β’ t ~ u β· B
β
-wk : Ο β·Κ· Ξ β Ξ
β Ξ β’ A β
B
β Ξ β’ wk Ο A β
wk Ο B
β
β-wk : Ο β·Κ· Ξ β Ξ
β Ξ β’ t β
u β· A
β Ξ β’ wk Ο t β
wk Ο u β· wk Ο A
~-wk : Ο β·Κ· Ξ β Ξ
β Ξ β’ t ~ u β· A
β Ξ β’ wk Ο t ~ wk Ο u β· 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 l β· U (1+ l)
β
β-βrefl : β’ Ξ β Ξ β’β
β β· U 0
β
β-Emptyrefl : β’ Ξ β Ξ β’β
Empty β· U 0
β
β-Unitrefl : β’ Ξ β Unit-allowed s β Ξ β’β
Unit s l β· U l
β
β-Ξ·-unit : Ξ β’ e β· Unit s l
β Ξ β’ eβ² β· Unit s l
β Unit-with-Ξ· s
β Ξ β’ e β
eβ² β· Unit s l
β
-Ξ Ξ£-cong : β {F G H E}
β Ξ β’ 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 β
H β· U lβ
β Ξ β F β’ G β
E β· U lβ
β Ξ Ξ£-allowed bm p q
β Ξ β’ Ξ Ξ£β¨ bm β© p , q β· F βΉ G β
Ξ Ξ£β¨ bm β© p , q β· H βΉ E β·
U (lβ βα΅ lβ)
β
β-zerorefl : β’ Ξ β Ξ β’β
zero β· β
β
-suc-cong : β {m n} β Ξ β’ m β
n β· β β Ξ β’ suc m β
suc n β· β
β
-prod-cong : β {F G t tβ² u uβ²}
β Ξ β 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 β· Ξ 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}
β Ξ β’ 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 β· 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 β’ G
β Ξ β’ r ~ s β· Ξ£Λ’ p , q β· F βΉ G
β Ξ β’ fst p r ~ fst p s β· F
~-snd : β {r s F G}
β Ξ β 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β²
β Ξ β’ 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β²}
β Ξ β (Ξ£Κ· 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Κ· l β’ A β
Aβ²
β Ξ β’ t ~ tβ² β· UnitΚ· l
β Ξ β’ u β
uβ² β· A [ starΚ· l ]β
β UnitΚ·-allowed
β Β¬ UnitΚ·-Ξ·
β Ξ β’ unitrec l p q A t u ~ unitrec l p q Aβ² tβ² uβ² β·
A [ t ]β
β
β-starrefl :
β’ Ξ β Unit-allowed s β Ξ β’β
star s l β· Unit s l
β
-Id-cong
: Ξ β’ Aβ β
Aβ
β Ξ β’ tβ β
tβ β· Aβ
β Ξ β’ uβ β
uβ β· Aβ
β Ξ β’ Id Aβ tβ uβ β
Id Aβ tβ uβ
β
β-Id-cong
: Ξ β’ Aβ β
Aβ β· U l
β Ξ β’ tβ β
tβ β· Aβ
β Ξ β’ uβ β
uβ β· Aβ
β Ξ β’ Id Aβ tβ uβ β
Id Aβ tβ uβ β· U l
β
β-rflrefl : Ξ β’ t β· A β Ξ β’β
rfl β· Id A t t
~-J
: Ξ β’ 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β β
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 lβ²} β Ξ β’ k ~ l β· U lβ² β Ξ β’ k β
l
~-to-β
k~l = β
-univ (~-to-β
β k~l)
opaque
β
-βrefl : β’ Ξ β Ξ β’β
β
β
-βrefl = β
-univ ββ β
β-βrefl
opaque
β
-Emptyrefl : β’ Ξ β Ξ β’β
Empty
β
-Emptyrefl = β
-univ ββ β
β-Emptyrefl
opaque
β
-Unitrefl : β’ Ξ β Unit-allowed s β Ξ β’β
Unit s l
β
-Unitrefl β’Ξ ok = β
-univ (β
β-Unitrefl β’Ξ ok)
opaque
wf-β’β
: Ξ β’ A β
B β Ξ β’β
A Γ Ξ β’β
B
wf-β’β
Aβ
B =
β
-trans Aβ
B (β
-sym Aβ
B) ,
β
-trans (β
-sym Aβ
B) Aβ
B
opaque
wf-β’β
β· : Ξ β’ t β
u β· A β Ξ β’β
t β· A Γ Ξ β’β
u β· A
wf-β’β
β· tβ
u =
β
β-trans tβ
u (β
β-sym tβ
u) ,
β
β-trans (β
β-sym tβ
u) tβ
u
opaque
wf-β’~β· : Ξ β’ t ~ u β· A β Ξ β’~ t β· A Γ Ξ β’~ u β· A
wf-β’~β· t~u =
~-trans t~u (~-sym t~u) ,
~-trans (~-sym t~u) t~u
opaque
included :
β¦ inc : Neutrals-included β¦ β Neutrals-included or-empty Ξ
included β¦ inc β¦ = possibly-nonempty β¦ ok = inc β¦
opaque
with-inc-β’β
:
Ξ β’ A β‘ B β
(β¦ inc : Neutrals-included β¦ β Ξ β’ A β
B) β
Ξ β’ A β
B
with-inc-β’β
Aβ‘B Aβ
B =
case Neutrals-included? of Ξ» where
(yes inc) β Aβ
B β¦ inc = inc β¦
(no ni) β β’β‘ββ’β
ni Aβ‘B
opaque
with-inc-β’β
β· :
Ξ β’ t β‘ u β· A β
(β¦ inc : Neutrals-included β¦ β Ξ β’ t β
u β· A) β
Ξ β’ t β
u β· A
with-inc-β’β
β· tβ‘u tβ
u =
case Neutrals-included? of Ξ» where
(yes inc) β tβ
u β¦ inc = inc β¦
(no ni) β β’β‘β·ββ’β
β· ni tβ‘u
record EqRelSet : Set (lsuc β) where
no-eta-equality
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 β
Neutrals-included : Set β
equality-relations :
Equality-relations _β’_β
_ _β’_β
_β·_ _β’_~_β·_ Neutrals-included
open Equality-relations equality-relations public