A constructive Cantor–Schröder–Bernstein theorem

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

@@ -20,6 +20,7 @@ open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.retractions
 open import foundation-core.sections
+open import foundation-core.torsorial-type-families
 ```
 
 </details>
@@ -134,6 +135,18 @@ module _
       is-contr-map-is-coherently-invertible ∘ is-coherently-invertible-is-equiv
 ```
 
+### The identity function is contractible
+
+```agda
+module _
+  {l1 : Level} {A : UU l1}
+  where
+
+  abstract
+    is-contr-map-id : is-contr-map (id {A = A})
+    is-contr-map-id = is-torsorial-Id'
+```
+
 ## See also
 
 - For the notion of biinvertible maps see

src/foundation-core/decidable-propositions.lagda.md

@@ -15,6 +15,7 @@ open import foundation.negation
 open import foundation.propositional-truncations
 open import foundation.transport-along-identifications
 open import foundation.unit-type
+open import foundation.universal-property-empty-type
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
@@ -224,6 +225,16 @@ module _
   is-decidable-prop-Σ : is-decidable-prop (Σ P Q)
   is-decidable-prop-Σ =
     ( is-prop-is-decidable-prop-Σ , is-decidable-is-decidable-prop-Σ)
+
+Σ-Decidable-Prop :
+  {l1 l2 : Level} →
+  (P : Decidable-Prop l1) →
+  (type-Decidable-Prop P → Decidable-Prop l2) → Decidable-Prop (l1 ⊔ l2)
+Σ-Decidable-Prop P Q =
+  ( Σ (type-Decidable-Prop P) (type-Decidable-Prop ∘ Q) ,
+    is-decidable-prop-Σ
+      ( is-decidable-prop-type-Decidable-Prop P)
+      ( is-decidable-prop-type-Decidable-Prop ∘ Q))
 ```
 
 ### The negation operation on decidable propositions
@@ -251,6 +262,78 @@ type-neg-Decidable-Prop :
 type-neg-Decidable-Prop P = type-Decidable-Prop (neg-Decidable-Prop P)
 ```
 
+### Function types between decidable propositions
+
+```agda
+module _
+  {l1 l2 : Level} {P : UU l1} {Q : UU l2}
+  where
+
+  is-decidable-prop-function-type' :
+    is-decidable P → (P → is-decidable-prop Q) → is-decidable-prop (P → Q)
+  is-decidable-prop-function-type' H K =
+    ( rec-coproduct
+      ( λ p → is-prop-function-type (is-prop-type-is-decidable-prop (K p)))
+      ( λ np → is-prop-is-contr (universal-property-empty-is-empty P np Q))
+      ( H)) ,
+    ( is-decidable-function-type' H (is-decidable-type-is-decidable-prop ∘ K))
+
+  is-decidable-prop-function-type :
+    is-decidable P → is-decidable-prop Q → is-decidable-prop (P → Q)
+  is-decidable-prop-function-type H K =
+    ( is-prop-function-type (is-prop-type-is-decidable-prop K)) ,
+    ( is-decidable-function-type H (is-decidable-type-is-decidable-prop K))
+
+hom-Decidable-Prop :
+  {l1 l2 : Level} →
+  Decidable-Prop l1 → Decidable-Prop l2 → Decidable-Prop (l1 ⊔ l2)
+hom-Decidable-Prop P Q =
+  ( type-Decidable-Prop P → type-Decidable-Prop Q) ,
+  ( is-decidable-prop-function-type
+    ( is-decidable-Decidable-Prop P)
+    ( is-decidable-prop-type-Decidable-Prop Q))
+```
+
+### Dependent products of decidable propositions
+
+```agda
+module _
+  {l1 l2 : Level} {P : UU l1} {Q : P → UU l2}
+  where
+
+  is-decidable-Π-is-decidable-prop :
+    is-decidable-prop P →
+    ((x : P) → is-decidable-prop (Q x)) →
+    is-decidable ((x : P) → Q x)
+  is-decidable-Π-is-decidable-prop H K =
+    rec-coproduct
+      ( λ x →
+        rec-coproduct
+          ( λ y →
+            inl (λ x' → tr Q (eq-is-prop (is-prop-type-is-decidable-prop H)) y))
+          ( λ ny → inr (λ f → ny (f x)))
+          ( is-decidable-type-is-decidable-prop (K x)))
+      ( λ nx → inl (λ x' → ex-falso (nx x')))
+      ( is-decidable-type-is-decidable-prop H)
+
+  is-decidable-prop-Π :
+    is-decidable-prop P →
+    ((x : P) → is-decidable-prop (Q x)) →
+    is-decidable-prop ((x : P) → Q x)
+  is-decidable-prop-Π H K =
+    ( is-prop-Π (is-prop-type-is-decidable-prop ∘ K)) ,
+    ( is-decidable-Π-is-decidable-prop H K)
+
+Π-Decidable-Prop :
+  {l1 l2 : Level} (P : Decidable-Prop l1) →
+  (type-Decidable-Prop P → Decidable-Prop l2) → Decidable-Prop (l1 ⊔ l2)
+Π-Decidable-Prop P Q =
+  ( (x : type-Decidable-Prop P) → type-Decidable-Prop (Q x)) ,
+  ( is-decidable-prop-Π
+    ( is-decidable-prop-type-Decidable-Prop P)
+    ( is-decidable-prop-type-Decidable-Prop ∘ Q))
+```
+
 ### Decidability of a propositional truncation
 
 ```agda

src/foundation.lagda.md

@@ -47,6 +47,7 @@ open import foundation.binary-transport public
 open import foundation.binary-type-duality public
 open import foundation.booleans public
 open import foundation.cantor-schroder-bernstein-escardo public
+open import foundation.cantor-schroder-bernstein-wlpo public
 open import foundation.cantors-theorem public
 open import foundation.cartesian-morphisms-arrows public
 open import foundation.cartesian-morphisms-span-diagrams public
@@ -89,6 +90,7 @@ open import foundation.connected-types public
 open import foundation.constant-maps public
 open import foundation.constant-span-diagrams public
 open import foundation.constant-type-families public
+open import foundation.constructive-cantor-schroder-bernstein public
 open import foundation.continuations public
 open import foundation.contractible-maps public
 open import foundation.contractible-types public
@@ -229,6 +231,7 @@ open import foundation.identity-systems public
 open import foundation.identity-truncated-types public
 open import foundation.identity-types public
 open import foundation.images public
+open import foundation.images-embeddings public
 open import foundation.images-subtypes public
 open import foundation.implicit-function-types public
 open import foundation.impredicative-encodings public

src/foundation/booleans.lagda.md

@@ -7,10 +7,7 @@ module foundation.booleans where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.decidable-equality
-open import foundation.decidable-types
 open import foundation.dependent-pair-types
-open import foundation.discrete-types
 open import foundation.involutions
 open import foundation.negated-equality
 open import foundation.raising-universe-levels
@@ -196,30 +193,18 @@ abstract
       ( λ x y → eq-Eq-bool)
 
 bool-Set : Set lzero
-bool-Set = bool , is-set-bool
-```
-
-### The booleans have decidable equality
-
-```agda
-has-decidable-equality-bool : has-decidable-equality bool
-has-decidable-equality-bool true true = inl refl
-has-decidable-equality-bool true false = inr neq-true-false-bool
-has-decidable-equality-bool false true = inr neq-false-true-bool
-has-decidable-equality-bool false false = inl refl
-
-bool-Discrete-Type : Discrete-Type lzero
-bool-Discrete-Type = bool , has-decidable-equality-bool
+pr1 bool-Set = bool
+pr2 bool-Set = is-set-bool
 ```
 
 ### The "is true" predicate on booleans
 
 ```agda
 is-true : bool → UU lzero
-is-true = _＝ true
+is-true = Eq-bool true
 
 is-prop-is-true : (b : bool) → is-prop (is-true b)
-is-prop-is-true b = is-set-bool b true
+is-prop-is-true = is-prop-Eq-bool true
 
 is-true-Prop : bool → Prop lzero
 is-true-Prop b = is-true b , is-prop-is-true b
@@ -229,27 +214,15 @@ is-true-Prop b = is-true b , is-prop-is-true b
 
 ```agda
 is-false : bool → UU lzero
-is-false = _＝ false
+is-false = Eq-bool false
 
 is-prop-is-false : (b : bool) → is-prop (is-false b)
-is-prop-is-false b = is-set-bool b false
+is-prop-is-false = is-prop-Eq-bool false
 
 is-false-Prop : bool → Prop lzero
 is-false-Prop b = is-false b , is-prop-is-false b
 ```
 
-### A boolean cannot be both true and false
-
-```agda
-not-is-false-is-true : (x : bool) → is-true x → ¬ (is-false x)
-not-is-false-is-true true t ()
-not-is-false-is-true false () f
-
-not-is-true-is-false : (x : bool) → is-false x → ¬ (is-true x)
-not-is-true-is-false true () f
-not-is-true-is-false false t ()
-```
-
 ### The type of booleans is equivalent to `Fin 2`
 
 ```agda