Skip to content

Commit

Permalink
Renaming and fix indentation
Browse files Browse the repository at this point in the history
  • Loading branch information
@maybemabeline
maybemabeline committed Oct 31, 2023
1 parent deff983 commit 37dba43
Show file tree
Hide file tree
Showing 2 changed files with 39 additions and 29 deletions.
60 changes: 35 additions & 25 deletions src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -158,11 +158,11 @@ module _
map-smash-prod-wedge-Pointed-Type =
map-pointed-map pointed-map-smash-prod-wedge-Pointed-Type

eq-map-smash-prod-wedge-Pointed-Type :
contraction-map-smash-prod-wedge-Pointed-Type :
( x : type-Pointed-Type (A ∨∗ B)) →
map-smash-prod-wedge-Pointed-Type x ＝
point-Pointed-Type (A ∧∗ B)
eq-map-smash-prod-wedge-Pointed-Type x =
contraction-map-smash-prod-wedge-Pointed-Type x =
( glue-pushout
( map-prod-wedge-Pointed-Type A B)
( map-pointed-map {A = A ∨∗ B} {B = unit-Pointed-Type}
Expand All @@ -184,29 +184,29 @@ module _
( preserves-point-pointed-map
( inclusion-point-Pointed-Type (A ∧∗ B)))

coh-eq-map-smash-prod-wedge-Pointed-Type :
coh-contraction-map-smash-prod-wedge-Pointed-Type :
( ap
( map-smash-prod-wedge-Pointed-Type)
( glue-wedge-Pointed-Type A B)) ∙
( eq-map-smash-prod-wedge-Pointed-Type
( contraction-map-smash-prod-wedge-Pointed-Type
( map-inr-wedge-Pointed-Type A B (point-Pointed-Type B))) ＝
( eq-map-smash-prod-wedge-Pointed-Type
( contraction-map-smash-prod-wedge-Pointed-Type
( map-inl-wedge-Pointed-Type A B (point-Pointed-Type A)))
coh-eq-map-smash-prod-wedge-Pointed-Type =
coh-contraction-map-smash-prod-wedge-Pointed-Type =
( inv-map-compute-dependent-identification-eq-value-function
( map-smash-prod-wedge-Pointed-Type)
( map-pointed-map
( constant-pointed-map (A ∨∗ B) (A ∧∗ B)))
( glue-wedge-Pointed-Type A B)
( eq-map-smash-prod-wedge-Pointed-Type
( contraction-map-smash-prod-wedge-Pointed-Type
( map-inl-wedge-Pointed-Type A B (point-Pointed-Type A)))
( eq-map-smash-prod-wedge-Pointed-Type
( contraction-map-smash-prod-wedge-Pointed-Type
( map-inr-wedge-Pointed-Type A B (point-Pointed-Type B)))
( apd
( eq-map-smash-prod-wedge-Pointed-Type)
( contraction-map-smash-prod-wedge-Pointed-Type)
( glue-wedge-Pointed-Type A B))) ∙
( identification-left-whisk
( eq-map-smash-prod-wedge-Pointed-Type
( contraction-map-smash-prod-wedge-Pointed-Type
( map-inl-wedge-Pointed-Type A B (point-Pointed-Type A)))
( ap-const
( point-Pointed-Type (A ∧∗ B))
Expand Down Expand Up @@ -234,8 +234,8 @@ module _
inl-glue-smash-prod-Pointed-Type x =
( ap
( map-smash-prod-prod-Pointed-Type A B)
( inv (inl-prod-wedge-Pointed-Type A B x))) ∙
( eq-map-smash-prod-wedge-Pointed-Type A B
( inv (compute-inl-prod-wedge-Pointed-Type A B x))) ∙
( contraction-map-smash-prod-wedge-Pointed-Type A B
( map-inl-wedge-Pointed-Type A B x))

inr-glue-smash-prod-Pointed-Type :
Expand All @@ -247,8 +247,8 @@ module _
inr-glue-smash-prod-Pointed-Type y =
( ap
( map-smash-prod-prod-Pointed-Type A B)
( inv (inr-prod-wedge-Pointed-Type A B y))) ∙
( eq-map-smash-prod-wedge-Pointed-Type A B
( inv (compute-inr-prod-wedge-Pointed-Type A B y))) ∙
( contraction-map-smash-prod-wedge-Pointed-Type A B
( map-inr-wedge-Pointed-Type A B y))

coh-glue-smash-prod-Pointed-Type :
Expand All @@ -258,37 +258,45 @@ module _
( identification-left-whisk
( ap
( map-smash-prod-prod-Pointed-Type A B)
( inv (inl-prod-wedge-Pointed-Type A B (point-Pointed-Type A))))
( inv (coh-eq-map-smash-prod-wedge-Pointed-Type A B))) ∙
( inv (compute-inl-prod-wedge-Pointed-Type A B (point-Pointed-Type A))))
( inv (coh-contraction-map-smash-prod-wedge-Pointed-Type A B))) ∙
( inv
( assoc
( ap (map-smash-prod-prod-Pointed-Type A B)
( inv (inl-prod-wedge-Pointed-Type A B (point-Pointed-Type A))))
( inv
( compute-inl-prod-wedge-Pointed-Type A B (point-Pointed-Type A))))
( ap (map-smash-prod-wedge-Pointed-Type A B)
( glue-wedge-Pointed-Type A B))
( eq-map-smash-prod-wedge-Pointed-Type A B
( contraction-map-smash-prod-wedge-Pointed-Type A B
( map-inr-wedge-Pointed-Type A B (point-Pointed-Type B))))) ∙
( identification-right-whisk
( ( identification-left-whisk
( ap (map-smash-prod-prod-Pointed-Type A B)
( inv (inl-prod-wedge-Pointed-Type A B (point-Pointed-Type A))))
( inv
( compute-inl-prod-wedge-Pointed-Type A B
( point-Pointed-Type A))))
( ap-comp
( map-smash-prod-prod-Pointed-Type A B)
( map-prod-wedge-Pointed-Type A B)
( glue-wedge-Pointed-Type A B))) ∙
( inv
( ap-concat
( map-smash-prod-prod-Pointed-Type A B)
( inv (inl-prod-wedge-Pointed-Type A B (point-Pointed-Type A)))
( inv
( compute-inl-prod-wedge-Pointed-Type A B
( point-Pointed-Type A)))
( ap
( map-prod-wedge-Pointed-Type A B)
( glue-wedge-Pointed-Type A B)))) ∙
( ap²
( map-smash-prod-prod-Pointed-Type A B)
( inv
( left-transpose-eq-concat
( inl-prod-wedge-Pointed-Type A B (point-Pointed-Type A))
( inv (inr-prod-wedge-Pointed-Type A B (point-Pointed-Type B)))
( compute-inl-prod-wedge-Pointed-Type A B
( point-Pointed-Type A))
( inv
( compute-inr-prod-wedge-Pointed-Type A B
( point-Pointed-Type B)))
( ap
( map-prod-wedge-Pointed-Type A B)
( glue-wedge-Pointed-Type A B))
Expand All @@ -297,8 +305,10 @@ module _
( ap
( map-prod-wedge-Pointed-Type A B)
( glue-wedge-Pointed-Type A B))
( inr-prod-wedge-Pointed-Type A B (point-Pointed-Type B))
( inl-prod-wedge-Pointed-Type A B (point-Pointed-Type A))
( compute-inr-prod-wedge-Pointed-Type A B
( point-Pointed-Type B))
( compute-inl-prod-wedge-Pointed-Type A B
( point-Pointed-Type A))
( ( compute-glue-cogap
( map-pointed-map
( inclusion-point-Pointed-Type A))
Expand All @@ -310,7 +320,7 @@ module _
( cocone-prod-wedge-Pointed-Type A B))
( point-Pointed-Type unit-Pointed-Type)) ∙
( right-unit))))))))
( eq-map-smash-prod-wedge-Pointed-Type A B
( contraction-map-smash-prod-wedge-Pointed-Type A B
( map-inr-wedge-Pointed-Type A B (point-Pointed-Type B))))
```

Expand Down
8 changes: 4 additions & 4 deletions src/synthetic-homotopy-theory/wedges-of-pointed-types.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -152,21 +152,21 @@ module _
type-Pointed-Type (A ∨∗ B) → type-Pointed-Type (A ×∗ B)
map-prod-wedge-Pointed-Type = pr1 pointed-map-prod-wedge-Pointed-Type

inl-prod-wedge-Pointed-Type :
compute-inl-prod-wedge-Pointed-Type :
( x : type-Pointed-Type A) →
( map-prod-wedge-Pointed-Type (map-inl-wedge-Pointed-Type A B x)) ＝
( x , point-Pointed-Type B)
inl-prod-wedge-Pointed-Type =
compute-inl-prod-wedge-Pointed-Type =
compute-inl-cogap-Pointed-Type
( inclusion-point-Pointed-Type A)
( inclusion-point-Pointed-Type B)
( cocone-prod-wedge-Pointed-Type)

inr-prod-wedge-Pointed-Type :
compute-inr-prod-wedge-Pointed-Type :
( y : type-Pointed-Type B) →
( map-prod-wedge-Pointed-Type (map-inr-wedge-Pointed-Type A B y)) ＝
( point-Pointed-Type A , y)
inr-prod-wedge-Pointed-Type =
compute-inr-prod-wedge-Pointed-Type =
compute-inr-cogap-Pointed-Type
( inclusion-point-Pointed-Type A)
( inclusion-point-Pointed-Type B)
Expand Down

0 comments on commit 37dba43

Please sign in to comment.