module Section3 where
open import Section1 public
infixr 7 _β_
data π― : Set where
β’ : π―
_β_ : π― β π― β π―
module _ where
injββ : β {A Aβ² B Bβ²} β A β B β‘ Aβ² β Bβ² β A β‘ Aβ²
injββ refl = refl
injββ : β {A Aβ² B Bβ²} β A β B β‘ Aβ² β Bβ² β B β‘ Bβ²
injββ refl = refl
_βπ―_ : (A Aβ² : π―) β Dec (A β‘ Aβ²)
β’ βπ― β’ = yes refl
β’ βπ― (Aβ² β Bβ²) = no Ξ» ()
(A β B) βπ― β’ = no Ξ» ()
(A β B) βπ― (Aβ² β Bβ²) with A βπ― Aβ² | B βπ― Bβ²
β¦ | yes refl | yes refl = yes refl
β¦ | yes refl | no Bβ’Bβ² = no (Ξ» p β injββ p β― Bβ’Bβ²)
β¦ | no Aβ’Aβ² | _ = no (Ξ» p β injββ p β― Aβ’Aβ²)
mutual
data π : Set where
[] : π
[_,_β·_] : (Ξ : π) (x : Name) {{_ : T (fresh x Ξ)}} β π― β π
fresh : Name β π β Bool
fresh x [] = true
fresh x [ Ξ , y β· A ] = and (x β y) (fresh x Ξ)
data _β_β·_ : π β Name β π― β Set where
zero : β {Ξ A x} {{_ : T (fresh x Ξ)}} β
[ Ξ , x β· A ] β x β· A
suc : β {Ξ A B x y} {{_ : T (fresh y Ξ)}} β
Ξ β x β· A β
[ Ξ , y β· B ] β x β· A
module _ where
injsuc : β {Ξ A B x y} {{_ : T (fresh y Ξ)}} {i iβ² : Ξ β x β· A} β
suc {B = B} {y = y} i β‘ suc iβ² β i β‘ iβ²
injsuc refl = refl
_ββ_ : β {Ξ A x} β (i iβ² : Ξ β x β· A) β Dec (i β‘ iβ²)
zero ββ zero = yes refl
zero ββ suc iβ² = no (Ξ» ())
suc i ββ zero = no (Ξ» ())
suc i ββ suc iβ² with i ββ iβ²
β¦ | yes refl = yes refl
β¦ | no iβ’iβ² = no (Ξ» p β injsuc p β― iβ’iβ²)
module _ where
_β_β·_ : π β Name β π― β Set
Ξ β x β· A = Β¬ (Ξ β x β· A)
freshββ : β {x Ξ A} {{_ : T (fresh x Ξ)}} β Ξ β x β· A
freshββ {x} {{Ο}} zero with x β x
freshββ {x} {{()}} zero | yes refl
freshββ {x} {{Ο}} zero | no xβ’x = refl β― xβ’x
freshββ {x} {{Ο}} (suc {y = y} i) with x β y
freshββ {x} {{()}} (suc {y = .x} i) | yes refl
freshββ {x} {{Ο}} (suc {y = y} i) | no xβ’y = i β― freshββ
freshlemβ : β {bβ²} β (x : Name) β Β¬ (T (and (x β x) bβ²))
freshlemβ x p with x β x
β¦ | yes refl = p
β¦ | no xβ’x = refl β― xβ’x
freshlemβ : β {bβ²} β (x {y} : Name) β T (and (x β y) bβ²) β T bβ²
freshlemβ x {y} p with x β y
β¦ | yes refl = elimβ₯ p
β¦ | no xβ’y = p
infix 3 _β_
data _β_ : π β π β Set where
done : β {Ξ} β
Ξ β []
step : β {Ξ Ξ A x} {{_ : T (fresh x Ξ)}} β
Ξ β Ξ β Ξ β x β· A β
Ξ β [ Ξ , x β· A ]
module _ where
injβstep : β {Ξ Ξ A x} {{_ : T (fresh x Ξ)}} {c cβ² : Ξ β Ξ} {i iβ² : Ξ β x β· A} β
step c i β‘ step cβ² iβ² β c β‘ cβ²
injβstep refl = refl
injβstep : β {Ξ Ξ A x} {{_ : T (fresh x Ξ)}} {c cβ² : Ξ β Ξ} {i iβ² : Ξ β x β· A} β
step c i β‘ step cβ² iβ² β i β‘ iβ²
injβstep refl = refl
_ββ_ : β {Ξ Ξ} β (c cβ² : Ξ β Ξ) β Dec (c β‘ cβ²)
done ββ done = yes refl
step c i ββ step cβ² iβ² with c ββ cβ² | i ββ iβ²
β¦ | yes refl | yes refl = yes refl
β¦ | yes refl | no iβ’iβ² = no (Ξ» p β injβstep p β― iβ’iβ²)
β¦ | no cβ’cβ² | _ = no (Ξ» p β injβstep p β― cβ’cβ²)
extβ : β {Ξ Ξ} β (β {A x} β Ξ β x β· A β Ξ β x β· A) β Ξ β Ξ
extβ {[]} f = done
extβ {[ Ξ , x β· A ]} f = step (extβ (Ξ» i β f (suc i))) (f zero)
module _ where
ββ¨_β©β : β {Ξ Ξ A x} β Ξ β Ξ β Ξ β x β· A β Ξ β x β· A
ββ¨ done β©β ()
ββ¨ step c i β©β zero = i
ββ¨ step c i β©β (suc j) = ββ¨ c β©β j
instance
raiseβ : β {A x} β Raiseable (_β x β· A)
raiseβ = record { ββ¨_β© = ββ¨_β©β }
reflβ : β {Ξ} β Ξ β Ξ
reflβ = extβ id
module _ where
_β_ : β {Ξ Ξ Ξ} β Ξ β Ξ β Ξ β Ξ β Ξ β Ξ
c β cβ² = extβ (Ξ» i β ββ¨ cβ² β© (ββ¨ c β© i))
transβ : β {Ξ Ξ Ξ} β Ξ β Ξ β Ξ β Ξ β Ξ β Ξ
transβ = flip _β_
weakβ : β {Ξ A x} {{_ : T (fresh x Ξ)}} β [ Ξ , x β· A ] β Ξ
weakβ = extβ suc
uniqβ : β {Ξ A x} β (i iβ² : Ξ β x β· A) β i β‘ iβ²
uniqβ zero zero = refl
uniqβ zero (suc iβ²) = iβ² β― freshββ
uniqβ (suc i) zero = i β― freshββ
uniqβ (suc i) (suc iβ²) = cong suc (uniqβ i iβ²)
uniqβ : β {Ξ Ξ} β (c cβ² : Ξ β Ξ) β c β‘ cβ²
uniqβ done done = refl
uniqβ (step c i) (step cβ² iβ²) = congΒ² step (uniqβ c cβ²) (uniqβ i iβ²)
module _ where
idββ : β {Ξ Ξ} β (c : Ξ β Ξ) (cβ² : Ξ β Ξ) β c β cβ² β‘ cβ²
idββ c cβ² = uniqβ (c β cβ²) cβ²
idββ : β {Ξ Ξ} β (c : Ξ β Ξ) (cβ² : Ξ β Ξ) β c β cβ² β‘ c
idββ c cβ² = uniqβ (c β cβ²) c
assocβ : β {Ξ Ξ Ξ Ξ©} β (c : Ξ β Ξ) (cβ² : Ξ β Ξ) (cβ³ : Ξ© β Ξ) β
c β (cβ² β cβ³) β‘ (c β cβ²) β cβ³
assocβ c cβ² cβ³ = uniqβ (c β (cβ² β cβ³)) ((c β cβ²) β cβ³)
compβ : β {Ξ Ξ Ξ} β (c : Ξ β Ξ) (cβ² : Ξ β Ξ) (cβ³ : Ξ β Ξ) β
c β cβ² β‘ cβ³
compβ c cβ² cβ³ = uniqβ (c β cβ²) cβ³
mutual
infix 3 _β’_
data _β’_ : π β π― β Set where
Ξ½ : β {Ξ A} β
(x : Name) β Ξ β x β· A β
Ξ β’ A
Ζ : β {Ξ A B} β
(x : Name) {{_ : T (fresh x Ξ)}} β [ Ξ , x β· A ] β’ B β
Ξ β’ A β B
_β_ : β {Ξ A B} β
Ξ β’ A β B β Ξ β’ A β
Ξ β’ B
_βΆ_ : β {Ξ Ξ A} β
Ξ β’ A β Ξ β Ξ β
Ξ β’ A
infix 3 _β_
data _β_ : π β π β Set where
Οβ¨_β© : β {Ξ Ξ} β
Ξ β Ξ β
Ξ β Ξ
_β_ : β {Ξ Ξ Ξ} β
Ξ β Ξ β Ξ β Ξ β
Ξ β Ξ
[_,_β_] : β {Ξ Ξ A} β
Ξ β Ξ β (x : Name) {{_ : T (fresh x Ξ)}} β Ξ β’ A β
Ξ β [ Ξ , x β· A ]
module _ where
ββ¨_β©β’ : β {Ξ Ξ A} β Ξ β Ξ β Ξ β’ A β Ξ β’ A
ββ¨ c β©β’ M = M βΆ Οβ¨ c β©
ββ¨_β©β : β {Ξ Ξ Ξ} β Ξ β Ξ β Ξ β Ξ β Ξ β Ξ
ββ¨ c β©β Ξ΄ = Ξ΄ β Οβ¨ c β©
ββ¨_β©β : β {Ξ Ξ Ξ} β Ξ β Ξ β Ξ β Ξ β Ξ β Ξ
ββ¨ c β©β Ξ΄ = Οβ¨ c β© β Ξ΄
reflβ : β {Ξ} β Ξ β Ξ
reflβ = Οβ¨ reflβ β©
transβ : β {Ξ Ξ Ξ} β Ξ β Ξ β Ξ β Ξ β Ξ β Ξ
transβ = flip _β_
weakβ : β {Ξ A x} {{_ : T (fresh x Ξ)}} β [ Ξ , x β· A ] β Ξ
weakβ = Οβ¨ weakβ β©
instance
raiseβ’ : β {A} β Raiseable (_β’ A)
raiseβ’ = record { ββ¨_β© = ββ¨_β©β’ }
raiseβ : β {Ξ} β Raiseable (_β Ξ)
raiseβ = record { ββ¨_β© = ββ¨_β©β }
lowerβ : β {Ξ} β Lowerable (Ξ β_)
lowerβ = record { ββ¨_β© = ββ¨_β©β }
mutual
infix 3 _β
_
data _β
_ : β {Ξ A} β Ξ β’ A β Ξ β’ A β Set where
reflβ
: β {Ξ A} {M : Ξ β’ A} β
M β
M
symβ
: β {Ξ A} {M Mβ² : Ξ β’ A} β
M β
Mβ² β
Mβ² β
M
transβ
: β {Ξ A} {M Mβ² Mβ³ : Ξ β’ A} β
M β
Mβ² β Mβ² β
Mβ³ β
M β
Mβ³
congΖβ
: β {Ξ A B x} {{_ : T (fresh x Ξ)}} {M Mβ² : [ Ξ , x β· A ] β’ B} β
M β
Mβ² β
Ζ x M β
Ζ x Mβ²
congββ
: β {Ξ A B} {M Mβ² : Ξ β’ A β B} {N Nβ² : Ξ β’ A} β
M β
Mβ² β N β
Nβ² β
M β N β
Mβ² β Nβ²
congβΆβ
: β {Ξ Ξ A} {M Mβ² : Ξ β’ A} {Ξ³ Ξ³β² : Ξ β Ξ} β
M β
Mβ² β Ξ³ β
β Ξ³β² β
M βΆ Ξ³ β
Mβ² βΆ Ξ³β²
convββ
: β {Ξ Ξ A B x} {{_ : T (fresh x Ξ)}} β
(M : [ Ξ , x β· A ] β’ B) (N : Ξ β’ A) (Ξ³ : Ξ β Ξ) β
(Ζ x M βΆ Ξ³) β N β
M βΆ [ Ξ³ , x β N ]
convββ
: β {Ξ A B x} {{_ : T (fresh x Ξ)}} β
(c : [ Ξ , x β· A ] β Ξ) (M : Ξ β’ A β B) β
M β
Ζ x ((M βΆ Οβ¨ c β©) β Ξ½ x zero)
convββ
: β {Ξ Ξ A x} {{_ : T (fresh x Ξ)}} β
(M : Ξ β’ A) (Ξ³ : Ξ β Ξ) β
Ξ½ x zero βΆ [ Ξ³ , x β M ] β
M
convββ
: β {Ξ Ξ A x} β
(c : Ξ β Ξ) (i : Ξ β x β· A) (j : Ξ β x β· A) β
Ξ½ x i βΆ Οβ¨ c β© β
Ξ½ x j
convβ
β
: β {Ξ A} β
(c : Ξ β Ξ) (M : Ξ β’ A) β
M βΆ Οβ¨ c β© β
M
convββ
: β {Ξ Ξ A B} β
(M : Ξ β’ A β B) (N : Ξ β’ A) (Ξ³ : Ξ β Ξ) β
(M β N) βΆ Ξ³ β
(M βΆ Ξ³) β (N βΆ Ξ³)
convββ
: β {Ξ Ξ Ξ A} β
(M : Ξ β’ A) (Ξ³ : Ξ β Ξ) (Ξ΄ : Ξ β Ξ) β
(M βΆ Ξ³) βΆ Ξ΄ β
M βΆ (Ξ³ β Ξ΄)
infix 3 _β
β_
data _β
β_ : β {Ξ Ξ} β Ξ β Ξ β Ξ β Ξ β Set where
reflβ
β : β {Ξ Ξ} {Ξ³ : Ξ β Ξ} β
Ξ³ β
β Ξ³
symβ
β : β {Ξ Ξ} {Ξ³ Ξ³β² : Ξ β Ξ} β
Ξ³ β
β Ξ³β² β
Ξ³β² β
β Ξ³
transβ
β : β {Ξ Ξ} {Ξ³ Ξ³β² Ξ³β³ : Ξ β Ξ} β
Ξ³ β
β Ξ³β² β Ξ³β² β
β Ξ³β³ β
Ξ³ β
β Ξ³β³
congββ
β : β {Ξ Ξ Ξ} {Ξ³ Ξ³β² : Ξ β Ξ} {Ξ΄ Ξ΄β² : Ξ β Ξ} β
Ξ³ β
β Ξ³β² β Ξ΄ β
β Ξ΄β² β
Ξ³ β Ξ΄ β
β Ξ³β² β Ξ΄β²
congββ
β : β {Ξ Ξ A x} {{_ : T (fresh x Ξ)}} {Ξ³ Ξ³β² : Ξ β Ξ} {M Mβ² : Ξ β’ A} β
Ξ³ β
β Ξ³β² β M β
Mβ² β
[ Ξ³ , x β M ] β
β [ Ξ³β² , x β Mβ² ]
convββ
β : β {Ξ Ξ Ξ Ξ©} β
(Ξ³ : Ξ β Ξ) (Ξ΄ : Ξ β Ξ) (ΞΈ : Ξ© β Ξ) β
(Ξ³ β Ξ΄) β ΞΈ β
β Ξ³ β (Ξ΄ β ΞΈ)
convββ
β : β {Ξ Ξ Ξ A x} {{_ : T (fresh x Ξ)}} β
(M : Ξ β’ A) (Ξ³ : Ξ β Ξ) (Ξ΄ : Ξ β Ξ) β
[ Ξ³ , x β M ] β Ξ΄ β
β [ Ξ³ β Ξ΄ , x β M βΆ Ξ΄ ]
convββ
β : β {Ξ Ξ A x} {{_ : T (fresh x Ξ)}} β
(c : [ Ξ , x β· A ] β Ξ) (M : Ξ β’ A) (Ξ³ : Ξ β Ξ) β
Οβ¨ c β© β [ Ξ³ , x β M ] β
β Ξ³
convββ
β : β {Ξ Ξ Ξ} β
(c : Ξ β Ξ) (cβ² : Ξ β Ξ) (cβ³ : Ξ β Ξ) β
Οβ¨ cβ² β© β Οβ¨ cβ³ β© β
β Οβ¨ c β©
convβ
β
β : β {Ξ Ξ} β
(c : Ξ β Ξ) (Ξ³ : Ξ β Ξ) β
Ξ³ β Οβ¨ c β© β
β Ξ³
convββ
β : β {Ξ} β
(c : Ξ β []) (Ξ³ : Ξ β []) β
Ξ³ β
β Οβ¨ c β©
convββ
β : β {Ξ Ξ A x} {{_ : T (fresh x Ξ)}} β
(c : [ Ξ , x β· A ] β Ξ) (Ξ³ : Ξ β [ Ξ , x β· A ]) (i : [ Ξ , x β· A ] β x β· A) β
Ξ³ β
β [ Οβ¨ c β© β Ξ³ , x β Ξ½ x i βΆ Ξ³ ]
module _ where
β‘ββ
: β {Ξ A} {M Mβ² : Ξ β’ A} β M β‘ Mβ² β M β
Mβ²
β‘ββ
refl = reflβ
module β
-Reasoning where
infix 1 begin_
begin_ : β {Ξ A} {M Mβ² : Ξ β’ A} β M β
Mβ² β M β
Mβ²
begin p = p
infixr 2 _β
β¨β©_
_β
β¨β©_ : β {Ξ A} (M {Mβ²} : Ξ β’ A) β M β
Mβ² β M β
Mβ²
M β
β¨β© p = p
infixr 2 _β
β¨_β©_
_β
β¨_β©_ : β {Ξ A} (M {Mβ² Mβ³} : Ξ β’ A) β M β
Mβ² β Mβ² β
Mβ³ β M β
Mβ³
M β
β¨ p β© pβ² = transβ
p pβ²
infixr 2 _β‘β¨β©_
_β‘β¨β©_ : β {Ξ A} (M {Mβ²} : Ξ β’ A) β M β
Mβ² β M β
Mβ²
M β‘β¨β© p = p
infixr 2 _β‘β¨_β©_
_β‘β¨_β©_ : β {Ξ A} (M {Mβ² Mβ³} : Ξ β’ A) β M β‘ Mβ² β Mβ² β
Mβ³ β M β
Mβ³
M β‘β¨ p β© pβ² = transβ
(β‘ββ
p) pβ²
infix 3 _β
_β : β {Ξ A} (M : Ξ β’ A) β M β
M
M β = reflβ
β‘ββ
β : β {Ξ Ξ} {Ξ³ Ξ³β² : Ξ β Ξ} β Ξ³ β‘ Ξ³β² β Ξ³ β
β Ξ³β²
β‘ββ
β refl = reflβ
β
module β
β-Reasoning where
infix 1 begin_
begin_ : β {Ξ Ξ} {Ξ³ Ξ³β² : Ξ β Ξ} β Ξ³ β
β Ξ³β² β Ξ³ β
β Ξ³β²
begin p = p
infixr 2 _β
ββ¨β©_
_β
ββ¨β©_ : β {Ξ Ξ} (Ξ³ {Ξ³β²} : Ξ β Ξ) β Ξ³ β
β Ξ³β² β Ξ³ β
β Ξ³β²
Ξ³ β
ββ¨β© p = p
infixr 2 _β
ββ¨_β©_
_β
ββ¨_β©_ : β {Ξ Ξ} (Ξ³ {Ξ³β² Ξ³β³} : Ξ β Ξ) β Ξ³ β
β Ξ³β² β Ξ³β² β
β Ξ³β³ β Ξ³ β
β Ξ³β³
Ξ³ β
ββ¨ p β© pβ² = transβ
β p pβ²
infixr 2 _β‘β¨β©_
_β‘β¨β©_ : β {Ξ Ξ} (Ξ³ {Ξ³β²} : Ξ β Ξ) β Ξ³ β
β Ξ³β² β Ξ³ β
β Ξ³β²
Ξ³ β‘β¨β© p = p
infixr 2 _β‘β¨_β©_
_β‘β¨_β©_ : β {Ξ Ξ} (Ξ³ {Ξ³β² Ξ³β³} : Ξ β Ξ) β Ξ³ β‘ Ξ³β² β Ξ³β² β
β Ξ³β³ β Ξ³ β
β Ξ³β³
Ξ³ β‘β¨ p β© pβ² = transβ
β (β‘ββ
β p) pβ²
infix 3 _β
_β : β {Ξ Ξ} (Ξ³ : Ξ β Ξ) β Ξ³ β
β Ξ³
Ξ³ β = reflβ
β