Central H-spaces

src/foundation-core/binary-relations.lagda.md

@@ -0,0 +1,220 @@
+# Binary relations
+
+```agda
+module foundation-core.binary-relations where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.iterated-dependent-product-types
+open import foundation.universe-levels
+
+open import foundation-core.identity-types
+open import foundation-core.negation
+open import foundation-core.propositions
+```
+
+</details>
+
+## Idea
+
+A {{#concept "binary relation" Agda=Relation}} on a type `A` is a family of types `R x y` depending on
+two variables `x y : A`. In the special case where each `R x y` is a
+[proposition](foundation-core.propositions.md), we say that the relation is
+valued in propositions. Thus, we take a general relation to mean a
+_proof-relevant_ relation.
+
+## Definition
+
+### Relations valued in types
+
+```agda
+Relation : {l1 : Level} (l : Level) (A : UU l1) → UU (l1 ⊔ lsuc l)
+Relation l A = A → A → UU l
+
+total-space-Relation :
+  {l1 l : Level} {A : UU l1} → Relation l A → UU (l1 ⊔ l)
+total-space-Relation {A = A} R = Σ (A × A) λ (a , a') → R a a'
+```
+
+### Relations valued in propositions
+
+```agda
+Relation-Prop :
+  (l : Level) {l1 : Level} (A : UU l1) → UU (lsuc l ⊔ l1)
+Relation-Prop l A = A → A → Prop l
+
+type-Relation-Prop :
+  {l1 l2 : Level} {A : UU l1} → Relation-Prop l2 A → Relation l2 A
+type-Relation-Prop R x y = pr1 (R x y)
+
+is-prop-type-Relation-Prop :
+  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A) →
+  (x y : A) → is-prop (type-Relation-Prop R x y)
+is-prop-type-Relation-Prop R x y = pr2 (R x y)
+
+total-space-Relation-Prop :
+  {l : Level} {l1 : Level} {A : UU l1} → Relation-Prop l A → UU (l ⊔ l1)
+total-space-Relation-Prop {A = A} R =
+  Σ (A × A) λ (a , a') → type-Relation-Prop R a a'
+```
+
+### The predicate of being a reflexive relation
+
+A relation `R` on a type `A` is said to be **reflexive** if it comes equipped
+with a function `(x : A) → R x x`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
+  where
+
+  is-reflexive : UU (l1 ⊔ l2)
+  is-reflexive = (x : A) → R x x
+```
+
+### The predicate of being a reflexive relation valued in propositions
+
+A relation `R` on a type `A` valued in propositions is said to be **reflexive**
+if its underlying relation is reflexive
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A)
+  where
+
+  is-reflexive-Relation-Prop : UU (l1 ⊔ l2)
+  is-reflexive-Relation-Prop = is-reflexive (type-Relation-Prop R)
+
+  is-prop-is-reflexive-Relation-Prop : is-prop is-reflexive-Relation-Prop
+  is-prop-is-reflexive-Relation-Prop =
+    is-prop-Π (λ x → is-prop-type-Relation-Prop R x x)
+```
+
+### The predicate of being a symmetric relation
+
+A relation `R` on a type `A` is said to be **symmetric** if it comes equipped
+with a function `(x y : A) → R x y → R y x`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
+  where
+
+  is-symmetric : UU (l1 ⊔ l2)
+  is-symmetric = (x y : A) → R x y → R y x
+```
+
+### The predicate of being a symmetric relation valued in propositions
+
+A relation `R` on a type `A` valued in propositions is said to be **symmetric**
+if its underlying relation is symmetric.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A)
+  where
+
+  is-symmetric-Relation-Prop : UU (l1 ⊔ l2)
+  is-symmetric-Relation-Prop = is-symmetric (type-Relation-Prop R)
+
+  is-prop-is-symmetric-Relation-Prop : is-prop is-symmetric-Relation-Prop
+  is-prop-is-symmetric-Relation-Prop =
+    is-prop-iterated-Π 3
+      ( λ x y r → is-prop-type-Relation-Prop R y x)
+```
+
+### The predicate of being a transitive relation
+
+A relation `R` on a type `A` is said to be **transitive** if it comes equipped
+with a function `(x y z : A) → R y z → R x y → R x z`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
+  where
+
+  is-transitive : UU (l1 ⊔ l2)
+  is-transitive = (x y z : A) → R y z → R x y → R x z
+```
+
+### The predicate of being a transitive relation valued in propositions
+
+A relation `R` on a type `A` valued in propositions is said to be **transitive**
+if its underlying relation is transitive.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A)
+  where
+
+  is-transitive-Relation-Prop : UU (l1 ⊔ l2)
+  is-transitive-Relation-Prop = is-transitive (type-Relation-Prop R)
+
+  is-prop-is-transitive-Relation-Prop : is-prop is-transitive-Relation-Prop
+  is-prop-is-transitive-Relation-Prop =
+    is-prop-iterated-Π 3
+      ( λ x y z →
+        is-prop-function-type
+          ( is-prop-function-type (is-prop-type-Relation-Prop R x z)))
+```
+
+### The predicate of being an irreflexive relation
+
+A relation `R` on a type `A` is said to be **irreflexive** if it comes equipped
+with a function `(x : A) → ¬ (R x y)`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
+  where
+
+  is-irreflexive : UU (l1 ⊔ l2)
+  is-irreflexive = (x : A) → ¬ (R x x)
+```
+
+### The predicate of being an asymmetric relation
+
+A relation `R` on a type `A` is said to be **asymmetric** if it comes equipped
+with a function `(x y : A) → R x y → ¬ (R y x)`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
+  where
+
+  is-asymmetric : UU (l1 ⊔ l2)
+  is-asymmetric = (x y : A) → R x y → ¬ (R y x)
+```
+
+### The predicate of being an antisymmetric relation
+
+A relation `R` on a type `A` is said to be **antisymmetric** if it comes
+equipped with a function `(x y : A) → R x y → R y x → x ＝ y`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
+  where
+
+  is-antisymmetric : UU (l1 ⊔ l2)
+  is-antisymmetric = (x y : A) → R x y → R y x → x ＝ y
+```
+
+### The predicate of being an antisymmetric relation valued in propositions
+
+A relation `R` on a type `A` valued in propositions is said to be
+**antisymmetric** if its underlying relation is antisymmetric.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A)
+  where
+
+  is-antisymmetric-Relation-Prop : UU (l1 ⊔ l2)
+  is-antisymmetric-Relation-Prop = is-antisymmetric (type-Relation-Prop R)
+```
+

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

@@ -840,12 +840,12 @@ module _
       ( coh x)
       ( H x)
 
-  right-unwhisker-cohernece-square-homotopies :
+  right-unwhisker-concat-coherence-square-homotopies :
     {u : (x : A) → B x} (H : i ~ u) →
     coherence-square-homotopies top left (right ∙h H) (bottom ∙h H) →
     coherence-square-homotopies top left right bottom
-  right-unwhisker-cohernece-square-homotopies H coh x =
-    right-unwhisker-cohernece-square-identifications
+  right-unwhisker-concat-coherence-square-homotopies H coh x =
+    right-unwhisker-concat-coherence-square-identifications
       ( top x)
       ( left x)
       ( right x)

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

@@ -788,11 +788,11 @@ module _
         ( inv right-unit)
         ( s))
 
-  right-unwhisker-cohernece-square-identifications :
+  right-unwhisker-concat-coherence-square-identifications :
     {u : A} (p : w ＝ u) →
     coherence-square-identifications top left (right ∙ p) (bottom ∙ p) →
     coherence-square-identifications top left right bottom
-  right-unwhisker-cohernece-square-identifications refl =
+  right-unwhisker-concat-coherence-square-identifications refl =
     ( inv-concat-right-identification-coherence-square-identifications
       ( top)
       ( left)

src/foundation-core/mere-equality.lagda.md

@@ -0,0 +1,74 @@
+# Mere equality
+
+```agda
+module foundation-core.mere-equality where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation-core.binary-relations
+open import foundation.functoriality-propositional-truncation
+open import foundation.propositional-truncations
+open import foundation.universe-levels
+
+open import foundation-core.identity-types
+open import foundation-core.propositions
+```
+
+</details>
+
+## Idea
+
+Two elements in a type are said to be {{#concept "merely equal" Agda=mere-eq}} if there is an element of the
+[propositionally truncated](foundation.propositional-truncations.md) [identity type](foundation-core.identity-types.md) between them.
+
+## Definitions
+
+### Mere equality
+
+```agda
+module _
+  {l : Level} {A : UU l}
+  where
+
+  mere-eq-Prop : A → A → Prop l
+  mere-eq-Prop x y = trunc-Prop (x ＝ y)
+
+  mere-eq : A → A → UU l
+  mere-eq x y = type-Prop (mere-eq-Prop x y)
+
+  is-prop-mere-eq : (x y : A) → is-prop (mere-eq x y)
+  is-prop-mere-eq x y = is-prop-type-trunc-Prop
+```
+
+## Properties
+
+### Reflexivity
+
+```agda
+refl-mere-eq :
+  {l : Level} {A : UU l} → is-reflexive (mere-eq {l} {A})
+refl-mere-eq _ = unit-trunc-Prop refl
+```
+
+### Symmetry
+
+```agda
+abstract
+  symmetric-mere-eq :
+    {l : Level} {A : UU l} → is-symmetric (mere-eq {l} {A})
+  symmetric-mere-eq _ _ = map-trunc-Prop inv
+```
+
+### Transitivity
+
+```agda
+abstract
+  transitive-mere-eq :
+    {l : Level} {A : UU l} → is-transitive (mere-eq {l} {A})
+  transitive-mere-eq x y z p q =
+    apply-universal-property-trunc-Prop q
+      ( mere-eq-Prop x z)
+      ( λ p' → map-trunc-Prop (p' ∙_) p)
+```

src/foundation.lagda.md

@@ -257,6 +257,8 @@ open import foundation.mere-embeddings public
 open import foundation.mere-equality public
 open import foundation.mere-equivalences public
 open import foundation.mere-functions public
+open import foundation.mere-homotopies public
+open import foundation.mere-identity-endomorphisms public
 open import foundation.mere-logical-equivalences public
 open import foundation.mere-path-cosplit-maps public
 open import foundation.monomorphisms public