Refactoring pointed types

src/foundation-core/commuting-squares-of-homotopies.lagda.md

@@ -37,7 +37,9 @@ homotopy is called a
 {{#concept "coherence" Disambiguation="commuting square of homotopies" Agda=coherence-square-homotopies}}
 of the square.
 
-## Definition
+## Definitions
+
+### Commuting squares of homotopies
 
 ```agda
 module _

src/foundation-core/constant-maps.lagda.md

@@ -12,9 +12,24 @@ open import foundation.universe-levels
 
 </details>
 
+## Idea
+
+The {{#concept "constant map" Agda=const}} from `A` to `B` at an element `b : B`
+is the function `x ↦ b` mapping every element `x : A` to the given element
+`b : B`. In common type theoretic notation, the constant map at `b` is the
+function
+
+```text
+  λ x → b.
+```
+
 ## Definition
 
 ```agda
 const : {l1 l2 : Level} (A : UU l1) (B : UU l2) → B → A → B
 const A B b x = b
 ```
+
+## See also
+
+- [Constant pointed maps](structured-types.constant-pointed-maps.md)

src/foundation-core/homotopies.lagda.md

@@ -274,6 +274,18 @@ inv-nat-htpy :
   ap f p ∙ H y ＝ H x ∙ ap g p
 inv-nat-htpy H p = inv (nat-htpy H p)
 
+nat-refl-htpy :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  {x y : A} (p : x ＝ y) →
+  nat-htpy (refl-htpy' f) p ＝ inv right-unit
+nat-refl-htpy f refl = refl
+
+inv-nat-refl-htpy :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  {x y : A} (p : x ＝ y) →
+  inv-nat-htpy (refl-htpy' f) p ＝ right-unit
+inv-nat-refl-htpy f refl = refl
+
 nat-htpy-id :
   {l : Level} {A : UU l} {f : A → A} (H : f ~ id)
   {x y : A} (p : x ＝ y) → H x ∙ p ＝ ap f p ∙ H y

src/foundation-core/identity-types.lagda.md

@@ -231,6 +231,8 @@ use of the fact that the identity types are defined _for all types_. In other
 words, since identity types are themselves types, we can consider identity types
 of identity types, and so on.
 
+#### Associators
+
 ```agda
 module _
   {l : Level} {A : UU l}
@@ -264,6 +266,21 @@ module _
   {l : Level} {A : UU l}
   where
 
+  double-assoc :
+    {x y z w v : A} (p : x ＝ y) (q : y ＝ z) (r : z ＝ w) (s : w ＝ v) →
+    (((p ∙ q) ∙ r) ∙ s) ＝ p ∙ (q ∙ (r ∙ s))
+  double-assoc refl q r s = assoc q r s
+
+  triple-assoc :
+    {x y z w v u : A}
+    (p : x ＝ y) (q : y ＝ z) (r : z ＝ w) (s : w ＝ v) (t : v ＝ u) →
+    ((((p ∙ q) ∙ r) ∙ s) ∙ t) ＝ p ∙ (q ∙ (r ∙ (s ∙ t)))
+  triple-assoc refl q r s t = double-assoc q r s t
+```
+
+#### Unit laws
+
+```agda
   left-unit : {x y : A} {p : x ＝ y} → refl ∙ p ＝ p
   left-unit = refl
 
@@ -387,11 +404,21 @@ module _
     p ∙ q ＝ r → q ＝ inv p ∙ r
   left-transpose-eq-concat refl q r s = s
 
+  inv-left-transpose-eq-concat :
+    {x y : A} (p : x ＝ y) {z : A} (q : y ＝ z) (r : x ＝ z) →
+    q ＝ inv p ∙ r → p ∙ q ＝ r
+  inv-left-transpose-eq-concat refl q r s = s
+
   right-transpose-eq-concat :
     {x y : A} (p : x ＝ y) {z : A} (q : y ＝ z) (r : x ＝ z) →
     p ∙ q ＝ r → p ＝ r ∙ inv q
   right-transpose-eq-concat p refl r s = (inv right-unit ∙ s) ∙ inv right-unit
 
+  inv-right-transpose-eq-concat :
+    {x y : A} (p : x ＝ y) {z : A} (q : y ＝ z) (r : x ＝ z) →
+    p ＝ r ∙ inv q → p ∙ q ＝ r
+  inv-right-transpose-eq-concat p refl r s = right-unit ∙ (s ∙ right-unit)
+
   double-transpose-eq-concat :
     {x y u v : A} (r : x ＝ u) (p : x ＝ y) (s : u ＝ v) (q : y ＝ v) →
     p ∙ q ＝ r ∙ s → (inv r) ∙ p ＝ s ∙ (inv q)