Propositional operations (#1008)

## Summary - Introduce a general naming scheme for infix endooperations on propositions and the corresponding endooperations on types - Remove uses of `∀` - remove the redundant `implication-Prop` - Add table for propositional logic - Add table for operations on propositions - Correct the definition of exclusive disjunction. It is now named "exclusive sum" (up for discussion) - Introduce _disjunction_, (the correct definition of) _exclusive disjunction_, and _mere logical equivalence_ of types - Introduce _coinhabitedness_ of types - Introduce universal quantification - Define the homotopy preorder of types - Prove that existential quantification of type families agrees with existential quantification of the propositional reflection of the type family - Prove that disjunction of types agree with disjunction of the propositional reflections of the summands Intersects with #1060. Resolves #984. --------- Co-authored-by: Egbert Rijke <[email protected]>
UniMath · Apr 11, 2024 · 11dfe99 · 11dfe99
1 parent eb2b01f
commit 11dfe99
Show file tree

Hide file tree

Showing 193 changed files with 3,522 additions and 1,607 deletions.
diff --git a/MIXFIX-OPERATORS.md b/MIXFIX-OPERATORS.md
@@ -163,22 +163,22 @@ Below, we outline a list of general rules when assigning associativities.
 
 ## Full table of assigned precedences
 
-| Precedence level | Operators                                                                                                                                                                                   |
-| ---------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
-| 50               | Unary nonparametric operators. This class is currently empty                                                                                                                                |
-| 45               | Exponentiative arithmetic operators                                                                                                                                                         |
-| 40               | Multiplicative arithmetic operators                                                                                                                                                         |
-| 36               | Subtractive arithmetic operators                                                                                                                                                            |
-| 35               | Additive arithmetic operators                                                                                                                                                               |
-| 30               | Relational arithmetic operators like`_≤-ℕ_` and `_<-ℕ_`                                                                                                                                     |
-| 25               | Parametric unary operators. This class is currently empty                                                                                                                                   |
-| 20               | Parametric exponentiative operators. This class is currently empty                                                                                                                          |
-| 17               | Left homotopy whiskering `_·l_`                                                                                                                                                             |
-| 16               | Right homotopy whiskering `_·r_`                                                                                                                                                            |
-| 15               | Parametric multiplicative operators like `_×_`,`_×∗_`, `_∧_`, `_∧∗_`, function composition operators like `_∘_`,`_∘∗_`, `_∘e_`, and `_∘iff_`, concatenation operators like `_∙_` and `_∙h_` |
-| 10               | Parametric additive operators like `_+_`, `_∨_`, `_∨∗_`, list concatenation, monadic bind operators for the type checking monad                                                             |
-| 6                | Parametric relational operators like `_＝_`, `_~_`, `_≃_`, and `_↔_`, elementhood relations, subtype relations                                                                              |
-| 5                | Directed function type-like formation operators, e.g. `_⇒_`, `_→∗_`, `_↠_`, `_↪_`, `_↪ᵈ_`, and `_⊆_`                                                                                        |
-| 3                | The pairing operators `_,_` and `_,ω_`                                                                                                                                                      |
-| 0-1              | Reasoning syntaxes                                                                                                                                                                          |
-| -∞               | Function type formation `_→_`                                                                                                                                                               |
+| Precedence level | Operators                                                                                                                                                                                          |
+| ---------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
+| 50               | Unary nonparametric operators. This class is currently empty                                                                                                                                       |
+| 45               | Exponentiative arithmetic operators                                                                                                                                                                |
+| 40               | Multiplicative arithmetic operators                                                                                                                                                                |
+| 36               | Subtractive arithmetic operators                                                                                                                                                                   |
+| 35               | Additive arithmetic operators                                                                                                                                                                      |
+| 30               | Relational arithmetic operators like`_≤-ℕ_` and `_<-ℕ_`                                                                                                                                            |
+| 25               | Parametric unary operators like `¬_` and `¬¬_`                                                                                                                                                     |
+| 20               | Parametric exponentiative operators. This class is currently empty                                                                                                                                 |
+| 17               | Left homotopy whiskering `_·l_`                                                                                                                                                                    |
+| 16               | Right homotopy whiskering `_·r_`                                                                                                                                                                   |
+| 15               | Parametric multiplicative operators like `_×_`,`_×∗_`, `_∧_`, `_∧∗_`, `_*_`, function composition operators like `_∘_`,`_∘∗_`, `_∘e_`, and `_∘iff_`, concatenation operators like `_∙_` and `_∙h_` |
+| 10               | Parametric additive operators like `_+_`, `_∨_`, `_∨∗_`, list concatenation, monadic bind operators for the type checking monad                                                                    |
+| 6                | Parametric relational operators like `_＝_`, `_~_`, `_≃_`, `_⇔_`, and `_↔_`, elementhood relations, subtype relations                                                                              |
+| 5                | Directed function type-like formation operators, e.g. `_⇒_`, `_↪_`, `_→∗_`, `_↠_`, `_↪ᵈ_`, and `_⊆_`                                                                                               |
+| 3                | The pairing operators `_,_` and `_,ω_`                                                                                                                                                             |
+| 0-1              | Reasoning syntaxes                                                                                                                                                                                 |
+| -∞               | Function type formation `_→_`                                                                                                                                                                      |
diff --git a/src/category-theory/categories.lagda.md b/src/category-theory/categories.lagda.md
@@ -18,6 +18,7 @@ open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types
+open import foundation.logical-equivalences
 open import foundation.propositions
 open import foundation.sets
 open import foundation.strictly-involutive-identity-types
@@ -312,7 +313,7 @@ module _
   is-equiv-is-category-is-surjective-iso-eq-Preunivalent-Category :
     is-equiv is-category-is-surjective-iso-eq-Preunivalent-Category
   is-equiv-is-category-is-surjective-iso-eq-Preunivalent-Category =
-    is-equiv-is-prop
+    is-equiv-has-converse-is-prop
       ( is-prop-is-surjective-iso-eq-Precategory
         ( precategory-Preunivalent-Category C))
       ( is-prop-is-category-Precategory (precategory-Preunivalent-Category C))
@@ -321,7 +322,7 @@ module _
   is-equiv-is-surjective-iso-eq-is-category-Preunivalent-Category :
     is-equiv is-surjective-iso-eq-is-category-Preunivalent-Category
   is-equiv-is-surjective-iso-eq-is-category-Preunivalent-Category =
-    is-equiv-is-prop
+    is-equiv-has-converse-is-prop
       ( is-prop-is-category-Precategory (precategory-Preunivalent-Category C))
       ( is-prop-is-surjective-iso-eq-Precategory
         ( precategory-Preunivalent-Category C))

diff --git a/src/category-theory/coproducts-in-precategories.lagda.md b/src/category-theory/coproducts-in-precategories.lagda.md
@@ -16,7 +16,7 @@ open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.iterated-dependent-product-types
 open import foundation.propositions
-open import foundation.unique-existence
+open import foundation.uniqueness-quantification
 open import foundation.universe-levels
 ```
 
@@ -39,7 +39,7 @@ module _
     (z : obj-Precategory C)
     (f : hom-Precategory C x z) →
     (g : hom-Precategory C y z) →
-    ∃!
+    uniquely-exists-structure
       ( hom-Precategory C p z)
       ( λ h →
         ( comp-hom-Precategory C h l ＝ f) ×

diff --git a/src/category-theory/dependent-products-of-large-precategories.lagda.md b/src/category-theory/dependent-products-of-large-precategories.lagda.md
@@ -14,6 +14,7 @@ open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.function-extensionality
 open import foundation.identity-types
+open import foundation.logical-equivalences
 open import foundation.propositions
 open import foundation.sets
 open import foundation.strictly-involutive-identity-types
@@ -215,7 +216,7 @@ module _
     (f : hom-Π-Large-Precategory I C x y) →
     is-equiv (is-fiberwise-iso-is-iso-Π-Large-Precategory f)
   is-equiv-is-fiberwise-iso-is-iso-Π-Large-Precategory f =
-    is-equiv-is-prop
+    is-equiv-has-converse-is-prop
       ( is-prop-is-iso-Large-Precategory (Π-Large-Precategory I C) f)
       ( is-prop-Π (λ i → is-prop-is-iso-Large-Precategory (C i) (f i)))
       ( is-iso-is-fiberwise-iso-Π-Large-Precategory f)
@@ -233,7 +234,7 @@ module _
     (f : hom-Π-Large-Precategory I C x y) →
     is-equiv (is-iso-is-fiberwise-iso-Π-Large-Precategory f)
   is-equiv-is-iso-is-fiberwise-iso-Π-Large-Precategory f =
-    is-equiv-is-prop
+    is-equiv-has-converse-is-prop
       ( is-prop-Π (λ i → is-prop-is-iso-Large-Precategory (C i) (f i)))
       ( is-prop-is-iso-Large-Precategory (Π-Large-Precategory I C) f)
       ( is-fiberwise-iso-is-iso-Π-Large-Precategory f)

diff --git a/src/category-theory/dependent-products-of-precategories.lagda.md b/src/category-theory/dependent-products-of-precategories.lagda.md
@@ -15,6 +15,7 @@ open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.function-extensionality
 open import foundation.identity-types
+open import foundation.logical-equivalences
 open import foundation.propositions
 open import foundation.sets
 open import foundation.strictly-involutive-identity-types
@@ -183,7 +184,7 @@ module _
     (f : hom-Π-Precategory I C x y) →
     is-equiv (is-fiberwise-iso-is-iso-Π-Precategory f)
   is-equiv-is-fiberwise-iso-is-iso-Π-Precategory f =
-    is-equiv-is-prop
+    is-equiv-has-converse-is-prop
       ( is-prop-is-iso-Precategory (Π-Precategory I C) f)
       ( is-prop-Π (λ i → is-prop-is-iso-Precategory (C i) (f i)))
       ( is-iso-is-fiberwise-iso-Π-Precategory f)
@@ -201,7 +202,7 @@ module _
     (f : hom-Π-Precategory I C x y) →
     is-equiv (is-iso-is-fiberwise-iso-Π-Precategory f)
   is-equiv-is-iso-is-fiberwise-iso-Π-Precategory f =
-    is-equiv-is-prop
+    is-equiv-has-converse-is-prop
       ( is-prop-Π (λ i → is-prop-is-iso-Precategory (C i) (f i)))
       ( is-prop-is-iso-Precategory (Π-Precategory I C) f)
       ( is-fiberwise-iso-is-iso-Π-Precategory f)

diff --git a/src/category-theory/essentially-surjective-functors-precategories.lagda.md b/src/category-theory/essentially-surjective-functors-precategories.lagda.md
@@ -43,14 +43,15 @@ module _
     Π-Prop
       ( obj-Precategory D)
       ( λ y →
-        ∃-Prop
+        exists-structure-Prop
           ( obj-Precategory C)
           ( λ x → iso-Precategory D (obj-functor-Precategory C D F x) y))
 
   is-essentially-surjective-functor-Precategory : UU (l1 ⊔ l3 ⊔ l4)
   is-essentially-surjective-functor-Precategory =
     ( y : obj-Precategory D) →
-    ∃ ( obj-Precategory C)
+    exists-structure
+      ( obj-Precategory C)
       ( λ x → iso-Precategory D (obj-functor-Precategory C D F x) y)
 
   is-prop-is-essentially-surjective-functor-Precategory :

diff --git a/src/category-theory/exponential-objects-precategories.lagda.md b/src/category-theory/exponential-objects-precategories.lagda.md
@@ -13,7 +13,7 @@ open import category-theory.products-in-precategories
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.identity-types
-open import foundation.unique-existence
+open import foundation.uniqueness-quantification
 open import foundation.universe-levels
 ```
 
@@ -47,7 +47,7 @@ module _
   is-exponential-obj-Precategory x y e ev =
     (z : obj-Precategory C)
     (f : hom-Precategory C (object-product-obj-Precategory C p z x) y) →
-    ∃!
+    uniquely-exists-structure
       ( hom-Precategory C z e)
       ( λ g →
         comp-hom-Precategory C ev

diff --git a/src/category-theory/faithful-maps-precategories.lagda.md b/src/category-theory/faithful-maps-precategories.lagda.md
@@ -16,7 +16,9 @@ open import foundation.equivalences
 open import foundation.function-types
 open import foundation.injective-maps
 open import foundation.iterated-dependent-product-types
+open import foundation.logical-equivalences
 open import foundation.propositions
+open import foundation.sets
 open import foundation.universe-levels
 ```
 
@@ -156,15 +158,15 @@ module _
   is-equiv-is-injective-hom-is-faithful-map-Precategory :
     is-equiv is-injective-hom-is-faithful-map-Precategory
   is-equiv-is-injective-hom-is-faithful-map-Precategory =
-    is-equiv-is-prop
+    is-equiv-has-converse-is-prop
       ( is-prop-is-faithful-map-Precategory C D F)
       ( is-prop-is-injective-hom-map-Precategory C D F)
       ( is-faithful-is-injective-hom-map-Precategory)
 
   is-equiv-is-faithful-is-injective-hom-map-Precategory :
     is-equiv is-faithful-is-injective-hom-map-Precategory
   is-equiv-is-faithful-is-injective-hom-map-Precategory =
-    is-equiv-is-prop
+    is-equiv-has-converse-is-prop
       ( is-prop-is-injective-hom-map-Precategory C D F)
       ( is-prop-is-faithful-map-Precategory C D F)
       ( is-injective-hom-is-faithful-map-Precategory)

diff --git a/src/category-theory/isomorphisms-in-categories.lagda.md b/src/category-theory/isomorphisms-in-categories.lagda.md
@@ -212,7 +212,7 @@ module _
 ### The type of isomorphisms form a set
 
 The type of isomorphisms between objects `x y : A` is a
-[subtype](foundation-core.subtypes.md) of the [foundation-core.sets.md)
+[subtype](foundation-core.subtypes.md) of the [set](foundation-core.sets.md)
 `hom x y` since being an isomorphism is a proposition.
 
 ```agda

diff --git a/src/category-theory/isomorphisms-in-precategories.lagda.md b/src/category-theory/isomorphisms-in-precategories.lagda.md
@@ -248,7 +248,7 @@ module _
 ### The type of isomorphisms form a set
 
 The type of isomorphisms between objects `x y : A` is a
-[subtype](foundation-core.subtypes.md) of the [foundation-core.sets.md)
+[subtype](foundation-core.subtypes.md) of the [set](foundation-core.sets.md)
 `hom x y` since being an isomorphism is a proposition.
 
 ```agda

diff --git a/src/category-theory/natural-numbers-object-precategories.lagda.md b/src/category-theory/natural-numbers-object-precategories.lagda.md
@@ -14,7 +14,7 @@ open import foundation.action-on-identifications-functions
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.identity-types
-open import foundation.unique-existence
+open import foundation.uniqueness-quantification
 open import foundation.universe-levels
 ```
 
@@ -43,7 +43,7 @@ module _
     (x : obj-Precategory C)
     (q : hom-Precategory C t x)
     (f : hom-Precategory C x x) →
-    ∃!
+    uniquely-exists-structure
       ( hom-Precategory C n x)
       ( λ u →
         ( comp-hom-Precategory C u z ＝ q) ×

diff --git a/src/category-theory/precategory-of-functors.lagda.md b/src/category-theory/precategory-of-functors.lagda.md
@@ -20,6 +20,7 @@ open import foundation.equivalences
 open import foundation.function-extensionality
 open import foundation.functoriality-dependent-pair-types
 open import foundation.identity-types
+open import foundation.logical-equivalences
 open import foundation.propositions
 open import foundation.strictly-involutive-identity-types
 open import foundation.universe-levels
@@ -199,7 +200,7 @@ module _
     (f : natural-transformation-Precategory C D F G) →
     is-equiv (is-iso-functor-is-natural-isomorphism-Precategory f)
   is-equiv-is-iso-functor-is-natural-isomorphism-Precategory f =
-    is-equiv-is-prop
+    is-equiv-has-converse-is-prop
       ( is-prop-is-natural-isomorphism-Precategory C D F G f)
       ( is-prop-is-iso-Precategory
         ( functor-precategory-Precategory C D) {F} {G} f)
@@ -209,7 +210,7 @@ module _
     (f : natural-transformation-Precategory C D F G) →
     is-equiv (is-natural-isomorphism-is-iso-functor-Precategory f)
   is-equiv-is-natural-isomorphism-is-iso-functor-Precategory f =
-    is-equiv-is-prop
+    is-equiv-has-converse-is-prop
       ( is-prop-is-iso-Precategory
         ( functor-precategory-Precategory C D) {F} {G} f)
       ( is-prop-is-natural-isomorphism-Precategory C D F G f)

diff --git a/src/category-theory/precategory-of-maps-precategories.lagda.md b/src/category-theory/precategory-of-maps-precategories.lagda.md
@@ -20,6 +20,7 @@ open import foundation.equivalences
 open import foundation.function-extensionality
 open import foundation.functoriality-dependent-pair-types
 open import foundation.identity-types
+open import foundation.logical-equivalences
 open import foundation.propositions
 open import foundation.strictly-involutive-identity-types
 open import foundation.universe-levels
@@ -199,7 +200,7 @@ module _
     (f : natural-transformation-map-Precategory C D F G) →
     is-equiv (is-iso-map-is-natural-isomorphism-map-Precategory f)
   is-equiv-is-iso-map-is-natural-isomorphism-map-Precategory f =
-    is-equiv-is-prop
+    is-equiv-has-converse-is-prop
       ( is-prop-is-natural-isomorphism-map-Precategory C D F G f)
       ( is-prop-is-iso-Precategory
         ( map-precategory-Precategory C D) {F} {G} f)
@@ -209,7 +210,7 @@ module _
     (f : natural-transformation-map-Precategory C D F G) →
     is-equiv (is-natural-isomorphism-map-is-iso-map-Precategory f)
   is-equiv-is-natural-isomorphism-map-is-iso-map-Precategory f =
-    is-equiv-is-prop
+    is-equiv-has-converse-is-prop
       ( is-prop-is-iso-Precategory
         ( map-precategory-Precategory C D) {F} {G} f)
       ( is-prop-is-natural-isomorphism-map-Precategory C D F G f)

diff --git a/src/category-theory/products-in-precategories.lagda.md b/src/category-theory/products-in-precategories.lagda.md
@@ -16,7 +16,7 @@ open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.iterated-dependent-product-types
 open import foundation.propositions
-open import foundation.unique-existence
+open import foundation.uniqueness-quantification
 open import foundation.universe-levels
 ```
 
@@ -52,8 +52,11 @@ module _
     (z : obj-Precategory C)
     (f : hom-Precategory C z x) →
     (g : hom-Precategory C z y) →
-    (∃! (hom-Precategory C z p) λ h →
-        (comp-hom-Precategory C l h ＝ f) × (comp-hom-Precategory C r h ＝ g))
+    ( uniquely-exists-structure
+      ( hom-Precategory C z p)
+      ( λ h →
+        ( comp-hom-Precategory C l h ＝ f) ×
+        ( comp-hom-Precategory C r h ＝ g)))
 
   product-obj-Precategory : obj-Precategory C → obj-Precategory C → UU (l1 ⊔ l2)
   product-obj-Precategory x y =