Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

A few local updates #10

Merged
merged 3 commits into from
Dec 15, 2024
Merged

A few local updates #10

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
877361d
update to Agda 2.6.4.3
PHart3 Dec 15, 2024
2440289
define ptd homotopy via == instead of =-=
PHart3 Dec 15, 2024
35a87e6
new name for helper function
PHart3 Dec 15, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 11 additions & 11 deletions Colimit-code/Map-Nat/CosColimitPstCmp.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,9 @@ module CosColimitPstCmp where

module _ {ℓ₁ ℓ₂ ℓ₃} {A : Type ℓ₁} {B : Type ℓ₂} {C : Type ℓ₃} (h : B → C) (f : A → B) where

ap-∘-∙ : {x y : A} (p₁ : x == y) {z : B} (p₂ : f y == z) {c : C} {s : h z == c}
ap-∘-∙-∙ : {x y : A} (p₁ : x == y) {z : B} (p₂ : f y == z) {c : C} {s : h z == c}
→ ap h (ap f p₁ ∙ p₂) ∙ s == ap (h ∘ f) p₁ ∙ ap h p₂ ∙ s
ap-∘-∙ idp p₂ = idp
ap-∘-∙-∙ idp p₂ = idp

ap-∘-rid : {x y : A} (p : x == y) → ap h (ap f p) ∙ idp == ap (h ∘ f) p
ap-∘-rid idp = idp
Expand Down Expand Up @@ -71,7 +71,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type
ap φ₁ (ap f p₁) ∙ idp) ∙
ap (φ₁ ∘ f ∘ right ∘ cin j) p₂ ∙
ap (φ₁ ∘ f) p₃ ∙ ap φ₁ p₄ ∙ p₅))
(ap-∘-∙ φ₁ f p₃ p₄) ◃∙
(ap-∘-∙-∙ φ₁ f p₃ p₄) ◃∙
long-path-red p₂
(ap (φ₁ ∘ f) p₃ ∙
ap φ₁ p₄ ∙ p₅)
Expand All @@ -98,7 +98,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type
ap (λ p → ap φ₁ p ∙ φ₂ a) (ap-cp-revR f (right ∘ cin j) p₂
p₁ ∙
ap (λ p → p ∙ fₚ a) (ap (ap f) τ))) ◃∙
ap-∘-∙ φ₁ f σ (fₚ a) ◃∎
ap-∘-∙-∙ φ₁ f σ (fₚ a) ◃∎
=ₛ
(ap-cp-revR (φ₁ ∘ f) (right ∘ cin j)
p₂ p₁ ∙
Expand All @@ -107,14 +107,14 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type
NatSq-1-Λ-red2 {i} {j} g a idp idp p₃ idp = =ₛ-in (lemma p₃ (fₚ a))
where
lemma : {z : P} (p : right (cin j (fst (F <#> g) (fun (F # i) a))) == z) (c : f z == fun T a)
→ ↯ (NatSq-1-Λ-aux g a idp idp p c (φ₂ a)) ∙ ap-∘-∙ φ₁ f p c == idp
→ ↯ (NatSq-1-Λ-aux g a idp idp p c (φ₂ a)) ∙ ap-∘-∙-∙ φ₁ f p c == idp
lemma idp c = idp

-- τ = (snd (comTri ColCoC g) a)

CosColim-NatSq1 : CosCocEq F U (Map-to-Lim-map (PostComp ColCoC (f , fₚ))) (PostComp ColCoC (φ ∘* (f , fₚ)))
W CosColim-NatSq1 = λ i x → idp
u CosColim-NatSq1 = λ i a → ap-∘-∙ φ₁ f (! (glue (cin i a))) (fₚ a)
u CosColim-NatSq1 = λ i a → ap-∘-∙-∙ φ₁ f (! (glue (cin i a))) (fₚ a)
Λ CosColim-NatSq1 {i} {j} g = (λ x → ap-∘-rid φ₁ f (fst (comTri ColCoC g) x)) , λ a → lemma a
where
lemma : (a : A) →
Expand All @@ -133,7 +133,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type
ap φ₁ (ap f (fst (comTri ColCoC g) (fun (F # i) a))) ∙ idp) ∙
ap (φ₁ ∘ f ∘ fst (comp ColCoC j)) (snd (F <#> g) a) ∙
ap (φ₁ ∘ f) (snd (comp ColCoC j) a) ∙
snd (φ ∘* f , fₚ) a) (ap-∘-∙ φ₁ f (! (glue (cin j a))) (fₚ a)) ◃∙
snd (φ ∘* f , fₚ) a) (ap-∘-∙-∙ φ₁ f (! (glue (cin j a))) (fₚ a)) ◃∙
long-path-red (snd (F <#> g) a) (ap (φ₁ ∘ f) (! (glue (cin j a))) ∙
ap (fst φ) (fₚ a) ∙ snd φ a) (ap (fst φ) (ap f (! (glue (cin j a))) ∙ fₚ a) ∙ snd φ a)
(ap φ₁ (ap f (ap right (cglue g (fun (F # i) a))))) idp ◃∙ -- here
Expand All @@ -143,7 +143,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type
(ap-cp-revR f (fst (comp ColCoC j)) (snd (F <#> g) a)
(fst (comTri ColCoC g) (fun (F # i) a)) ∙
ap (λ p → p ∙ fₚ a) (ap (ap f) (snd (comTri ColCoC g) a)))) ◃∙
ap-∘-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
ap-∘-∙-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
=ₛ
(ap-cp-revR (φ₁ ∘ f) (fst (comp ColCoC j))
(snd (F <#> g) a) (fst (comTri ColCoC g) (fun (F # i) a)) ∙
Expand All @@ -165,7 +165,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type
ap φ₁ (ap f (fst (comTri ColCoC g) (fun (F # i) a))) ∙ idp) ∙
ap (φ₁ ∘ f ∘ fst (comp ColCoC j)) (snd (F <#> g) a) ∙
ap (φ₁ ∘ f) (snd (comp ColCoC j) a) ∙
snd (φ ∘* f , fₚ) a) (ap-∘-∙ φ₁ f (! (glue (cin j a))) (fₚ a)) ◃∙
snd (φ ∘* f , fₚ) a) (ap-∘-∙-∙ φ₁ f (! (glue (cin j a))) (fₚ a)) ◃∙
long-path-red (snd (F <#> g) a) (ap (φ₁ ∘ f) (! (glue (cin j a))) ∙
ap (fst φ) (fₚ a) ∙ snd φ a) (ap (fst φ) (ap f (! (glue (cin j a))) ∙ fₚ a) ∙ snd φ a)
(ap φ₁ (ap f (ap right (cglue g (fun (F # i) a))))) idp ◃∙
Expand All @@ -175,7 +175,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type
(ap-cp-revR f (fst (comp ColCoC j)) (snd (F <#> g) a)
(fst (comTri ColCoC g) (fun (F # i) a)) ∙
ap (λ p → p ∙ fₚ a) (ap (ap f) (snd (comTri ColCoC g) a)))) ◃∙
ap-∘-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
ap-∘-∙-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
=ₛ⟨ 0 & 4 & NatSq-1-Λ-red g a (ap right (cglue g (fun (F # i) a))) (snd (F <#> g) a) (! (glue (cin j a))) (fₚ a) (φ₂ a) ⟩
↯ (NatSq-1-Λ-aux g a (ap right (cglue g (fun (F # i) a))) (snd (F <#> g) a) (! (glue (cin j a))) (fₚ a) (φ₂ a)) ◃∙
ap (λ q → q) (ap-cp-revR φ₁ (f ∘ fst (comp ColCoC j)) (snd (F <#> g) a)
Expand All @@ -184,7 +184,7 @@ module _ {ℓv ℓe ℓ ℓd ℓc₁ ℓc₂} {Γ : Graph ℓv ℓe} {A : Type
(ap-cp-revR f (fst (comp ColCoC j)) (snd (F <#> g) a)
(fst (comTri ColCoC g) (fun (F # i) a)) ∙
ap (λ p → p ∙ fₚ a) (ap (ap f) (snd (comTri ColCoC g) a)))) ◃∙
ap-∘-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
ap-∘-∙-∙ φ₁ f (! (glue (cin i a))) (fₚ a) ◃∎
=ₛ⟨ NatSq-1-Λ-red2 g a (ap right (cglue g (fun (F # i) a))) (snd (F <#> g) a) (! (glue (cin j a))) (snd (comTri ColCoC g) a) ⟩
(ap-cp-revR (φ₁ ∘ f) (fst (comp ColCoC j))
(snd (F <#> g) a) (fst (comTri ColCoC g) (fun (F # i) a)) ∙
Expand Down
2 changes: 1 addition & 1 deletion Colimit-code/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ check the entire development in a reasonable amount of time.

## Manual Type-Checking

1. Install Agda 2.6.3.
1. Install Agda 2.6.4.3.
2. Install the stripped, modified HoTT-Agda library under `../HoTT-Agda`.
3. Type-check the file `Main-Theorem/CosColim-Adjunction.agda`.

Expand Down
4 changes: 2 additions & 2 deletions Dockerfile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@ ARG GHC_VERSION=9.4.7
FROM fossa/haskell-static-alpine:ghc-${GHC_VERSION} AS agda

WORKDIR /build/agda
# Agda 2.6.3
ARG AGDA_VERSION=b499d12412bac32ab1af9f470463ed9dc54f8907
# Agda 2.6.4.3
ARG AGDA_VERSION=714c7d2c76c5ffda3180e95c28669259f0dc5b5c
RUN \
git init && \
git remote add origin https://github.com/agda/agda.git && \
Expand Down
2 changes: 1 addition & 1 deletion HoTT-Agda/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ lemmas. The structure of the source code is described below.
Setup
-----

The library is compatible with Agda 2.6.3. To use it, you need a recent version of Agda and to include at
The library is compatible with Agda 2.6.4.3. To use it, you need a recent version of Agda and to include at
least the path to `hott-core.agda-lib` in your Agda library list.

Agda Options
Expand Down
10 changes: 5 additions & 5 deletions HoTT-Agda/core/lib/PathOver.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -385,22 +385,22 @@ module _ {i j} {X : Ptd i} {Y : Ptd j} where

infixr 30 _⊙-comp_
_⊙-comp_ : (f g : X ⊙→ Y) → Type (lmax i j)
_⊙-comp_ f g = Σ (fst f ∼ fst g) λ H → ! (H (pt X)) ∙ snd f =-= snd g
_⊙-comp_ f g = Σ (fst f ∼ fst g) λ H → ! (H (pt X)) ∙ snd f == snd g

comp-⊙∼ : {f g : X ⊙→ Y} (H : f ⊙∼ g) → ! (fst H (pt X)) ∙ snd f =-= snd g
comp-⊙∼ {f = f} H = ! (transp-cst=idf-l (fst H (pt X)) (snd f)) ◃∙ to-transp (snd H) ◃∎
comp-⊙∼ : {f g : X ⊙→ Y} (H : f ⊙∼ g) → ! (fst H (pt X)) ∙ snd f == snd g
comp-⊙∼ {f = f} H = ! (transp-cst=idf-l (fst H (pt X)) (snd f)) ∙ to-transp (snd H)

⊙-to-comp : {f g : X ⊙→ Y} → f ⊙∼ g → f ⊙-comp g
⊙-to-comp H = fst H , comp-⊙∼ H

comp-to-⊙ : {f g : X ⊙→ Y} → f ⊙-comp g → f ⊙∼ g
fst (comp-to-⊙ H) = fst H
snd (comp-to-⊙ {f} H) =
from-transp (_== pt Y) (fst H (pt X)) (transp-cst=idf-l (fst H (pt X)) (snd f) ∙ ↯ (snd H))
from-transp (_== pt Y) (fst H (pt X)) (transp-cst=idf-l (fst H (pt X)) (snd f) ∙ snd H)

⊙id-to-comp : {f g : X ⊙→ Y} (p : f == g) → f ⊙-comp g
fst (⊙id-to-comp idp) = λ x → idp
snd (⊙id-to-comp idp) = idp ◃∎
snd (⊙id-to-comp idp) = idp

{- Various other lemmas -}

Expand Down
49 changes: 25 additions & 24 deletions HoTT-Agda/core/lib/types/Homogeneous.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ module _ {i} {X : Type i} where
has-sect⊙.sect⊙-eq (⊙∼-eval-sect (homog auto homog-idf)) =
⊙λ= (comp-to-⊙
((λ x → app= (ap (fst ∘ ⊙Ω-fmap) homog-idf ∙ ap fst ⊙Ω-fmap-idf) x) ,
pathseq))
↯ pathseq))
where
lemma : {m : ⊙[ X , f z ] ⊙→ ⊙[ X , f z ]} (τ : m == ⊙idf ⊙[ X , f z ])
→ ! (ap (λ u → u idp) (ap (fst ∘ ⊙Ω-fmap) τ) ∙ idp) ∙
Expand Down Expand Up @@ -117,58 +117,58 @@ module _ {i} {X : Type i} where
∼⊙homog= : (x : X) {g : Z → X}
{fₚ : f z == x} {gₚ : g z == x}
{H₁ H₂ : f == g}
{H₁ₚ : ! (app= H₁ z) ∙ fₚ =-= gₚ}
{H₂ₚ : ! (app= H₂ z) ∙ fₚ =-= gₚ}
{H₁ₚ : ! (app= H₁ z) ∙ fₚ == gₚ}
{H₂ₚ : ! (app= H₂ z) ∙ fₚ == gₚ}
→ H₁ == H₂ → (app= H₁ , H₁ₚ) ⊙→∼ (app= H₂ , H₂ₚ)
fst (∼⊙homog= x {fₚ = idp} {H₁ = idp} {H₁ₚ = H₁ₚ} {H₂ₚ} idp) =
λ x₁ → app= (fst (r-inv (⊙∼-evalΩ-sect η))
(ap-post∙idp∘!-inv (↯ (H₁ₚ) ∙ ! (↯ (H₂ₚ))))) x₁
(ap-post∙idp∘!-inv (H₁ₚ ∙ ! (H₂ₚ)))) x₁
snd (∼⊙homog= x {fₚ = idp} {H₁ = idp} {H₁ₚ = H₁ₚ} {H₂ₚ} idp) =
post↯-rotate-in (=ₛ-in (ap (ap (λ p → ! p ∙ idp))
(app= (ap fst (sect⊙-eq (⊙∼-evalΩ-sect η)))
(ap-post∙idp∘!-inv (↯ (H₁ₚ) ∙ ! (↯ (H₂ₚ))))) ∙
(ap-post∙idp∘!-inv (H₁ₚ ∙ ! (H₂ₚ)))) ∙
<–-inv-r (ap-equiv (post∙idp∘!-is-equiv) idp idp)
(↯ (H₁ₚ) ∙ ! (↯ (H₂ₚ)))))
(H₁ₚ ∙ ! (H₂ₚ))))

∼⊙homog∼ : (x : X) {g : Z → X}
{fₚ : f z == x} {gₚ : g z == x}
{H₁ H₂ : f ∼ g}
{H₁ₚ : ! (H₁ z) ∙ fₚ =-= gₚ}
{H₂ₚ : ! (H₂ z) ∙ fₚ =-= gₚ}
{H₁ₚ : ! (H₁ z) ∙ fₚ == gₚ}
{H₂ₚ : ! (H₂ z) ∙ fₚ == gₚ}
→ H₁ ∼ H₂ → (H₁ , H₁ₚ) ⊙→∼ (H₂ , H₂ₚ)
fst (∼⊙homog∼ x {fₚ = idp} {gₚ} {H₁} {H₂} {H₁ₚ} {H₂ₚ} K) t =
! (app=-β H₁ t) ∙
fst (∼⊙homog= x {fₚ = idp} {gₚ = gₚ} {H₁ = λ= H₁} {H₂ = λ= H₂}
{H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ ↯ (H₁ₚ)) ◃∎}
{H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ ↯ (H₂ₚ)) ◃∎}
{H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ H₁ₚ)}
{H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ H₂ₚ)}
(ap λ= (λ= K))) t ∙
app=-β H₂ t
snd (∼⊙homog∼ x {fₚ = idp} {gₚ} {H₁} {H₂} {H₁ₚ} {H₂ₚ} K) =
ap (λ p → ! p ∙ idp) (! (app=-β H₁ z) ∙
fst (∼⊙homog= (f z) {fₚ = idp} {gₚ = gₚ} {H₁ = λ= H₁} {H₂ = λ= H₂}
{H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ ↯ (H₁ₚ)) ◃∎}
{H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ ↯ (H₂ₚ)) ◃∎}
{H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ H₁ₚ)}
{H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ H₂ₚ)}
(ap λ= (λ= K))) z ∙ app=-β H₂ z) ◃∙
H₂ₚ
H₂ₚ ◃∎
=ₛ₁⟨ 0 & 1 & ap-!∙∙ (λ p → ! p ∙ idp) (app=-β H₁ z)
(fst (∼⊙homog= (f z) {fₚ = idp} {gₚ = gₚ} {H₁ = λ= H₁} {H₂ = λ= H₂}
{H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ ↯ (H₁ₚ)) ◃∎}
{H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ ↯ (H₂ₚ)) ◃∎}
{H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ H₁ₚ)}
{H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ H₂ₚ)}
(ap λ= (λ= K))) z) (app=-β H₂ z) ⟩
↯ (! (ap (λ p → ! p ∙ idp) (app=-β H₁ z)) ◃∙
ap (λ p → ! p ∙ idp) (fst (∼⊙homog= (f z) {fₚ = idp} {gₚ = gₚ}
{H₁ = λ= H₁} {H₂ = λ= H₂}
{H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ ↯ (H₁ₚ)) ◃∎}
{H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ ↯ (H₂ₚ)) ◃∎}
{H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ H₁ₚ)}
{H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ H₂ₚ)}
(ap λ= (λ= K))) z) ◃∙
ap (λ p → ! p ∙ idp) (app=-β H₂ z) ◃∎) ◃∙ H₂ₚ
ap (λ p → ! p ∙ idp) (app=-β H₂ z) ◃∎) ◃∙ H₂ₚ ◃∎
=ₛ⟨ pre-rotate-in-↯-assoc
(snd (∼⊙homog= x
{fₚ = idp} {gₚ = gₚ} {H₁ = λ= H₁} {H₂ = λ= H₂}
{H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ ↯ (H₁ₚ)) ◃∎}
{H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ ↯ (H₂ₚ)) ◃∎}
{H₁ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₁ z) ∙ H₁ₚ)}
{H₂ₚ = (ap (λ p → ! p ∙ idp) (app=-β H₂ z) ∙ H₂ₚ)}
(ap λ= (λ= K)))) ⟩
H₁ₚ ∎ₛ
H₁ₚ ◃∎ ∎ₛ

-- All loop spaces are coherently homogeneous.

Expand All @@ -183,12 +183,13 @@ module _ {i} {X : Type i} {x : X} where
snd (auto loop-homog q) = post∙-is-equiv (! p ∙ q)
homog-idf loop-homog =
⊙λ= (comp-to-⊙ ((λ x₁ → ap (λ c → x₁ ∙ c) (!-inv-l p) ∙ ∙-unit-r x₁) ,
!-inv-l-r-unit-assoc p ◃∎))
!-inv-l-r-unit-assoc p))

∼⊙Ωhomog∼ : ∀ {j} {Z : Ptd j} {p : x == x}
{f g : Z ⊙→ ⊙[ x == x , p ]}
{H₁ H₂ : fst f ∼ fst g}
{H₁ₚ : ! (H₁ (pt Z)) ∙ snd f =-= snd g}
{H₂ₚ : ! (H₂ (pt Z)) ∙ snd f =-= snd g}
{H₁ₚ : ! (H₁ (pt Z)) ∙ snd f == snd g}
{H₂ₚ : ! (H₂ (pt Z)) ∙ snd f == snd g}
→ H₁ ∼ H₂ → (H₁ , H₁ₚ) ⊙→∼ (H₂ , H₂ₚ)
∼⊙Ωhomog∼ {Z = Z} {p} {f} K = ∼⊙homog∼ (loop-homog {p = fst f (pt Z)}) p K

40 changes: 20 additions & 20 deletions HoTT-Agda/core/lib/types/Pointed.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,27 +60,27 @@ module _ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} where
→ ((h ⊙∘ g) ⊙∘ f) ⊙-comp (h ⊙∘ (g ⊙∘ f))
fst (⊙∘-assoc-comp (h , hpt) (g , gpt) (f , fpt)) = λ x → idp
snd (⊙∘-assoc-comp (h , hpt) (g , gpt) (f , fpt)) =
! (∙-assoc (ap (h ∘ g) fpt) (ap h gpt) hpt) ◃∙
ap (λ p → p ∙ hpt) (ap (λ p → p ∙ ap h gpt) (ap-∘ h g fpt)) ◃∙
ap (λ p → p ∙ hpt) (∙-ap h (ap g fpt) gpt) ◃∎
! (∙-assoc (ap (h ∘ g) fpt) (ap h gpt) hpt) ∙
ap (λ p → p ∙ hpt) (ap (λ p → p ∙ ap h gpt) (ap-∘ h g fpt)) ∙
ap (λ p → p ∙ hpt) (∙-ap h (ap g fpt) gpt)

-- pre- and post-comp on (unfolded) homotopies of pointed maps

⊙∘-post : {f₁ f₂ : X ⊙→ Y} (g : Y ⊙→ Z) (H : f₁ ⊙-comp f₂) → g ⊙∘ f₁ ⊙-comp g ⊙∘ f₂
fst (⊙∘-post g H) = λ x → ap (fst g) (fst H x)
snd (⊙∘-post {f₁} g H) =
! (∙-assoc (! (ap (fst g) (fst H (pt X)))) (ap (fst g) (snd f₁)) (snd g)) ◃∙
ap (λ p → p ∙ snd g) (!-ap-∙ (fst g) (fst H (pt X)) (snd f₁)) ◃∙
ap (λ p → p ∙ snd g) (ap (ap (fst g)) (↯ (snd H))) ◃∎
! (∙-assoc (! (ap (fst g) (fst H (pt X)))) (ap (fst g) (snd f₁)) (snd g)) ∙
ap (λ p → p ∙ snd g) (!-ap-∙ (fst g) (fst H (pt X)) (snd f₁)) ∙
ap (λ p → p ∙ snd g) (ap (ap (fst g)) (snd H))

⊙∘-pre : {f₁ f₂ : X ⊙→ Y} (g : Z ⊙→ X) (H : f₁ ⊙-comp f₂) → f₁ ⊙∘ g ⊙-comp f₂ ⊙∘ g
fst (⊙∘-pre g H) = λ x → fst H (fst g x)
snd (⊙∘-pre {f₁} {f₂} g H) =
! (∙-assoc (! (fst H (fst g (pt Z)))) (ap (fst f₁) (snd g)) (snd f₁)) ◃∙
ap (λ p → p ∙ snd f₁) (hmtpy-nat-!-sq (fst H) (snd g)) ◃∙
∙-assoc (ap (fst f₂) (snd g)) (! (fst H (pt X))) (snd f₁) ◃∙
ap (λ p → ap (fst f₂) (snd g) ∙ p) (↯ (snd H)) ◃∎

! (∙-assoc (! (fst H (fst g (pt Z)))) (ap (fst f₁) (snd g)) (snd f₁)) ∙
ap (λ p → p ∙ snd f₁) (hmtpy-nat-!-sq (fst H) (snd g)) ∙
∙-assoc (ap (fst f₂) (snd g)) (! (fst H (pt X))) (snd f₁) ∙
ap (λ p → ap (fst f₂) (snd g) ∙ p) (snd H)
-- concatenation of homotopies of pointed maps

module _ {i j} {X : Ptd i} {Y : Ptd j} {f₁ f₂ f₃ : X ⊙→ Y} where
Expand All @@ -89,9 +89,9 @@ module _ {i j} {X : Ptd i} {Y : Ptd j} {f₁ f₂ f₃ : X ⊙→ Y} where
_∙⊙∼_ : f₁ ⊙-comp f₂ → f₂ ⊙-comp f₃ → f₁ ⊙-comp f₃
fst (H₁ ∙⊙∼ H₂) = λ x → fst H₁ x ∙ fst H₂ x
snd (H₁ ∙⊙∼ H₂) =
ap (λ p → ! (p ∙ fst H₂ (pt X)) ∙ snd f₁) (tri-exch (↯ (snd H₁))) ◃∙
ap (λ p → ! ((snd f₁ ∙ ! (snd f₂)) ∙ p) ∙ snd f₁) (tri-exch (↯ (snd H₂))) ◃∙
!3-∙3 (snd f₁) (snd f₂) (snd f₃) ◃∎
ap (λ p → ! (p ∙ fst H₂ (pt X)) ∙ snd f₁) (tri-exch (snd H₁)) ∙
ap (λ p → ! ((snd f₁ ∙ ! (snd f₂)) ∙ p) ∙ snd f₁) (tri-exch (snd H₂)) ∙
!3-∙3 (snd f₁) (snd f₂) (snd f₃)

-- inverse of homotopy of pointed maps

Expand All @@ -100,16 +100,16 @@ module _ {i j} {X : Ptd i} {Y : Ptd j} where
!-⊙∼ : {f₁ f₂ : X ⊙→ Y} (H : f₁ ⊙-comp f₂) → f₂ ⊙-comp f₁
fst (!-⊙∼ (H₀ , H₁)) x = ! (H₀ x)
snd (!-⊙∼ {f₁} {f₂} (H₀ , H₁)) =
ap (λ p → p ∙ snd f₂) (!-! (H₀ (pt (X)))) ◃∙
ap (λ p → H₀ (pt X) ∙ p) (↯ (seq-! H₁)) ◃∙
! (∙-assoc (H₀ (pt X)) (! (H₀ (pt X))) (snd f₁)) ◃∙
ap (λ p → p ∙ snd f₁) (!-inv-r (H₀ (pt X))) ◃∎
ap (λ p → p ∙ snd f₂) (!-! (H₀ (pt (X)))) ∙
ap (λ p → H₀ (pt X) ∙ p) (! H₁) ∙
! (∙-assoc (H₀ (pt X)) (! (H₀ (pt X))) (snd f₁)) ∙
ap (λ p → p ∙ snd f₁) (!-inv-r (H₀ (pt X)))

-- identity homotopy of pointed maps

⊙∼-id : (f : X ⊙→ Y) → f ⊙-comp f
fst (⊙∼-id (f , fₚ)) x = idp
snd (⊙∼-id (f , fₚ)) = idp ◃∎
snd (⊙∼-id (f , fₚ)) = idp

-- homotopies of homotopies of pointed maps

Expand All @@ -119,7 +119,7 @@ module _ {i j} {X : Ptd i} {Y : Ptd j} where
_⊙→∼_ : {f g : X ⊙→ Y} (H₁ H₂ : f ⊙-comp g) → Type (lmax i j)
_⊙→∼_ {f = f} H₁ H₂ =
Σ (fst H₁ ∼ fst H₂)
(λ K → ap (λ p → ! p ∙ snd f) (K (pt X)) ◃∙ snd H₂ =ₛ snd H₁)
(λ K → ap (λ p → ! p ∙ snd f) (K (pt X)) ◃∙ snd H₂ ◃∎ =ₛ snd H₁ ◃∎)

-- pointed sections

Expand Down
Loading
Loading