Skip to content

Commit fe9d734

Browse files
FrozenWintersFrozenWinters
committed
Adding my solutions
1 parent 40a91b6 commit fe9d734

File tree

1 file changed

+224
-0
lines changed

1 file changed

+224
-0
lines changed

‎Agda/HITs/Solutions6-Astra.agda

+224
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,224 @@
1+
{-# OPTIONS --rewriting --without-K #-}
2+
3+
open import new-prelude
4+
5+
open import Lecture6-notes
6+
open import Lecture5-notes
7+
8+
module Solutions6-Astra where
9+
10+
private
11+
variable
12+
ℓ ℓ₁ ℓ₂ : Level
13+
14+
postulate
15+
𝑓𝑖𝑔₈ : Type
16+
𝑝𝑡 : 𝑓𝑖𝑔₈
17+
𝑙₁ : 𝑝𝑡 ≡ 𝑝𝑡
18+
𝑙₂ : 𝑝𝑡 ≡ 𝑝𝑡
19+
𝑓𝑖𝑔₈-elim : (X : 𝑓𝑖𝑔₈ → Type ℓ)
20+
(x : X 𝑝𝑡) (p : x ≡ x [ X ↓ 𝑙₁ ]) (q : x ≡ x [ X ↓ 𝑙₂ ])
21+
(x : 𝑓𝑖𝑔₈) → X x
22+
𝑓𝑖𝑔₈-elim-𝑝𝑡 : (X : 𝑓𝑖𝑔₈ → Type ℓ)
23+
(x : X 𝑝𝑡) (p : x ≡ x [ X ↓ 𝑙₁ ]) (q : x ≡ x [ X ↓ 𝑙₂ ]) →
24+
𝑓𝑖𝑔₈-elim X x p q 𝑝𝑡 ≡ x
25+
{-# REWRITE 𝑓𝑖𝑔₈-elim-𝑝𝑡 #-}
26+
27+
postulate
28+
𝑓𝑖𝑔₈-elim-𝑙₁ : (X : 𝑓𝑖𝑔₈ → Type ℓ)
29+
(x : X 𝑝𝑡) (p : x ≡ x [ X ↓ 𝑙₁ ]) (q : x ≡ x [ X ↓ 𝑙₂ ]) →
30+
apd (𝑓𝑖𝑔₈-elim X x p q) 𝑙₁ ≡ p
31+
𝑓𝑖𝑔₈-elim-𝑙₂ : (X : 𝑓𝑖𝑔₈ → Type ℓ)
32+
(x : X 𝑝𝑡) (p : x ≡ x [ X ↓ 𝑙₁ ]) (q : x ≡ x [ X ↓ 𝑙₂ ]) →
33+
apd (𝑓𝑖𝑔₈-elim X x p q) 𝑙₂ ≡ q
34+
35+
Path→PathP : {A : Type ℓ₁} {B : Type ℓ₂} {a₁ a₂ : A} {b₁ b₂ : B}
36+
(p : a₁ ≡ a₂) → b₁ ≡ b₂ → b₁ ≡ b₂ [ (λ _ → B) ↓ p ]
37+
Path→PathP (refl _) (refl _) = reflo
38+
39+
PathP→Path : {A : Type ℓ₁} {B : Type ℓ₂} {a₁ a₂ : A}
40+
{b₁ b₂ : B} (p : a₁ ≡ a₂) → b₁ ≡ b₂ [ (λ _ → B) ↓ p ] → b₁ ≡ b₂
41+
PathP→Path (refl _) reflo = refl _
42+
43+
Path-η : {A : Type ℓ₁} {B : Type ℓ₂}
44+
{a1 a2 : A} {b1 b2 : B} (p : a1 ≡ a2) (q : b1 ≡ b2) →
45+
PathP→Path p (Path→PathP p q) ≡ q
46+
Path-η (refl _) (refl _) = refl _
47+
48+
ap-apd : {A : Type ℓ₁} {B : Type ℓ₂} {a1 a2 : A}
49+
(p : a1 ≡ a2) (f : A → B) →
50+
Path→PathP p (ap f p) ≡ apd f p
51+
ap-apd (refl _) f = refl reflo
52+
53+
𝑓𝑖𝑔₈-rec : {X : Type ℓ} (x : X) (p : x ≡ x [ X ]) (q : x ≡ x [ X ]) →
54+
𝑓𝑖𝑔₈ → X
55+
𝑓𝑖𝑔₈-rec {X = X} x p q =
56+
𝑓𝑖𝑔₈-elim (λ _ → X) x (Path→PathP 𝑙₁ p) (Path→PathP 𝑙₂ q)
57+
58+
𝑓𝑖𝑔₈-rec-𝑝𝑡 : {X : Type ℓ} (x : X) (p : x ≡ x [ X ]) (q : x ≡ x [ X ]) →
59+
𝑓𝑖𝑔₈-rec x p q 𝑝𝑡 ≡ x
60+
𝑓𝑖𝑔₈-rec-𝑝𝑡 _ _ _ = refl _
61+
62+
𝑓𝑖𝑔₈-rec-𝑙₁ : {X : Type ℓ} (x : X) (p : x ≡ x [ X ]) (q : x ≡ x [ X ]) →
63+
ap (𝑓𝑖𝑔₈-rec x p q) 𝑙₁ ≡ p
64+
𝑓𝑖𝑔₈-rec-𝑙₁ {X = X} x p q =
65+
! (Path-η 𝑙₁ (ap (𝑓𝑖𝑔₈-rec x p q) 𝑙₁))
66+
∙ ap (PathP→Path 𝑙₁)
67+
(ap-apd 𝑙₁ (𝑓𝑖𝑔₈-rec x p q)
68+
∙ 𝑓𝑖𝑔₈-elim-𝑙₁ (λ _ → X) x (Path→PathP 𝑙₁ p) (Path→PathP 𝑙₂ q))
69+
∙ Path-η 𝑙₁ p
70+
71+
𝑓𝑖𝑔₈-rec-𝑙₂ : {X : Type ℓ} (x : X) (p : x ≡ x [ X ]) (q : x ≡ x [ X ]) →
72+
ap (𝑓𝑖𝑔₈-rec x p q) 𝑙₂ ≡ q
73+
𝑓𝑖𝑔₈-rec-𝑙₂ {X = X} x p q =
74+
! (Path-η 𝑙₂ (ap (𝑓𝑖𝑔₈-rec x p q) 𝑙₂))
75+
∙ ap (PathP→Path 𝑙₂)
76+
(ap-apd 𝑙₂ (𝑓𝑖𝑔₈-rec x p q)
77+
∙ 𝑓𝑖𝑔₈-elim-𝑙₂ (λ _ → X) x (Path→PathP 𝑙₁ p) (Path→PathP 𝑙₂ q))
78+
∙ Path-η 𝑙₂ q
79+
80+
concat-equiv : {A : Type} {x y z : A} →
81+
y ≡ z → (x ≡ y) ≃ (x ≡ z)
82+
concat-equiv p =
83+
Equivalence
84+
(λ q → q ∙ p)
85+
(Inverse
86+
(λ q → q ∙ ! p)
87+
(λ q →
88+
! (∙assoc q p (! p)) ∙ ap (q ∙_) (!-inv-r p))
89+
(λ q → q ∙ ! p)
90+
(λ q →
91+
! (∙assoc q (! p) p) ∙ ap (q ∙_) (!-inv-l p)))
92+
93+
transport-∙ : {A : Type ℓ₁} {B : A → Type ℓ₂}
94+
{x y z : A} (p : x ≡ y) (q : y ≡ z) →
95+
transport B (p ∙ q) ∼ transport B q ∘ transport B p
96+
transport-∙ (refl _) (refl _) α = refl α
97+
98+
module AssumeF₂
99+
(F₂ : Type)
100+
(𝑒 : F₂)
101+
(𝑠ℎ₁ : F₂ ≃ F₂)
102+
(𝑠ℎ₂ : F₂ ≃ F₂)
103+
(F₂-rec : {ℓ : Level} {X : Type ℓ} (x : X) (m1 : X ≃ X) (m2 : X ≃ X) →
104+
F₂ → X)
105+
(F₂-rec-𝑒 : {ℓ : Level} {X : Type ℓ} (x : X) (m1 : X ≃ X) (m2 : X ≃ X) →
106+
F₂-rec x m1 m2 𝑒 ≡ x)
107+
(F₂-rec-𝑠ℎ₁ : {ℓ : Level} {X : Type ℓ} (x : X) (m1 : X ≃ X) (m2 : X ≃ X)
108+
(a : F₂) → F₂-rec x m1 m2 (fwd 𝑠ℎ₁ a) ≡ fwd m1 (F₂-rec x m1 m2 a))
109+
(F₂-rec-𝑠ℎ₂ : {ℓ : Level} {X : Type ℓ} (x : X) (m1 : X ≃ X) (m2 : X ≃ X)
110+
(a : F₂) → F₂-rec x m1 m2 (fwd 𝑠ℎ₂ a) ≡ fwd m2 (F₂-rec x m1 m2 a))
111+
(F₂-rec-unique : {ℓ : Level} {X : Type ℓ} (f : F₂ → X) (x : X)
112+
(m1 : X ≃ X) (m2 : X ≃ X) → f 𝑒 ≡ x →
113+
((f ∘ fwd 𝑠ℎ₁) ∼ (fwd m1 ∘ f)) → ((f ∘ fwd 𝑠ℎ₂) ∼ (fwd m2 ∘ f)) →
114+
(z : F₂) → f z ≡ F₂-rec x m1 m2 z)
115+
(hSetF : is-set F₂) where
116+
117+
Cover : 𝑓𝑖𝑔₈ → Type
118+
Cover = 𝑓𝑖𝑔₈-rec F₂ (ua 𝑠ℎ₁) (ua 𝑠ℎ₂)
119+
120+
encode : {x : 𝑓𝑖𝑔₈} → 𝑝𝑡 ≡ x → Cover x
121+
encode p = transport Cover p 𝑒
122+
123+
loopify : F₂ → 𝑝𝑡 ≡ 𝑝𝑡
124+
loopify = F₂-rec (refl 𝑝𝑡) (concat-equiv 𝑙₁) (concat-equiv 𝑙₂)
125+
126+
tr-Cover-𝑙₁ : (α : F₂) → transport Cover 𝑙₁ α ≡ fwd 𝑠ℎ₁ α
127+
tr-Cover-𝑙₁ α =
128+
transport Cover 𝑙₁ α
129+
≡⟨ transport-ap-assoc Cover 𝑙₁ ⟩
130+
transport (λ X → X) (ap Cover 𝑙₁) α
131+
≡⟨ ap (λ ϕ → transport (λ X → X) ϕ α)
132+
(𝑓𝑖𝑔₈-rec-𝑙₁ F₂ (ua 𝑠ℎ₁) (ua 𝑠ℎ₂)) ⟩
133+
transport (λ X → X) (ua 𝑠ℎ₁) α
134+
≡⟨ uaβ 𝑠ℎ₁ ⟩
135+
fwd 𝑠ℎ₁ α
136+
∎
137+
138+
tr-Cover-𝑙₂ : (α : F₂) → transport Cover 𝑙₂ α ≡ fwd 𝑠ℎ₂ α
139+
tr-Cover-𝑙₂ α =
140+
transport Cover 𝑙₂ α
141+
≡⟨ transport-ap-assoc Cover 𝑙₂ ⟩
142+
transport (λ X → X) (ap Cover 𝑙₂) α
143+
≡⟨ ap (λ ϕ → transport (λ X → X) ϕ α)
144+
(𝑓𝑖𝑔₈-rec-𝑙₂ F₂ (ua 𝑠ℎ₁) (ua 𝑠ℎ₂)) ⟩
145+
transport (λ X → X) (ua 𝑠ℎ₂) α
146+
≡⟨ uaβ 𝑠ℎ₂ ⟩
147+
fwd 𝑠ℎ₂ α
148+
∎
149+
150+
loopify-𝑙₁ : (α : F₂) →
151+
loopify (transport Cover 𝑙₁ α) ≡ loopify α ∙ 𝑙₁
152+
loopify-𝑙₁ α =
153+
loopify (transport Cover 𝑙₁ α)
154+
≡⟨ ap loopify (tr-Cover-𝑙₁ α) ⟩
155+
loopify (fwd 𝑠ℎ₁ α)
156+
≡⟨ F₂-rec-𝑠ℎ₁ (refl 𝑝𝑡) (concat-equiv 𝑙₁) (concat-equiv 𝑙₂) α ⟩
157+
loopify α ∙ 𝑙₁
158+
∎
159+
160+
loopify-𝑙₂ : (α : F₂) →
161+
loopify (transport Cover 𝑙₂ α) ≡ loopify α ∙ 𝑙₂
162+
loopify-𝑙₂ α =
163+
loopify (transport Cover 𝑙₂ α)
164+
≡⟨ ap loopify (tr-Cover-𝑙₂ α) ⟩
165+
loopify (fwd 𝑠ℎ₂ α)
166+
≡⟨ F₂-rec-𝑠ℎ₂ (refl 𝑝𝑡) (concat-equiv 𝑙₁) (concat-equiv 𝑙₂) α ⟩
167+
loopify α ∙ 𝑙₂
168+
∎
169+
170+
decode : {x : 𝑓𝑖𝑔₈} → Cover x → 𝑝𝑡 ≡ x
171+
decode {x} =
172+
𝑓𝑖𝑔₈-elim (λ α → Cover α → 𝑝𝑡 ≡ α)
173+
loopify
174+
(PathOver-→ (λ α → PathOver-path-to (! (loopify-𝑙₁ α))))
175+
(PathOver-→ (λ α → PathOver-path-to (! (loopify-𝑙₂ α))))
176+
x
177+
178+
encode-decode : {x : 𝑓𝑖𝑔₈} (p : 𝑝𝑡 ≡ x) → decode (encode p) ≡ p
179+
encode-decode (refl .𝑝𝑡) =
180+
F₂-rec-𝑒 (refl 𝑝𝑡) (concat-equiv 𝑙₁) (concat-equiv 𝑙₂)
181+
182+
𝑠ℎ₁-lem : (α : F₂) →
183+
encode (loopify (fwd 𝑠ℎ₁ α)) ≡ fwd 𝑠ℎ₁ (encode (loopify α))
184+
𝑠ℎ₁-lem α =
185+
encode (loopify (fwd 𝑠ℎ₁ α))
186+
≡⟨ ap encode
187+
(F₂-rec-𝑠ℎ₁ (refl 𝑝𝑡) (concat-equiv 𝑙₁) (concat-equiv 𝑙₂) α) ⟩
188+
encode (loopify α ∙ 𝑙₁)
189+
≡⟨ transport-∙ (loopify α) 𝑙₁ 𝑒 ⟩
190+
transport Cover 𝑙₁ (transport Cover (loopify α) 𝑒)
191+
≡⟨ tr-Cover-𝑙₁ (transport Cover (loopify α) 𝑒) ⟩
192+
fwd 𝑠ℎ₁ (encode (loopify α))
193+
∎
194+
195+
𝑠ℎ₂-lem : (α : F₂) →
196+
encode (loopify (fwd 𝑠ℎ₂ α)) ≡ fwd 𝑠ℎ₂ (encode (loopify α))
197+
𝑠ℎ₂-lem α =
198+
encode (loopify (fwd 𝑠ℎ₂ α))
199+
≡⟨ ap encode
200+
(F₂-rec-𝑠ℎ₂ (refl 𝑝𝑡) (concat-equiv 𝑙₁) (concat-equiv 𝑙₂) α) ⟩
201+
encode (loopify α ∙ 𝑙₂)
202+
≡⟨ transport-∙ (loopify α) 𝑙₂ 𝑒 ⟩
203+
transport Cover 𝑙₂ (transport Cover (loopify α) 𝑒)
204+
≡⟨ tr-Cover-𝑙₂ (transport Cover (loopify α) 𝑒) ⟩
205+
fwd 𝑠ℎ₂ (encode (loopify α))
206+
∎
207+
208+
encode-loopify : (α : F₂) → encode (loopify α) ≡ α
209+
encode-loopify α =
210+
F₂-rec-unique (encode ∘ loopify) 𝑒 𝑠ℎ₁ 𝑠ℎ₂
211+
(ap encode (encode-decode (refl 𝑝𝑡))) 𝑠ℎ₁-lem 𝑠ℎ₂-lem α
212+
∙ ! (F₂-rec-unique (λ β → β) 𝑒 𝑠ℎ₁ 𝑠ℎ₂
213+
(refl 𝑒) (λ _ → refl _) (λ _ → refl _) α)
214+
215+
decode-encode : {x : 𝑓𝑖𝑔₈} (p : Cover x) → encode (decode {x} p) ≡ p
216+
decode-encode {x} =
217+
𝑓𝑖𝑔₈-elim (λ x → (p : Cover x) → encode (decode {x} p) ≡ p)
218+
encode-loopify
219+
(PathOver-Π (λ {y} {z} q →
220+
fwd (transport-to-pathover _ _ _ _) (hSetF _ _ _ _)))
221+
(PathOver-Π (λ {y} {z} q →
222+
fwd (transport-to-pathover _ _ _ _) (hSetF _ _ _ _)))
223+
x
224+

0 commit comments

Comments
 (0)