Logic, equality, and compactness

references.bib

@@ -258,6 +258,15 @@ @online{DavidJaz/Cohesion
   howpublished = {{{GitHub}} repository}
 }
 
+@misc{Diener18,
+  title         = {Constructive Reverse Mathematics},
+  author        = {Hannes Diener},
+  year          = {2018},
+  eprint        = {1804.05495},
+  archiveprefix = {arXiv},
+  primaryclass  = {math.LO}
+}
+
 @article{dJE23,
   title       = {{On Small Types in Univalent Foundations}},
   author      = {de Jong, Tom and Escardó, Martín Hötzel},
@@ -333,6 +342,21 @@ @article{Esc08
   primaryclass = {cs.LO}
 }
 
+@article{Esc13,
+  author     = {Escardó, Martín Hötzel},
+  title      = {Infinite sets that satisfy the principle of omniscience in any
+                variety of constructive mathematics},
+  journal    = {The Journal of Symbolic Logic},
+  volume     = {78},
+  year       = {2013},
+  number     = {3},
+  pages      = {764--784},
+  issn       = {0022-4812,1943-5886},
+  mrclass    = {03F50 (03F55)},
+  mrnumber   = {3135497},
+  mrreviewer = {Paulo\ Oliva}
+}
+
 @online{Esc17YetAnother,
   title        = {Yet another characterization of univalence},
   author       = {Escardó, Martín Hötzel},

src/category-theory/representing-arrow-category.lagda.md

@@ -12,15 +12,20 @@ open import category-theory.isomorphisms-in-precategories
 open import category-theory.precategories
 
 open import foundation.booleans
+open import foundation.decidable-propositions
 open import foundation.dependent-pair-types
 open import foundation.empty-types
 open import foundation.identity-types
+open import foundation.inequality-booleans
 open import foundation.logical-equivalences
+open import foundation.logical-operations-booleans
 open import foundation.propositions
 open import foundation.sets
 open import foundation.subtypes
 open import foundation.unit-type
 open import foundation.universe-levels
+
+open import order-theory.posets
 ```
 
 </details>
@@ -42,9 +47,7 @@ obj-representing-arrow-Category = bool
 
 hom-set-representing-arrow-Category :
   obj-representing-arrow-Category → obj-representing-arrow-Category → Set lzero
-hom-set-representing-arrow-Category true true = unit-Set
-hom-set-representing-arrow-Category true false = empty-Set
-hom-set-representing-arrow-Category false _ = unit-Set
+hom-set-representing-arrow-Category x y = set-Prop (leq-bool-Prop x y)
 
 hom-representing-arrow-Category :
   obj-representing-arrow-Category → obj-representing-arrow-Category → UU lzero
@@ -60,8 +63,8 @@ comp-hom-representing-arrow-Category :
   hom-representing-arrow-Category y z →
   hom-representing-arrow-Category x y →
   hom-representing-arrow-Category x z
-comp-hom-representing-arrow-Category {true} {true} {true} _ _ = star
-comp-hom-representing-arrow-Category {false} _ _ = star
+comp-hom-representing-arrow-Category {x} {y} {z} =
+  transitive-leq-bool {x} {y} {z}
 
 associative-comp-hom-representing-arrow-Category :
   {x y z w : obj-representing-arrow-Category} →
@@ -79,8 +82,7 @@ associative-comp-hom-representing-arrow-Category {false} h g f = refl
 
 id-hom-representing-arrow-Category :
   {x : obj-representing-arrow-Category} → hom-representing-arrow-Category x x
-id-hom-representing-arrow-Category {true} = star
-id-hom-representing-arrow-Category {false} = star
+id-hom-representing-arrow-Category {x} = refl-leq-bool {x}
 
 left-unit-law-comp-hom-representing-arrow-Category :
   {x y : obj-representing-arrow-Category} →
@@ -101,49 +103,19 @@ right-unit-law-comp-hom-representing-arrow-Category {true} {true} f = refl
 right-unit-law-comp-hom-representing-arrow-Category {false} f = refl
 
 representing-arrow-Precategory : Precategory lzero lzero
-representing-arrow-Precategory =
-  make-Precategory
-    ( obj-representing-arrow-Category)
-    ( hom-set-representing-arrow-Category)
-    ( λ {x} {y} {z} → comp-hom-representing-arrow-Category {x} {y} {z})
-    ( λ x → id-hom-representing-arrow-Category {x})
-    ( λ {x} {y} {z} {w} →
-      associative-comp-hom-representing-arrow-Category {x} {y} {z} {w})
-    ( λ {x} {y} → left-unit-law-comp-hom-representing-arrow-Category {x} {y})
-    ( λ {x} {y} → right-unit-law-comp-hom-representing-arrow-Category {x} {y})
+representing-arrow-Precategory = precategory-Poset bool-Poset
 ```
 
 ### The representing arrow category
 
 ```agda
 is-category-representing-arrow-Category :
   is-category-Precategory representing-arrow-Precategory
-is-category-representing-arrow-Category true true =
-    is-equiv-has-converse-is-prop
-    ( is-set-bool true true)
-    ( is-prop-type-subtype
-      ( is-iso-prop-Precategory representing-arrow-Precategory {true} {true})
-      ( is-prop-unit))
-    ( λ _ → refl)
-is-category-representing-arrow-Category true false =
-  is-equiv-is-empty
-    ( iso-eq-Precategory representing-arrow-Precategory true false)
-    ( hom-iso-Precategory representing-arrow-Precategory)
-is-category-representing-arrow-Category false true =
-  is-equiv-is-empty
-    ( iso-eq-Precategory representing-arrow-Precategory false true)
-    ( hom-inv-iso-Precategory representing-arrow-Precategory)
-is-category-representing-arrow-Category false false =
-  is-equiv-has-converse-is-prop
-    ( is-set-bool false false)
-    ( is-prop-type-subtype
-      ( is-iso-prop-Precategory representing-arrow-Precategory {false} {false})
-      ( is-prop-unit))
-    ( λ _ → refl)
+is-category-representing-arrow-Category =
+  is-category-precategory-Poset bool-Poset
 
 representing-arrow-Category : Category lzero lzero
-pr1 representing-arrow-Category = representing-arrow-Precategory
-pr2 representing-arrow-Category = is-category-representing-arrow-Category
+representing-arrow-Category = category-Poset bool-Poset
 ```
 
 ## Properties

src/elementary-number-theory/decidable-types.lagda.md

@@ -14,6 +14,7 @@ open import elementary-number-theory.upper-bounds-natural-numbers
 
 open import foundation.cartesian-product-types
 open import foundation.coproduct-types
+open import foundation.decidable-type-families
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
@@ -35,7 +36,7 @@ decidable.
 
 ```agda
 is-decidable-Σ-ℕ :
-  {l : Level} (m : ℕ) (P : ℕ → UU l) (d : is-decidable-fam P) →
+  {l : Level} (m : ℕ) (P : ℕ → UU l) (d : is-decidable-family P) →
   is-decidable (Σ ℕ (λ x → (leq-ℕ m x) × (P x))) → is-decidable (Σ ℕ P)
 is-decidable-Σ-ℕ m P d (inl (pair x (pair l p))) = inl (pair x p)
 is-decidable-Σ-ℕ zero-ℕ P d (inr f) =
@@ -60,7 +61,7 @@ is-decidable-Σ-ℕ (succ-ℕ m) P d (inr f) with d zero-ℕ
 ```agda
 is-decidable-bounded-Σ-ℕ :
   {l1 l2 : Level} (m : ℕ) (P : ℕ → UU l1) (Q : ℕ → UU l2)
-  (dP : is-decidable-fam P) (dQ : is-decidable-fam Q)
+  (dP : is-decidable-family P) (dQ : is-decidable-family Q)
   (H : is-upper-bound-ℕ P m) → is-decidable (Σ ℕ (λ x → (P x) × (Q x)))
 is-decidable-bounded-Σ-ℕ m P Q dP dQ H =
   is-decidable-Σ-ℕ
@@ -76,7 +77,7 @@ is-decidable-bounded-Σ-ℕ m P Q dP dQ H =
           ( pr1 (pr2 p))))
 
 is-decidable-bounded-Σ-ℕ' :
-  {l : Level} (m : ℕ) (P : ℕ → UU l) (d : is-decidable-fam P) →
+  {l : Level} (m : ℕ) (P : ℕ → UU l) (d : is-decidable-family P) →
   is-decidable (Σ ℕ (λ x → (leq-ℕ x m) × (P x)))
 is-decidable-bounded-Σ-ℕ' m P d =
   is-decidable-bounded-Σ-ℕ m
@@ -92,15 +93,15 @@ is-decidable-bounded-Σ-ℕ' m P d =
 ```agda
 is-decidable-strictly-bounded-Σ-ℕ :
   {l1 l2 : Level} (m : ℕ) (P : ℕ → UU l1) (Q : ℕ → UU l2)
-  (dP : is-decidable-fam P) (dQ : is-decidable-fam Q)
+  (dP : is-decidable-family P) (dQ : is-decidable-family Q)
   (H : is-strict-upper-bound-ℕ P m) →
   is-decidable (Σ ℕ (λ x → (P x) × (Q x)))
 is-decidable-strictly-bounded-Σ-ℕ m P Q dP dQ H =
   is-decidable-bounded-Σ-ℕ m P Q dP dQ
     ( is-upper-bound-is-strict-upper-bound-ℕ P m H)
 
 is-decidable-strictly-bounded-Σ-ℕ' :
-  {l : Level} (m : ℕ) (P : ℕ → UU l) (d : is-decidable-fam P) →
+  {l : Level} (m : ℕ) (P : ℕ → UU l) (d : is-decidable-family P) →
   is-decidable (Σ ℕ (λ x → (le-ℕ x m) × (P x)))
 is-decidable-strictly-bounded-Σ-ℕ' m P d =
   is-decidable-strictly-bounded-Σ-ℕ m
@@ -115,7 +116,7 @@ is-decidable-strictly-bounded-Σ-ℕ' m P d =
 
 ```agda
 is-decidable-Π-ℕ :
-  {l : Level} (P : ℕ → UU l) (d : is-decidable-fam P) (m : ℕ) →
+  {l : Level} (P : ℕ → UU l) (d : is-decidable-family P) (m : ℕ) →
   is-decidable ((x : ℕ) → (leq-ℕ m x) → P x) → is-decidable ((x : ℕ) → P x)
 is-decidable-Π-ℕ P d zero-ℕ (inr nH) = inr (λ f → nH (λ x y → f x))
 is-decidable-Π-ℕ P d zero-ℕ (inl H) = inl (λ x → H x (leq-zero-ℕ x))
@@ -136,8 +137,8 @@ is-decidable-Π-ℕ P d (succ-ℕ m) (inl H) with d zero-ℕ
 
 ```agda
 is-decidable-bounded-Π-ℕ :
-  {l1 l2 : Level} (P : ℕ → UU l1) (Q : ℕ → UU l2) (dP : is-decidable-fam P) →
-  (dQ : is-decidable-fam Q) (m : ℕ) (H : is-upper-bound-ℕ P m) →
+  {l1 l2 : Level} (P : ℕ → UU l1) (Q : ℕ → UU l2) (dP : is-decidable-family P) →
+  (dQ : is-decidable-family Q) (m : ℕ) (H : is-upper-bound-ℕ P m) →
   is-decidable ((x : ℕ) → P x → Q x)
 is-decidable-bounded-Π-ℕ P Q dP dQ m H =
   is-decidable-Π-ℕ
@@ -147,7 +148,7 @@ is-decidable-bounded-Π-ℕ P Q dP dQ m H =
     ( inl (λ x l p → ex-falso (contradiction-leq-ℕ x m (H x p) l)))
 
 is-decidable-bounded-Π-ℕ' :
-  {l : Level} (P : ℕ → UU l) (d : is-decidable-fam P) (m : ℕ) →
+  {l : Level} (P : ℕ → UU l) (d : is-decidable-family P) (m : ℕ) →
   is-decidable ((x : ℕ) → (leq-ℕ x m) → P x)
 is-decidable-bounded-Π-ℕ' P d m =
   is-decidable-bounded-Π-ℕ
@@ -163,14 +164,14 @@ is-decidable-bounded-Π-ℕ' P d m =
 
 ```agda
 is-decidable-strictly-bounded-Π-ℕ :
-  {l1 l2 : Level} (P : ℕ → UU l1) (Q : ℕ → UU l2) (dP : is-decidable-fam P) →
-  (dQ : is-decidable-fam Q) (m : ℕ) (H : is-strict-upper-bound-ℕ P m) →
+  {l1 l2 : Level} (P : ℕ → UU l1) (Q : ℕ → UU l2) (dP : is-decidable-family P) →
+  (dQ : is-decidable-family Q) (m : ℕ) (H : is-strict-upper-bound-ℕ P m) →
   is-decidable ((x : ℕ) → P x → Q x)
 is-decidable-strictly-bounded-Π-ℕ P Q dP dQ m H =
   is-decidable-bounded-Π-ℕ P Q dP dQ m (λ x p → leq-le-ℕ x m (H x p))
 
 is-decidable-strictly-bounded-Π-ℕ' :
-  {l : Level} (P : ℕ → UU l) (d : is-decidable-fam P) (m : ℕ) →
+  {l : Level} (P : ℕ → UU l) (d : is-decidable-family P) (m : ℕ) →
   is-decidable ((x : ℕ) → le-ℕ x m → P x)
 is-decidable-strictly-bounded-Π-ℕ' P d m =
   is-decidable-strictly-bounded-Π-ℕ

src/elementary-number-theory/equality-natural-numbers.lagda.md

@@ -14,6 +14,7 @@ open import foundation.coproduct-types
 open import foundation.decidable-equality
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
+open import foundation.discrete-types
 open import foundation.empty-types
 open import foundation.equivalences
 open import foundation.function-types
@@ -22,11 +23,11 @@ open import foundation.identity-types
 open import foundation.propositions
 open import foundation.set-truncations
 open import foundation.sets
+open import foundation.tight-apartness-relations
 open import foundation.unit-type
 open import foundation.universe-levels
 
 open import foundation-core.decidable-propositions
-open import foundation-core.discrete-types
 open import foundation-core.torsorial-type-families
 ```
 
@@ -179,3 +180,11 @@ is-equiv-Eq-eq-ℕ {m} {n} =
 equiv-unit-trunc-ℕ-Set : ℕ ≃ type-trunc-Set ℕ
 equiv-unit-trunc-ℕ-Set = equiv-unit-trunc-Set ℕ-Set
 ```
+
+### The natural numbers have a tight apartness relation
+
+```agda
+ℕ-Type-With-Tight-Apartness : Type-With-Tight-Apartness lzero lzero
+ℕ-Type-With-Tight-Apartness =
+  type-with-tight-apartness-Discrete-Type ℕ-Discrete-Type
+```

src/elementary-number-theory/greatest-common-divisor-natural-numbers.lagda.md

@@ -24,6 +24,7 @@ open import elementary-number-theory.well-ordering-principle-natural-numbers
 open import foundation.action-on-identifications-functions
 open import foundation.cartesian-product-types
 open import foundation.coproduct-types
+open import foundation.decidable-type-families
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
@@ -87,7 +88,7 @@ pr2 (refl-is-common-divisor-ℕ x) = refl-div-ℕ x
 
 ```agda
 is-decidable-is-common-divisor-ℕ :
-  (a b : ℕ) → is-decidable-fam (is-common-divisor-ℕ a b)
+  (a b : ℕ) → is-decidable-family (is-common-divisor-ℕ a b)
 is-decidable-is-common-divisor-ℕ a b x =
   is-decidable-product
     ( is-decidable-div-ℕ x a)
@@ -137,7 +138,7 @@ leq-sum-is-common-divisor-ℕ a b d H =
 
 ```agda
 is-decidable-is-multiple-of-gcd-ℕ :
-  (a b : ℕ) → is-decidable-fam (is-multiple-of-gcd-ℕ a b)
+  (a b : ℕ) → is-decidable-family (is-multiple-of-gcd-ℕ a b)
 is-decidable-is-multiple-of-gcd-ℕ a b n =
   is-decidable-function-type'
     ( is-decidable-neg (is-decidable-is-zero-ℕ (a +ℕ b)))

src/elementary-number-theory/inequality-natural-numbers.lagda.md

@@ -182,13 +182,16 @@ cases-order-three-elements-ℕ x y z =
 
 order-three-elements-ℕ :
   (x y z : ℕ) → cases-order-three-elements-ℕ x y z
-order-three-elements-ℕ zero-ℕ zero-ℕ zero-ℕ = inl (inl (pair star star))
-order-three-elements-ℕ zero-ℕ zero-ℕ (succ-ℕ z) = inl (inl (pair star star))
-order-three-elements-ℕ zero-ℕ (succ-ℕ y) zero-ℕ = inl (inr (pair star star))
+order-three-elements-ℕ zero-ℕ zero-ℕ zero-ℕ =
+  inl (inl (star , star))
+order-three-elements-ℕ zero-ℕ zero-ℕ (succ-ℕ z) =
+  inl (inl (star , star))
+order-three-elements-ℕ zero-ℕ (succ-ℕ y) zero-ℕ =
+  inl (inr (star , star))
 order-three-elements-ℕ zero-ℕ (succ-ℕ y) (succ-ℕ z) =
   inl (map-coproduct (pair star) (pair star) (linear-leq-ℕ y z))
 order-three-elements-ℕ (succ-ℕ x) zero-ℕ zero-ℕ =
-  inr (inl (inl (pair star star)))
+  inr (inl (inl (star , star)))
 order-three-elements-ℕ (succ-ℕ x) zero-ℕ (succ-ℕ z) =
   inr (inl (map-coproduct (pair star) (pair star) (linear-leq-ℕ z x)))
 order-three-elements-ℕ (succ-ℕ x) (succ-ℕ y) zero-ℕ =
@@ -362,8 +365,8 @@ leq-add-ℕ' m n =
 
 ```agda
 subtraction-leq-ℕ : (n m : ℕ) → n ≤-ℕ m → Σ ℕ (λ l → l +ℕ n ＝ m)
-subtraction-leq-ℕ zero-ℕ m p = pair m refl
-subtraction-leq-ℕ (succ-ℕ n) (succ-ℕ m) p = pair (pr1 P) (ap succ-ℕ (pr2 P))
+subtraction-leq-ℕ zero-ℕ m p = (m , refl)
+subtraction-leq-ℕ (succ-ℕ n) (succ-ℕ m) p = (pr1 P , ap succ-ℕ (pr2 P))
   where
   P : Σ ℕ (λ l' → l' +ℕ n ＝ m)
   P = subtraction-leq-ℕ n m p
@@ -450,12 +453,12 @@ leq-mul-ℕ' k x =
 leq-mul-is-nonzero-ℕ :
   (k x : ℕ) → is-nonzero-ℕ k → x ≤-ℕ (x *ℕ k)
 leq-mul-is-nonzero-ℕ k x H with is-successor-is-nonzero-ℕ H
-... | pair l refl = leq-mul-ℕ l x
+... | (l , refl) = leq-mul-ℕ l x
 
 leq-mul-is-nonzero-ℕ' :
   (k x : ℕ) → is-nonzero-ℕ k → x ≤-ℕ (k *ℕ x)
 leq-mul-is-nonzero-ℕ' k x H with is-successor-is-nonzero-ℕ H
-... | pair l refl = leq-mul-ℕ' l x
+... | (l , refl) = leq-mul-ℕ' l x
 ```
 
 ## See also

src/elementary-number-theory/kolakoski-sequence.lagda.md

@@ -14,6 +14,7 @@ open import elementary-number-theory.strong-induction-natural-numbers
 open import foundation.booleans
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
+open import foundation.logical-operations-booleans
 ```
 
 </details>

src/elementary-number-theory/negative-integers.lagda.md

@@ -14,6 +14,7 @@ open import elementary-number-theory.nonzero-integers
 open import foundation.action-on-identifications-functions
 open import foundation.coproduct-types
 open import foundation.decidable-subtypes
+open import foundation.decidable-type-families
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
@@ -96,7 +97,7 @@ neg-one-negative-ℤ = (neg-one-ℤ , star)
 ### Negativity is decidable
 
 ```agda
-is-decidable-is-negative-ℤ : is-decidable-fam is-negative-ℤ
+is-decidable-is-negative-ℤ : is-decidable-family is-negative-ℤ
 is-decidable-is-negative-ℤ (inl x) = inl star
 is-decidable-is-negative-ℤ (inr x) = inr id
 

src/elementary-number-theory/nonnegative-integers.lagda.md

@@ -13,6 +13,7 @@ open import elementary-number-theory.natural-numbers
 open import foundation.action-on-identifications-functions
 open import foundation.coproduct-types
 open import foundation.decidable-subtypes
+open import foundation.decidable-type-families
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
@@ -98,7 +99,7 @@ one-nonnegative-ℤ = (one-ℤ , star)
 ### Nonnegativity is decidable
 
 ```agda
-is-decidable-is-nonnegative-ℤ : is-decidable-fam is-nonnegative-ℤ
+is-decidable-is-nonnegative-ℤ : is-decidable-family is-nonnegative-ℤ
 is-decidable-is-nonnegative-ℤ (inl x) = inr id
 is-decidable-is-nonnegative-ℤ (inr x) = inl star