Define the noncoherent wild precategory of pointed types (#1179)

src/foundation/function-types.lagda.md

@@ -11,6 +11,7 @@ open import foundation-core.function-types public
 ```agda
 open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
+open import foundation.commuting-pentagons-of-identifications
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
 open import foundation.homotopy-induction
@@ -28,6 +29,38 @@ open import foundation-core.transport-along-identifications
 
 ## Properties
 
+### Associativity of function composition
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
+  (h : C → D) (g : B → C) (f : A → B)
+  where
+
+  associative-comp : (h ∘ g) ∘ f ＝ h ∘ (g ∘ f)
+  associative-comp = refl
+```
+
+### The Mac Lane pentagon for function composition
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5}
+  {f : A → B} {g : B → C} {h : C → D} {i : D → E}
+  where
+
+  mac-lane-pentagon-comp :
+    let α₁ = (ap (_∘ f) (associative-comp i h g))
+        α₂ = (associative-comp i (h ∘ g) f)
+        α₃ = (ap (i ∘_) (associative-comp h g f))
+        α₄ = (associative-comp (i ∘ h) g f)
+        α₅ = (associative-comp i h (g ∘ f))
+    in
+      coherence-pentagon-identifications α₁ α₄ α₂ α₅ α₃
+  mac-lane-pentagon-comp = refl
+```
+
 ### Transport in a family of function types
 
 Consider two type families `B` and `C` over `A`, an identification `p : x ＝ y`

src/structured-types.lagda.md

@@ -92,6 +92,7 @@ open import structured-types.universal-property-pointed-equivalences public
 open import structured-types.unpointed-maps public
 open import structured-types.whiskering-pointed-2-homotopies-concatenation public
 open import structured-types.whiskering-pointed-homotopies-composition public
+open import structured-types.wild-category-of-pointed-types public
 open import structured-types.wild-groups public
 open import structured-types.wild-loops public
 open import structured-types.wild-monoids public

src/structured-types/pointed-homotopies.lagda.md

@@ -284,6 +284,10 @@ module _
   concat-pointed-htpy : f ~∗ h
   pr1 concat-pointed-htpy = htpy-concat-pointed-htpy
   pr2 concat-pointed-htpy = coherence-point-concat-pointed-htpy
+
+  infixl 15 _∙h∗_
+  _∙h∗_ : f ~∗ h
+  _∙h∗_ = concat-pointed-htpy
 ```
 
 ### Inverses of pointed homotopies
@@ -554,6 +558,39 @@ module _
   pr2 is-binary-equiv-concat-pointed-htpy = is-equiv-concat-pointed-htpy
 ```
 
+## Reasoning with pointed homotopies
+
+Pointed homotopies can be constructed by equational reasoning in the following
+way:
+
+```text
+pointed-homotopy-reasoning
+  f ~∗ g by htpy-1
+    ~∗ h by htpy-2
+    ~∗ i by htpy-3
+```
+
+The pointed homotopy obtained in this way is `htpy-1 ∙h∗ (htpy-2 ∙h∗ htpy-3)`,
+i.e., it is associated fully to the right.
+
+```agda
+infixl 1 pointed-homotopy-reasoning_
+infixl 0 step-pointed-homotopy-reasoning
+
+pointed-homotopy-reasoning_ :
+  {l1 l2 : Level} {X : Pointed-Type l1} {Y : Pointed-Fam l2 X}
+  (f : pointed-Π X Y) → f ~∗ f
+pointed-homotopy-reasoning f = refl-pointed-htpy f
+
+step-pointed-homotopy-reasoning :
+  {l1 l2 : Level} {X : Pointed-Type l1} {Y : Pointed-Fam l2 X}
+  {f g : pointed-Π X Y} → f ~∗ g →
+  (h : pointed-Π X Y) → g ~∗ h → f ~∗ h
+step-pointed-homotopy-reasoning p h q = p ∙h∗ q
+
+syntax step-pointed-homotopy-reasoning p h q = p ~∗ h by q
+```
+
 ## See also
 
 - [Pointed 2-homotopies](structured-types.pointed-2-homotopies.md)

src/structured-types/wild-category-of-pointed-types.lagda.md

@@ -0,0 +1,274 @@
+# The wild category of pointed types
+
+```agda
+{-# OPTIONS --guardedness #-}
+
+module structured-types.wild-category-of-pointed-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.universe-levels
+open import foundation.whiskering-identifications-concatenation
+
+open import structured-types.globular-types
+open import structured-types.large-globular-types
+open import structured-types.large-reflexive-globular-types
+open import structured-types.large-transitive-globular-types
+open import structured-types.pointed-2-homotopies
+open import structured-types.pointed-dependent-functions
+open import structured-types.pointed-families-of-types
+open import structured-types.pointed-homotopies
+open import structured-types.pointed-maps
+open import structured-types.pointed-types
+open import structured-types.reflexive-globular-types
+open import structured-types.transitive-globular-types
+open import structured-types.uniform-pointed-homotopies
+
+open import wild-category-theory.noncoherent-large-wild-higher-precategories
+open import wild-category-theory.noncoherent-wild-higher-precategories
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "wild category of pointed types" Agda=uniform-Pointed-Type-Noncoherent-Large-Wild-Higher-Precategory Agda=Pointed-Type-Noncoherent-Large-Wild-Higher-Precategory}}
+consists of [pointed types](structured-types.pointed-types.md),
+[pointed functions](structured-types.pointed-maps.md), and
+[pointed homotopies](structured-types.pointed-homotopies.md).
+
+We give two equivalent definitions: the first uses
+[uniform pointed homotopies](structured-types.uniform-pointed-homotopies.md),
+giving a uniform definition for all higher cells. However, uniform pointed
+homotopies are not as workable directly as pointed homotopies, although the
+types are equivalent. Therefore we give a second, nonuniform definition of the
+wild category of pointed types where the 2-cells are pointed homotopies, the
+3-cells are [pointed 2-homotopies](structured-types.pointed-2-homotopies.md) and
+the higher cells are [identities](foundation-core.identity-types.md).
+
+## Definitions
+
+### The uniform definition of the wild category of pointed types
+
+#### The uniform globular structure on dependent pointed function types
+
+```agda
+uniform-globular-structure-pointed-Π :
+  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} →
+  globular-structure (l1 ⊔ l2) (pointed-Π A B)
+uniform-globular-structure-pointed-Π =
+  λ where
+  .1-cell-globular-structure →
+    uniform-pointed-htpy
+  .globular-structure-1-cell-globular-structure f g →
+    uniform-globular-structure-pointed-Π
+
+is-reflexive-uniform-globular-structure-pointed-Π :
+  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} →
+  is-reflexive-globular-structure
+    ( uniform-globular-structure-pointed-Π {A = A} {B})
+is-reflexive-uniform-globular-structure-pointed-Π =
+  λ where
+  .is-reflexive-1-cell-is-reflexive-globular-structure →
+    refl-uniform-pointed-htpy
+  .is-reflexive-globular-structure-1-cell-is-reflexive-globular-structure f g →
+    is-reflexive-uniform-globular-structure-pointed-Π
+
+is-transitive-uniform-globular-structure-pointed-Π :
+  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} →
+  is-transitive-globular-structure
+    ( uniform-globular-structure-pointed-Π {A = A} {B})
+is-transitive-uniform-globular-structure-pointed-Π =
+  λ where
+  .comp-1-cell-is-transitive-globular-structure {f} {g} {h} H K →
+    concat-uniform-pointed-htpy {f = f} {g} {h} K H
+  .is-transitive-globular-structure-1-cell-is-transitive-globular-structure
+    H K →
+    is-transitive-uniform-globular-structure-pointed-Π
+```
+
+#### The uniform large globular structure on pointed types
+
+```agda
+uniform-large-globular-structure-Pointed-Type :
+  large-globular-structure (_⊔_) Pointed-Type
+uniform-large-globular-structure-Pointed-Type =
+  λ where
+  .1-cell-large-globular-structure X Y →
+    (X →∗ Y)
+  .globular-structure-1-cell-large-globular-structure X Y →
+    uniform-globular-structure-pointed-Π
+
+is-reflexive-uniform-large-globular-structure-Pointed-Type :
+  is-reflexive-large-globular-structure
+    uniform-large-globular-structure-Pointed-Type
+is-reflexive-uniform-large-globular-structure-Pointed-Type =
+  λ where
+  .is-reflexive-1-cell-is-reflexive-large-globular-structure X →
+    id-pointed-map
+  .is-reflexive-globular-structure-1-cell-is-reflexive-large-globular-structure
+    X Y →
+    is-reflexive-uniform-globular-structure-pointed-Π
+
+is-transitive-uniform-large-globular-structure-Pointed-Type :
+  is-transitive-large-globular-structure
+    uniform-large-globular-structure-Pointed-Type
+is-transitive-uniform-large-globular-structure-Pointed-Type =
+  λ where
+  .comp-1-cell-is-transitive-large-globular-structure g f →
+    g ∘∗ f
+  .is-transitive-globular-structure-1-cell-is-transitive-large-globular-structure
+    X Y →
+    is-transitive-uniform-globular-structure-pointed-Π
+```
+
+#### The uniform noncoherent large wild higher precategory of pointed types
+
+```agda
+uniform-Pointed-Type-Noncoherent-Large-Wild-Higher-Precategory :
+  Noncoherent-Large-Wild-Higher-Precategory lsuc (_⊔_)
+uniform-Pointed-Type-Noncoherent-Large-Wild-Higher-Precategory =
+  λ where
+  .obj-Noncoherent-Large-Wild-Higher-Precategory →
+    Pointed-Type
+  .hom-globular-structure-Noncoherent-Large-Wild-Higher-Precategory →
+    uniform-large-globular-structure-Pointed-Type
+  .id-hom-globular-structure-Noncoherent-Large-Wild-Higher-Precategory →
+    is-reflexive-uniform-large-globular-structure-Pointed-Type
+  .comp-hom-globular-structure-Noncoherent-Large-Wild-Higher-Precategory →
+    is-transitive-uniform-large-globular-structure-Pointed-Type
+```
+
+### The nonuniform definition of the wild category of pointed types
+
+#### The nonuniform globular structure on dependent pointed function types
+
+```agda
+globular-structure-pointed-Π :
+  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} →
+  globular-structure (l1 ⊔ l2) (pointed-Π A B)
+globular-structure-pointed-Π =
+  λ where
+  .1-cell-globular-structure →
+    pointed-htpy
+  .globular-structure-1-cell-globular-structure f g
+    .1-cell-globular-structure →
+    pointed-2-htpy
+  .globular-structure-1-cell-globular-structure f g
+    .globular-structure-1-cell-globular-structure H K →
+      globular-structure-Id (pointed-2-htpy H K)
+
+is-reflexive-globular-structure-pointed-Π :
+  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} →
+  is-reflexive-globular-structure (globular-structure-pointed-Π {A = A} {B})
+is-reflexive-globular-structure-pointed-Π =
+  λ where
+  .is-reflexive-1-cell-is-reflexive-globular-structure →
+    refl-pointed-htpy
+  .is-reflexive-globular-structure-1-cell-is-reflexive-globular-structure f g
+    .is-reflexive-1-cell-is-reflexive-globular-structure →
+      refl-pointed-2-htpy
+  .is-reflexive-globular-structure-1-cell-is-reflexive-globular-structure f g
+    .is-reflexive-globular-structure-1-cell-is-reflexive-globular-structure
+      H K →
+      is-reflexive-globular-structure-Id (pointed-2-htpy H K)
+
+is-transitive-globular-structure-pointed-Π :
+  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} →
+  is-transitive-globular-structure (globular-structure-pointed-Π {A = A} {B})
+is-transitive-globular-structure-pointed-Π =
+  λ where
+  .comp-1-cell-is-transitive-globular-structure {f} {g} {h} H K →
+    concat-pointed-htpy {f = f} {g} {h} K H
+  .is-transitive-globular-structure-1-cell-is-transitive-globular-structure H K
+    .comp-1-cell-is-transitive-globular-structure α β →
+    concat-pointed-2-htpy β α
+  .is-transitive-globular-structure-1-cell-is-transitive-globular-structure H K
+    .is-transitive-globular-structure-1-cell-is-transitive-globular-structure
+      α β →
+      is-transitive-globular-structure-Id (pointed-2-htpy α β)
+```
+
+#### The uniform large globular structure on pointed types
+
+```agda
+large-globular-structure-Pointed-Type :
+  large-globular-structure (_⊔_) Pointed-Type
+large-globular-structure-Pointed-Type =
+  λ where
+  .1-cell-large-globular-structure X Y →
+    (X →∗ Y)
+  .globular-structure-1-cell-large-globular-structure X Y →
+    globular-structure-pointed-Π
+
+is-reflexive-large-globular-structure-Pointed-Type :
+  is-reflexive-large-globular-structure large-globular-structure-Pointed-Type
+is-reflexive-large-globular-structure-Pointed-Type =
+  λ where
+  .is-reflexive-1-cell-is-reflexive-large-globular-structure X →
+    id-pointed-map
+  .is-reflexive-globular-structure-1-cell-is-reflexive-large-globular-structure
+    X Y →
+    is-reflexive-globular-structure-pointed-Π
+
+is-transitive-large-globular-structure-Pointed-Type :
+  is-transitive-large-globular-structure large-globular-structure-Pointed-Type
+is-transitive-large-globular-structure-Pointed-Type =
+  λ where
+  .comp-1-cell-is-transitive-large-globular-structure g f →
+    g ∘∗ f
+  .is-transitive-globular-structure-1-cell-is-transitive-large-globular-structure
+    X Y →
+    is-transitive-globular-structure-pointed-Π
+```
+
+#### The nonuniform noncoherent large wild higher precategory of pointed types
+
+```agda
+Pointed-Type-Noncoherent-Large-Wild-Higher-Precategory :
+  Noncoherent-Large-Wild-Higher-Precategory lsuc (_⊔_)
+Pointed-Type-Noncoherent-Large-Wild-Higher-Precategory =
+  λ where
+  .obj-Noncoherent-Large-Wild-Higher-Precategory →
+    Pointed-Type
+  .hom-globular-structure-Noncoherent-Large-Wild-Higher-Precategory →
+    large-globular-structure-Pointed-Type
+  .id-hom-globular-structure-Noncoherent-Large-Wild-Higher-Precategory →
+    is-reflexive-large-globular-structure-Pointed-Type
+  .comp-hom-globular-structure-Noncoherent-Large-Wild-Higher-Precategory →
+    is-transitive-large-globular-structure-Pointed-Type
+```
+
+## Properties
+
+### The left unit law for the identity pointed map
+
+```agda
+module _
+  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
+  where
+
+  left-unit-law-id-pointed-map :
+    (f : A →∗ B) → id-pointed-map ∘∗ f ~∗ f
+  pr1 (left-unit-law-id-pointed-map f) = refl-htpy
+  pr2 (left-unit-law-id-pointed-map f) = right-unit ∙ ap-id (pr2 f)
+```
+
+### The right unit law for the identity pointed map
+
+```agda
+module _
+  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
+  where
+
+  right-unit-law-id-pointed-map :
+    (f : A →∗ B) → f ∘∗ id-pointed-map ~∗ f
+  right-unit-law-id-pointed-map = refl-pointed-htpy
+```

src/synthetic-homotopy-theory.lagda.md

@@ -1,7 +1,7 @@
 # Synthetic homotopy theory
 
 ```agda
-{-# OPTIONS --rewriting #-}
+{-# OPTIONS --rewriting --guardedness #-}
 ```
 
 ## Files in the synthetic homotopy theory folder