Logic

references.bib

@@ -264,6 +264,25 @@ @article{EKMS93
   keywords = {axiality,closure operation,Galois connection,interior operation,polarity}
 }
 
+@article{Esc08,
+  author       = {Escardó, Martín Hötzel},
+  title        = {Exhaustible sets in higher-type computation},
+  journal      = {Logical Methods in Computer Science},
+  volume       = {4},
+  year         = {2008},
+  month        = {8},
+  number       = {3},
+  issue        = {3},
+  publisher    = {Centre pour la Communication Scientifique Directe (CCSD)},
+  pages        = {3:3, 37},
+  issn         = {1860-5974},
+  doi          = {10.2168/LMCS-4(3:3)2008},
+  eprint       = {0808.0441},
+  eprinttype   = {arxiv},
+  eprintclass  = {cs},
+  primaryclass = {cs.LO}
+}
+
 @online{Esc19DefinitionsEquivalence,
   title        = {Definitions of Equivalence Satisfying Judgmental/Strict Groupoid Laws?},
   author       = {Escardó, Martín Hötzel},
@@ -480,6 +499,22 @@ @online{MR23
   keywords    = {20B30 03B15,Mathematics - Group Theory,Mathematics - Logic}
 }
 
+@article{Esc21b,
+  author        = {Escardó, Martín Hötzel},
+  title         = {Injective types in univalent mathematics},
+  journal       = {Mathematical Structures in Computer Science},
+  volume        = {31},
+  year          = {2021},
+  number        = {1},
+  pages         = {89--111},
+  issn          = {0960-1295,1469-8072},
+  doi           = {10.1017/S0960129520000225},
+  eprint        = {1903.01211},
+  archiveprefix = {arXiv},
+  primaryclass  = {math.CT},
+  url           = {https://martinescardo.github.io/TypeTopology/InjectiveTypes.Article.html}
+}
+
 @book{MRR88,
   title       = {A {{Course}} in {{Constructive Algebra}}},
   author      = {Mines, Ray and Richman, Fred and Ruitenburg, Wim},

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

@@ -13,10 +13,12 @@ open import foundation.dependent-pair-types
 open import foundation.double-negation
 open import foundation.negation
 open import foundation.propositional-truncations
+open import foundation.transport-along-identifications
 open import foundation.unit-type
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
+open import foundation-core.contractible-types
 open import foundation-core.empty-types
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types
@@ -32,14 +34,11 @@ A {{#concept "decidable proposition" Agda=is-decidable-Prop}} is a
 [proposition](foundation-core.propositions.md) that has a
 [decidable](foundation.decidable-types.md) underlying type.
 
-## Definition
+## Definitions
 
-### The subtype of decidable propositions
+### The property of a proposition of being decidable
 
 ```agda
-is-decidable-prop : {l : Level} → UU l → UU l
-is-decidable-prop A = is-prop A × is-decidable A
-
 is-prop-is-decidable :
   {l : Level} {A : UU l} → is-prop A → is-prop (is-decidable A)
 is-prop-is-decidable is-prop-A =
@@ -50,6 +49,16 @@ is-decidable-Prop :
 pr1 (is-decidable-Prop P) = is-decidable (type-Prop P)
 pr2 (is-decidable-Prop P) = is-prop-is-decidable (is-prop-type-Prop P)
 
+is-decidable-type-Prop : {l : Level} → Prop l → UU l
+is-decidable-type-Prop P = is-decidable (type-Prop P)
+```
+
+### The subuniverse of decidable propositions
+
+```agda
+is-decidable-prop : {l : Level} → UU l → UU l
+is-decidable-prop A = is-prop A × is-decidable A
+
 is-prop-is-decidable-prop :
   {l : Level} (X : UU l) → is-prop (is-decidable-prop X)
 is-prop-is-decidable-prop X =
@@ -63,6 +72,16 @@ is-decidable-prop-Prop :
   {l : Level} (A : UU l) → Prop l
 pr1 (is-decidable-prop-Prop A) = is-decidable-prop A
 pr2 (is-decidable-prop-Prop A) = is-prop-is-decidable-prop A
+
+module _
+  {l : Level} {A : UU l} (H : is-decidable-prop A)
+  where
+
+  is-prop-type-is-decidable-prop : is-prop A
+  is-prop-type-is-decidable-prop = pr1 H
+
+  is-decidable-type-is-decidable-prop : is-decidable A
+  is-decidable-type-is-decidable-prop = pr2 H
 ```
 
 ### Decidable propositions
@@ -93,7 +112,8 @@ module _
   is-decidable-prop-type-Decidable-Prop = pr2 P
 
   is-decidable-prop-Decidable-Prop : Prop l
-  pr1 is-decidable-prop-Decidable-Prop = is-decidable type-Decidable-Prop
+  pr1 is-decidable-prop-Decidable-Prop =
+    is-decidable type-Decidable-Prop
   pr2 is-decidable-prop-Decidable-Prop =
     is-prop-is-decidable is-prop-type-Decidable-Prop
 ```
@@ -110,6 +130,14 @@ pr1 empty-Decidable-Prop = empty
 pr2 empty-Decidable-Prop = is-decidable-prop-empty
 ```
 
+### Empty types are decidable propositions
+
+```agda
+is-decidable-prop-is-empty :
+  {l : Level} {A : UU l} → is-empty A → is-decidable-prop A
+is-decidable-prop-is-empty H = is-prop-is-empty H , inr H
+```
+
 ### The unit type is a decidable proposition
 
 ```agda
@@ -122,6 +150,14 @@ pr1 unit-Decidable-Prop = unit
 pr2 unit-Decidable-Prop = is-decidable-prop-unit
 ```
 
+### Contractible types are decidable propositions
+
+```agda
+is-decidable-prop-is-contr :
+  {l : Level} {A : UU l} → is-contr A → is-decidable-prop A
+is-decidable-prop-is-contr H = is-prop-is-contr H , inl (center H)
+```
+
 ### The product of two decidable propositions is a decidable proposition
 
 ```agda
@@ -154,6 +190,42 @@ module _
   pr2 product-Decidable-Prop = is-decidable-prop-product-Decidable-Prop
 ```
 
+### The dependent sum of a family of decidable propositions over a decidable proposition
+
+```agda
+module _
+  {l1 l2 : Level} {P : UU l1} {Q : P → UU l2}
+  (H : is-decidable-prop P) (K : (x : P) → is-decidable-prop (Q x))
+  where
+
+  is-prop-is-decidable-prop-Σ : is-prop (Σ P Q)
+  is-prop-is-decidable-prop-Σ =
+    is-prop-Σ
+      ( is-prop-type-is-decidable-prop H)
+      ( is-prop-type-is-decidable-prop ∘ K)
+
+  is-decidable-is-decidable-prop-Σ : is-decidable (Σ P Q)
+  is-decidable-is-decidable-prop-Σ =
+    rec-coproduct
+      ( λ x →
+        rec-coproduct
+          ( λ y → inl (x , y))
+          ( λ ny →
+            inr
+              ( λ xy →
+                ny
+                  ( tr Q
+                    ( eq-is-prop (is-prop-type-is-decidable-prop H))
+                    ( pr2 xy))))
+          ( is-decidable-type-is-decidable-prop (K x)))
+      ( λ nx → inr (λ xy → nx (pr1 xy)))
+      ( is-decidable-type-is-decidable-prop H)
+
+  is-decidable-prop-Σ : is-decidable-prop (Σ P Q)
+  is-decidable-prop-Σ =
+    ( is-prop-is-decidable-prop-Σ , is-decidable-is-decidable-prop-Σ)
+```
+
 ### The negation operation on decidable propositions
 
 ```agda

src/foundation-core/embeddings.lagda.md

@@ -30,7 +30,9 @@ better behaved homotopically than
 being an equivalence is a [property](foundation-core.propositions.md) under
 [function extensionality](foundation.function-extensionality.md).
 
-## Definition
+## Definitions
+
+### The predicate on maps of being embeddings
 
 ```agda
 module _
@@ -48,7 +50,11 @@ module _
   inv-equiv-ap-is-emb :
     {f : A → B} (e : is-emb f) {x y : A} → (f x ＝ f y) ≃ (x ＝ y)
   inv-equiv-ap-is-emb e = inv-equiv (equiv-ap-is-emb e)
+```
 
+### The type of embeddings
+
+```agda
 infix 5 _↪_
 _↪_ :
   {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2)
@@ -73,6 +79,29 @@ module _
   inv-equiv-ap-emb e = inv-equiv (equiv-ap-emb e)
 ```
 
+### The type of embeddings into a type
+
+```agda
+Emb : (l1 : Level) {l2 : Level} (B : UU l2) → UU (lsuc l1 ⊔ l2)
+Emb l1 B = Σ (UU l1) (λ A → A ↪ B)
+
+module _
+  {l1 l2 : Level} {B : UU l2} (f : Emb l1 B)
+  where
+
+  type-Emb : UU l1
+  type-Emb = pr1 f
+
+  emb-Emb : type-Emb ↪ B
+  emb-Emb = pr2 f
+
+  map-Emb : type-Emb → B
+  map-Emb = map-emb emb-Emb
+
+  is-emb-map-Emb : is-emb map-Emb
+  is-emb-map-Emb = is-emb-map-emb emb-Emb
+```
+
 ## Examples
 
 ### The identity map is an embedding

src/foundation-core/equality-dependent-pair-types.lagda.md

@@ -45,11 +45,18 @@ module _
 
 ```agda
   refl-Eq-Σ : (s : Σ A B) → Eq-Σ s s
-  pr1 (refl-Eq-Σ (pair a b)) = refl
-  pr2 (refl-Eq-Σ (pair a b)) = refl
+  refl-Eq-Σ s = refl , refl
+
+  eq-base-eq-pair : {s t : Σ A B} → s ＝ t → pr1 s ＝ pr1 t
+  eq-base-eq-pair = ap pr1
+
+  dependent-eq-family-eq-pair :
+    {s t : Σ A B} (p : s ＝ t) →
+    dependent-identification B (eq-base-eq-pair p) (pr2 s) (pr2 t)
+  dependent-eq-family-eq-pair {s} p = tr-ap pr1 (λ x _ → pr2 x) p (pr1 s)
 
   pair-eq-Σ : {s t : Σ A B} → s ＝ t → Eq-Σ s t
-  pair-eq-Σ {s} refl = refl-Eq-Σ s
+  pair-eq-Σ p = eq-base-eq-pair p , dependent-eq-family-eq-pair p
 
   eq-pair-eq-base :
     {x y : A} {s : B x} (p : x ＝ y) → (x , s) ＝ (y , tr B p s)
@@ -78,11 +85,11 @@ module _
 
   is-retraction-pair-eq-Σ :
     (s t : Σ A B) → pair-eq-Σ {s} {t} ∘ eq-pair-Σ' {s} {t} ~ id {A = Eq-Σ s t}
-  is-retraction-pair-eq-Σ (pair x y) (pair .x .y) (pair refl refl) = refl
+  is-retraction-pair-eq-Σ (x , y) (.x , .y) (refl , refl) = refl
 
   is-section-pair-eq-Σ :
-    (s t : Σ A B) → ((eq-pair-Σ' {s} {t}) ∘ (pair-eq-Σ {s} {t})) ~ id
-  is-section-pair-eq-Σ (pair x y) .(pair x y) refl = refl
+    (s t : Σ A B) → eq-pair-Σ' {s} {t} ∘ pair-eq-Σ {s} {t} ~ id
+  is-section-pair-eq-Σ (x , y) .(x , y) refl = refl
 
   abstract
     is-equiv-eq-pair-Σ : (s t : Σ A B) → is-equiv (eq-pair-Σ' {s} {t})
@@ -110,14 +117,6 @@ module _
 
   η-pair : (t : Σ A B) → (pair (pr1 t) (pr2 t)) ＝ t
   η-pair t = refl
-
-  eq-base-eq-pair-Σ : {s t : Σ A B} → (s ＝ t) → (pr1 s ＝ pr1 t)
-  eq-base-eq-pair-Σ p = pr1 (pair-eq-Σ p)
-
-  dependent-eq-family-eq-pair-Σ :
-    {s t : Σ A B} → (p : s ＝ t) →
-    dependent-identification B (eq-base-eq-pair-Σ p) (pr2 s) (pr2 t)
-  dependent-eq-family-eq-pair-Σ p = pr2 (pair-eq-Σ p)
 ```
 
 ### Lifting equality to the total space
@@ -128,7 +127,7 @@ module _
   where
 
   lift-eq-Σ :
-    {x y : A} (p : x ＝ y) (b : B x) → (pair x b) ＝ (pair y (tr B p b))
+    {x y : A} (p : x ＝ y) (b : B x) → pair x b ＝ pair y (tr B p b)
   lift-eq-Σ refl b = refl
 ```
 
@@ -148,7 +147,7 @@ tr-Σ C refl z = refl
 ```agda
 tr-eq-pair-Σ :
   {l1 l2 l3 : Level} {A : UU l1} {a0 a1 : A}
-  {B : A → UU l2} {b0 : B a0} {b1 : B a1} (C : (Σ A B) → UU l3)
+  {B : A → UU l2} {b0 : B a0} {b1 : B a1} (C : Σ A B → UU l3)
   (p : a0 ＝ a1) (q : dependent-identification B p b0 b1) (u : C (a0 , b0)) →
   tr C (eq-pair-Σ p q) u ＝
   tr (λ x → C (a1 , x)) q (tr C (eq-pair-Σ p refl) u)