From 37dba435a2efb1ce6a343b03c25023c288161530 Mon Sep 17 00:00:00 2001 From: Mabel Najdovski Date: Tue, 31 Oct 2023 10:52:01 +0100 Subject: [PATCH] Renaming and fix indentation --- .../smash-products-of-pointed-types.lagda.md | 60 +++++++++++-------- .../wedges-of-pointed-types.lagda.md | 8 +-- 2 files changed, 39 insertions(+), 29 deletions(-) diff --git a/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md index 37b62076a5..8fa69c7b96 100644 --- a/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md +++ b/src/synthetic-homotopy-theory/smash-products-of-pointed-types.lagda.md @@ -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} @@ -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)) @@ -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 : @@ -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 : @@ -258,20 +258,23 @@ 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) @@ -279,7 +282,9 @@ module _ ( 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)))) ∙ @@ -287,8 +292,11 @@ module _ ( 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)) @@ -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)) @@ -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)))) ``` diff --git a/src/synthetic-homotopy-theory/wedges-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/wedges-of-pointed-types.lagda.md index 2e21c37142..b78c57bca8 100644 --- a/src/synthetic-homotopy-theory/wedges-of-pointed-types.lagda.md +++ b/src/synthetic-homotopy-theory/wedges-of-pointed-types.lagda.md @@ -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)