update
This commit is contained in:
parent
5d3ebb119b
commit
e2212f7999
2 changed files with 24 additions and 3 deletions
|
@ -28,4 +28,8 @@
|
||||||
}
|
}
|
||||||
</style>
|
</style>
|
||||||
|
|
||||||
<h1>HoTT Book Progress</h1>
|
<h1>HoTT Book Progress</h1>
|
||||||
|
|
||||||
|
<p>
|
||||||
|
Last 7 days: <img src="https://wakapi.mzhang.io/api/badge/michael/interval:last_7_days/project:type-theory" />
|
||||||
|
</p>
|
|
@ -99,10 +99,27 @@ module theorem2∙1∙6 where
|
||||||
Ω² {l} = Ω[_] {l = l} 2
|
Ω² {l} = Ω[_] {l = l} 2
|
||||||
|
|
||||||
compose2 : {l : Level} {A : Set l} {a : A} → fst (Ω² (A , a)) → fst (Ω² (A , a)) → fst (Ω² (A , a))
|
compose2 : {l : Level} {A : Set l} {a : A} → fst (Ω² (A , a)) → fst (Ω² (A , a)) → fst (Ω² (A , a))
|
||||||
compose2 x y = x ∙ y
|
compose2 x y = horiz x y
|
||||||
|
where
|
||||||
|
variable
|
||||||
|
A : Set l
|
||||||
|
a b c : A
|
||||||
|
p q : a ≡ b
|
||||||
|
r s : b ≡ c
|
||||||
|
α : p ≡ q
|
||||||
|
β : r ≡ s
|
||||||
|
|
||||||
|
_∙ᵣ_ : p ≡ q → (r : b ≡ c) → p ∙ r ≡ q ∙ r
|
||||||
|
α ∙ᵣ refl = sym (lemma2∙1∙4.i1 _) ∙ α ∙ lemma2∙1∙4.i1 _
|
||||||
|
|
||||||
|
_∙ₗ_ : (q : a ≡ b) → r ≡ s → q ∙ r ≡ q ∙ s
|
||||||
|
refl ∙ₗ β = sym (lemma2∙1∙4.i2 _) ∙ β ∙ lemma2∙1∙4.i2 _
|
||||||
|
|
||||||
|
horiz : p ≡ q → r ≡ s → p ∙ r ≡ q ∙ s
|
||||||
|
horiz α β = (α ∙ᵣ _) ∙ (_ ∙ₗ β)
|
||||||
|
|
||||||
compose2-commutative : {l : Level} {A : Set l} {a : A} (x y : fst (Ω² (A , a))) → compose2 x y ≡ compose2 y x
|
compose2-commutative : {l : Level} {A : Set l} {a : A} (x y : fst (Ω² (A , a))) → compose2 x y ≡ compose2 y x
|
||||||
compose2-commutative {l} {A} {a} x y = {! !}
|
compose2-commutative {l} {A} {a} x y = {! x !}
|
||||||
```
|
```
|
||||||
|
|
||||||
### Definition 2.1.7 (pointed type)
|
### Definition 2.1.7 (pointed type)
|
||||||
|
|
Loading…
Reference in a new issue