296 lines
8.5 KiB
Agda
296 lines
8.5 KiB
Agda
module 0Trinitarianism.Quest4Solutions where
|
||
|
||
open import 0Trinitarianism.Preambles.P4
|
||
|
||
private
|
||
variable
|
||
u : Level
|
||
|
||
|
||
data Id {A : Type} : (x y : A) → Type where
|
||
|
||
rfl : {x : A} → Id x x
|
||
|
||
idSym : (A : Type) (x y : A) → Id x y → Id y x
|
||
idSym A x .x rfl = rfl
|
||
|
||
Sym : {A : Type} {x y : A} → Id x y → Id y x
|
||
Sym rfl = rfl
|
||
|
||
_*_ : {A : Type} {x y z : A} → Id x y → Id y z → Id x z
|
||
rfl * q = q
|
||
|
||
_*0_ : {A : Type} {x y z : A} → Id x y → Id y z → Id x z
|
||
p *0 rfl = p
|
||
|
||
_*1_ : {A : Type} {x y z : A} → Id x y → Id y z → Id x z
|
||
rfl *1 rfl = rfl
|
||
|
||
------------Cong-------------------------
|
||
|
||
private
|
||
variable
|
||
A B : Type
|
||
w x y z : A
|
||
|
||
------------Groupoid Laws----------------
|
||
|
||
rfl* : (p : Id x y) → Id (rfl * p) p
|
||
rfl* p = rfl
|
||
|
||
*rfl : (p : Id x y) → Id (p * rfl) p
|
||
*rfl rfl = rfl
|
||
|
||
*Sym : (p : Id x y) → Id (p * Sym p) rfl
|
||
*Sym rfl = rfl
|
||
|
||
Sym* : (p : Id x y) → Id rfl (p * Sym p)
|
||
Sym* rfl = rfl
|
||
|
||
Assoc : (p : Id w x) (q : Id x y) (r : Id y z)
|
||
→ Id ((p * q) * r) (p * (q * r))
|
||
Assoc rfl q r = rfl
|
||
|
||
|
||
-------------Mapping Out----------------
|
||
|
||
outOfId : (M : (y : A) → Id x y → Type) → M x rfl
|
||
→ {y : A} (p : Id x y) → M y p
|
||
outOfId M h rfl = h
|
||
|
||
------------Path vs Id--------------------
|
||
|
||
Path→Id : x ≡ y → Id x y
|
||
Path→Id {A} {x} = J (λ y p → Id x y) rfl
|
||
|
||
Id→Path : Id x y → x ≡ y
|
||
Id→Path rfl = refl
|
||
|
||
-----------Basics about paths--------------
|
||
|
||
Cong : (f : A → B) → Id x y → Id (f x) (f y)
|
||
Cong f rfl = rfl
|
||
|
||
cong' : (f : A → B) (p : x ≡ y) → f x ≡ f y
|
||
cong' {x = x} f = J (λ y p → f x ≡ f y) refl
|
||
|
||
cong'' : (f : A → B) (p : x ≡ y) → f x ≡ f y
|
||
cong'' f p = Id→Path (Cong f (Path→Id p))
|
||
|
||
------------Path vs Id---------------------
|
||
|
||
Path→IdRefl : Path→Id (refl {x = x}) ≡ rfl
|
||
Path→IdRefl {x = x} = JRefl (λ y p → Id x y) rfl
|
||
|
||
Path≡Id : (x ≡ y) ≡ (Id x y)
|
||
Path≡Id {A} {x} {y} = isoToPath (iso Path→Id Id→Path rightInv leftInv) where
|
||
|
||
rightInv : section (Path→Id {A} {x} {y}) Id→Path
|
||
rightInv rfl = Path→IdRefl
|
||
|
||
leftInv : retract (Path→Id {A} {x} {y}) Id→Path
|
||
leftInv = J (λ y p → Id→Path (Path→Id p) ≡ p) (cong (λ p → Id→Path p) Path→IdRefl)
|
||
|
||
-----------Basics about Path Space-----------------
|
||
|
||
sym : {x y : A} → x ≡ y → y ≡ x
|
||
sym {A} {x} = J (λ y1 p → y1 ≡ x) refl
|
||
|
||
symRefl : {x : A} → sym {A} {x} {x} (refl) ≡ refl
|
||
symRefl {A} {x} = JRefl (λ y1 p → y1 ≡ x) refl
|
||
|
||
Trans : {x y z : A} → x ≡ y → y ≡ z → x ≡ z
|
||
Trans {x = x} {z = z} = J (λ y1 p → y1 ≡ z → x ≡ z) λ q → q
|
||
|
||
_∙_ = Trans -- input \.
|
||
|
||
_≡⟨_⟩_ : (x : A) → x ≡ y → y ≡ z → x ≡ z -- input \< and \>
|
||
_ ≡⟨ x≡y ⟩ y≡z = x≡y ∙ y≡z
|
||
|
||
_∎ : (x : A) → x ≡ x -- input \qed
|
||
_ ∎ = refl
|
||
|
||
infixr 30 _∙_
|
||
infix 3 _∎
|
||
infixr 2 _≡⟨_⟩_
|
||
|
||
TransRefl : {x y : A} → Trans {A} {x} {x} {y} refl ≡ λ q → q
|
||
TransRefl {x = x} {y = y} = JRefl ((λ y1 p → y1 ≡ y → x ≡ y)) λ q → q
|
||
|
||
refl∙refl : {x : A} → refl {_} {A} {x} ∙ refl ≡ refl
|
||
refl∙refl = cong (λ f → f refl) TransRefl
|
||
|
||
∙refl : {x y : A} (p : x ≡ y) → Trans p refl ≡ p
|
||
∙refl {A} {x} {y} = J (λ y p → Trans p refl ≡ p) refl∙refl
|
||
|
||
refl∙ : {A : Type} {x y : A} (p : x ≡ y) → refl ∙ p ≡ p
|
||
refl∙ = J (λ y p → refl ∙ p ≡ p) refl∙refl
|
||
|
||
|
||
∙sym : {A : Type} {x y : A} (p : x ≡ y) → p ∙ sym p ≡ refl
|
||
∙sym = J (λ y p → p ∙ sym p ≡ refl)
|
||
(
|
||
refl ∙ sym refl
|
||
≡⟨ cong (λ p → refl ∙ p) symRefl ⟩
|
||
refl ∙ refl
|
||
≡⟨ refl∙refl ⟩
|
||
refl ∎
|
||
)
|
||
|
||
|
||
sym∙ : {A : Type} {x y : A} (p : x ≡ y) → (sym p) ∙ p ≡ refl
|
||
sym∙ = J (λ y p → (sym p) ∙ p ≡ refl)
|
||
(
|
||
(sym refl) ∙ refl
|
||
≡⟨ cong (λ p → p ∙ refl) symRefl ⟩
|
||
refl ∙ refl
|
||
≡⟨ refl∙refl ⟩
|
||
refl ∎
|
||
)
|
||
|
||
assoc : {A : Type} {w x : A} (p : w ≡ x) {y z : A} (q : x ≡ y) (r : y ≡ z)
|
||
→ (p ∙ q) ∙ r ≡ p ∙ (q ∙ r)
|
||
assoc {A} = J
|
||
-- casing on p
|
||
(λ x p → {y z : A} (q : x ≡ y) (r : y ≡ z) → (p ∙ q) ∙ r ≡ p ∙ (q ∙ r))
|
||
-- reduce to showing when p = refl
|
||
λ q r → ((refl ∙ q) ∙ r)
|
||
≡⟨ cong (λ p' → p' ∙ r) (refl∙ q) ⟩
|
||
(q ∙ r)
|
||
≡⟨ sym (refl∙ (q ∙ r)) ⟩
|
||
(refl ∙ (q ∙ r)) ∎
|
||
|
||
------------------Transport---------------------
|
||
|
||
id : A → A
|
||
id x = x
|
||
|
||
pathToFun : A ≡ B → A → B
|
||
pathToFun {A} = J (λ B p → (A → B)) id
|
||
|
||
pathToFunRefl : pathToFun (refl {x = A}) ≡ id
|
||
pathToFunRefl {A} = JRefl (λ B p → (A → B)) id
|
||
|
||
pathToFunReflx : pathToFun (refl {x = A}) x ≡ x
|
||
pathToFunReflx {x = x} = cong (λ f → f x) pathToFunRefl
|
||
|
||
endPt : (B : A → Type) (p : x ≡ y) → B x → B y
|
||
endPt {x = x} B = J (λ y p → B x → B y) id
|
||
|
||
endPtRefl : (B : A → Type) → endPt B (refl {x = x}) ≡ id
|
||
endPtRefl {x = x} B = JRefl ((λ y p → B x → B y)) id
|
||
|
||
endPt' : (B : A → Type) (p : x ≡ y) → B x → B y
|
||
endPt' B p = pathToFun (cong B p )
|
||
|
||
--------------funExt---------------------
|
||
|
||
funExt : (B : A → Type) (f g : (a : A) → B a) →
|
||
((a : A) → f a ≡ g a) → f ≡ g
|
||
funExt B f g h = λ i a → h a i
|
||
|
||
funExtPath : (B : A → Type) (f g : (a : A) → B a) → (f ≡ g) ≡ ((a : A) → f a ≡ g a)
|
||
funExtPath {A} B f g = isoToPath (iso fun (funExt B f g) rightInv leftInv) where
|
||
|
||
fun : f ≡ g → (a : A) → f a ≡ g a
|
||
fun h = λ a i → h i a
|
||
|
||
rightInv : section fun (funExt B f g)
|
||
rightInv h = refl
|
||
|
||
leftInv : retract fun (funExt B f g)
|
||
leftInv h = refl
|
||
|
||
--------------Path on Products-----------
|
||
|
||
data _×_ (A B : Type) : Type where
|
||
|
||
_,_ : A → B → A × B
|
||
|
||
Id× : {A B : Type} (a0 a1 : A) (b0 b1 : B)
|
||
→ (Id {A × B} ( a0 , b0 ) ( a1 , b1 )) ≡ (Id a0 a1 × Id b0 b1)
|
||
Id× {A} {B} a0 a1 b0 b1 = isoToPath (iso fun inv rightInv leftInv) where
|
||
|
||
fun : Id {A = A × B} ( a0 , b0 ) ( a1 , b1 ) → Id a0 a1 × Id b0 b1
|
||
fun rfl = rfl , rfl
|
||
|
||
inv : Id a0 a1 × Id b0 b1 → Id {A = A × B} ( a0 , b0 ) ( a1 , b1 )
|
||
inv (rfl , rfl) = rfl
|
||
|
||
rightInv : section fun inv
|
||
rightInv (rfl , rfl) = refl
|
||
|
||
leftInv : retract fun inv
|
||
leftInv rfl = refl
|
||
|
||
fst : A × B → A
|
||
fst (a , b) = a
|
||
|
||
snd : A × B → B
|
||
snd (a , b) = b
|
||
|
||
Path× : {A B : Type} (x y : A × B) → (x ≡ y) ≡ ((fst x ≡ fst y) × (snd x ≡ snd y))
|
||
Path× {A} {B} (a0 , b0) (a1 , b1) =
|
||
isoToPath (iso fun (inv a0 a1 b0 b1) rightInv leftInv) where
|
||
|
||
fun : {x y : A × B} → x ≡ y → (fst x ≡ fst y) × (snd x ≡ snd y)
|
||
fun {x} {y} = J (λ y p → (fst x ≡ fst y) × (snd x ≡ snd y)) (refl , refl)
|
||
|
||
funRefl : (x : A × B) → fun (refl {x = x}) ≡ ( refl , refl )
|
||
funRefl x = JRefl {_} {A × B} {x}
|
||
((λ y p → (fst x ≡ fst y) × (snd x ≡ snd y))) ( refl , refl )
|
||
|
||
inv : (a0 a1 : A) (b0 b1 : B) → (a0 ≡ a1) × (b0 ≡ b1)
|
||
→ _≡_ {A = A × B} ( a0 , b0 ) ( a1 , b1 )
|
||
inv a0 a1 b0 b1 (p , q) =
|
||
J -- first induct on p
|
||
(λ y p → _≡_ {A = A × B} ( a0 , b0 ) ( y , b1 ))
|
||
(
|
||
J -- then induct on q
|
||
(λ y q → _≡_ {A = A × B} ( a0 , b0 ) ( a0 , y ))
|
||
refl
|
||
q
|
||
) p
|
||
|
||
invRefl : (a : A) (b : B) → inv a a b b (refl , refl) ≡ refl
|
||
invRefl a b =
|
||
inv a a b b (refl , refl)
|
||
≡⟨ JRefl (λ y p → (a , b) ≡ (y , b)) (J (λ y q → (a , b) ≡ (a , y)) refl refl) ⟩
|
||
J (λ y q → _≡_ {A = A × B} ( a , b ) ( a , y )) refl refl
|
||
≡⟨ JRefl ((λ y q → _≡_ {A = A × B} ( a , b ) ( a , y ))) refl ⟩
|
||
refl ∎
|
||
|
||
Inv : (x y : A × B) → (fst x ≡ fst y) × (snd x ≡ snd y) → x ≡ y
|
||
Inv (a0 , b0) (a1 , b1) = inv a0 a1 b0 b1
|
||
|
||
InvRefl : {x : A × B} → Inv x x (refl , refl) ≡ refl {x = x}
|
||
InvRefl {a , b} = invRefl a b
|
||
|
||
rightInv : section fun (inv a0 a1 b0 b1)
|
||
rightInv (p , q) =
|
||
J -- first induct on p
|
||
(λ y p → fun (inv a0 y b0 b1 (p , q)) ≡ (p , q))
|
||
(
|
||
J -- then induct on q
|
||
(λ y q → fun (inv a0 a0 b0 y (refl , q)) ≡ (refl , q))
|
||
(
|
||
fun (inv a0 a0 b0 b0 (refl , refl))
|
||
≡⟨ cong fun (invRefl a0 b0) ⟩
|
||
fun (refl {x = (a0 , b0)})
|
||
≡⟨ funRefl (a0 , b0) ⟩
|
||
(refl , refl) ∎)
|
||
q)
|
||
p
|
||
|
||
leftInv : {x y : A × B} → retract fun (Inv x y)
|
||
leftInv {x} = J (λ y p → Inv x y (fun p) ≡ p)
|
||
(
|
||
Inv x x (fun {x = x} refl)
|
||
≡⟨ cong (Inv x x) (funRefl x) ⟩
|
||
Inv x x (refl , refl)
|
||
≡⟨ InvRefl ⟩
|
||
refl ∎)
|
||
|
||
leftinv : (x y : A × B) → retract fun (inv (fst x) (fst y) (snd x) (snd y))
|
||
leftinv (a0 , b0) (a1 , b1) = leftInv
|