Merge branch 'master' of github.com:UniMath/agda-unimath into irratio…

…nality-sqrt-2

references.bib

@@ -513,6 +513,20 @@ @online{oeis
   howpublished = {website},
 }
 
+@phdthesis{Qui16,
+  title = {Lawvere–Tierney sheafification in Homotopy Type Theory},
+  author = {Quirin, Kevin},
+  url = {https://kevinquirin.github.io/thesis/main.pdf},
+  year = {2016},
+  month = dec,
+  number = {2016EMNA0298},
+  school = {École des Mines de Nantes},
+  abstract = {The main goal of this thesis is to define an extension of Gödel not-not translation to all truncated types, in the setting of homotopy type theory. This goal will use some existing theories, like Lawvere–Tierney sheaves theory in toposes, we will adapt in the setting of homotopy type theory. In particular, we will define a Lawvere–Tierney sheafification functor, which is the main theorem presented in this thesis.
+  To define it, we will need some concepts, either already defined in type theory, either not existing yet. In particular, we will define a theory of colimits over graphs as well as their truncated version, and the notion of truncated modalities, based on the existing definition of modalities.
+  Almost all the result presented in this thesis are formalized with the proof assistant Coq together with the library [HoTT/Coq].},
+  langid = {english}
+}
+
 @book{Rie17,
   title     = {Category {{Theory}} in {{Context}}},
   author    = {Riehl, Emily},

src/elementary-number-theory.lagda.md

@@ -148,6 +148,7 @@ open import elementary-number-theory.strict-inequality-integer-fractions public
 open import elementary-number-theory.strict-inequality-integers public
 open import elementary-number-theory.strict-inequality-natural-numbers public
 open import elementary-number-theory.strict-inequality-rational-numbers public
+open import elementary-number-theory.strict-inequality-standard-finite-types public
 open import elementary-number-theory.strictly-ordered-pairs-of-natural-numbers public
 open import elementary-number-theory.strong-induction-natural-numbers public
 open import elementary-number-theory.sums-of-natural-numbers public

src/elementary-number-theory/strict-inequality-standard-finite-types.lagda.md

@@ -0,0 +1,183 @@
+# Strict inequality on the standard finite types
+
+```agda
+module elementary-number-theory.strict-inequality-standard-finite-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.coproduct-types
+open import foundation.empty-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.transport-along-identifications
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Definitions
+
+### The strict inequality relation on the standard finite types
+
+```agda
+le-Fin-Prop : (k : ℕ) → Fin k → Fin k → Prop lzero
+le-Fin-Prop (succ-ℕ k) (inl x) (inl y) = le-Fin-Prop k x y
+le-Fin-Prop (succ-ℕ k) (inl x) (inr star) = unit-Prop
+le-Fin-Prop (succ-ℕ k) (inr star) y = empty-Prop
+
+le-Fin : (k : ℕ) → Fin k → Fin k → UU lzero
+le-Fin k x y = type-Prop (le-Fin-Prop k x y)
+
+is-prop-le-Fin :
+  (k : ℕ) (x y : Fin k) → is-prop (le-Fin k x y)
+is-prop-le-Fin k x y = is-prop-type-Prop (le-Fin-Prop k x y)
+```
+
+### The predicate on maps between standard finite types of preserving strict inequality
+
+```agda
+preserves-le-Fin : (n m : ℕ) → (Fin n → Fin m) → UU lzero
+preserves-le-Fin n m f =
+  (a b : Fin n) →
+  le-Fin n a b →
+  le-Fin m (f a) (f b)
+
+is-prop-preserves-le-Fin :
+  (n m : ℕ) (f : Fin n → Fin m) →
+  is-prop (preserves-le-Fin n m f)
+is-prop-preserves-le-Fin n m f =
+  is-prop-Π λ a →
+  is-prop-Π λ b →
+  is-prop-Π λ p →
+  is-prop-le-Fin m (f a) (f b)
+```
+
+### A map `Fin (succ-ℕ m) → Fin (succ-ℕ n)` preserving strict inequality restricts to a map `Fin m → Fin n`
+
+#### The induced map obtained by restricting
+
+```agda
+restriction-preserves-le-Fin' :
+  (m n : ℕ) (f : Fin (succ-ℕ m) → Fin (succ-ℕ n)) →
+  (preserves-le-Fin (succ-ℕ m) (succ-ℕ n) f) →
+  (x : Fin m) → (y : Fin (succ-ℕ n)) →
+  (f (inl x) ＝ y) → Fin n
+restriction-preserves-le-Fin' (succ-ℕ m) n f pf x (inl y) p = y
+restriction-preserves-le-Fin' (succ-ℕ m) n f pf x (inr y) p =
+  ex-falso
+    ( tr (λ - → le-Fin (succ-ℕ n) - (f (inr star))) p
+      ( pf (inl x) (inr star) star))
+
+restriction-preserves-le-Fin :
+  (m n : ℕ) (f : Fin (succ-ℕ m) → Fin (succ-ℕ n)) →
+  (preserves-le-Fin (succ-ℕ m) (succ-ℕ n) f) →
+  Fin m → Fin n
+restriction-preserves-le-Fin m n f pf x =
+  restriction-preserves-le-Fin' m n f pf x (f (inl x)) refl
+```
+
+#### The induced map is indeed a restriction
+
+```agda
+inl-restriction-preserves-le-Fin' :
+  (m n : ℕ) (f : Fin (succ-ℕ m) → Fin (succ-ℕ n)) →
+  (pf : preserves-le-Fin (succ-ℕ m) (succ-ℕ n) f) →
+  (x : Fin m) →
+  (rx : Fin (succ-ℕ n)) →
+  (px : f (inl x) ＝ rx) →
+  inl-Fin n (restriction-preserves-le-Fin' m n f pf x rx px) ＝ f (inl-Fin m x)
+inl-restriction-preserves-le-Fin' (succ-ℕ m) n f pf x (inl a) px = inv px
+inl-restriction-preserves-le-Fin' (succ-ℕ m) n f pf x (inr a) px =
+  ex-falso
+    ( tr (λ - → le-Fin (succ-ℕ n) - (f (inr star))) px
+      ( pf (inl x) (inr star) star))
+
+inl-restriction-preserves-le-Fin :
+  (m n : ℕ) (f : Fin (succ-ℕ m) → Fin (succ-ℕ n)) →
+  (pf : preserves-le-Fin (succ-ℕ m) (succ-ℕ n) f) →
+  (x : Fin m) →
+  inl-Fin n (restriction-preserves-le-Fin m n f pf x) ＝ f (inl-Fin m x)
+inl-restriction-preserves-le-Fin m n f pf x =
+  inl-restriction-preserves-le-Fin' m n f pf x (f (inl x)) refl
+```
+
+#### The induced map preserves strict inequality
+
+```agda
+preserves-le-restriction-preserves-le-Fin' :
+  (m n : ℕ) (f : Fin (succ-ℕ m) → Fin (succ-ℕ n)) →
+  (pf : preserves-le-Fin (succ-ℕ m) (succ-ℕ n) f) →
+  ( a : Fin m)
+  ( b : Fin m) →
+  ( ra : Fin (succ-ℕ n)) →
+  ( pa : f (inl a) ＝ ra) →
+  ( rb : Fin (succ-ℕ n)) →
+  ( pb : f (inl b) ＝ rb) →
+  le-Fin m a b →
+  le-Fin n
+    (restriction-preserves-le-Fin' m n f pf a ra pa)
+    (restriction-preserves-le-Fin' m n f pf b rb pb)
+preserves-le-restriction-preserves-le-Fin'
+  (succ-ℕ m) n f pf a b (inl x) pa (inl y) pb H =
+  tr (le-Fin (succ-ℕ n) (inl x)) pb
+    ( tr (λ - → le-Fin (succ-ℕ n) - (f (inl b))) pa
+    ( pf (inl a) (inl b) H))
+preserves-le-restriction-preserves-le-Fin'
+  (succ-ℕ m) n f pf a b (inl x) pa (inr y) pb H =
+  ex-falso
+    ( tr (λ - → le-Fin (succ-ℕ n) - (f (inr star))) pb
+      ( pf (inl b) (inr star) star))
+preserves-le-restriction-preserves-le-Fin'
+  (succ-ℕ m) n f pf a b (inr x) pa y pb H =
+  ex-falso
+    ( tr (λ - → le-Fin (succ-ℕ n) - (f (inr star))) pa
+      ( pf (inl a) (inr star) star))
+
+preserves-le-restriction-preserves-le-Fin :
+  (m n : ℕ) (f : Fin (succ-ℕ m) → Fin (succ-ℕ n)) →
+  (pf : preserves-le-Fin (succ-ℕ m) (succ-ℕ n) f) →
+  preserves-le-Fin m n (restriction-preserves-le-Fin m n f pf)
+preserves-le-restriction-preserves-le-Fin m n f pf a b H =
+  preserves-le-restriction-preserves-le-Fin' m n f pf a b
+    ( f (inl a)) refl (f (inl b)) refl H
+```
+
+### A strict inequality preserving map implies an inequality of cardinalities
+
+```agda
+leq-preserves-le-Fin :
+  (m n : ℕ) → (f : Fin m → Fin n) →
+  preserves-le-Fin m n f → leq-ℕ m n
+leq-preserves-le-Fin 0 0 f pf = star
+leq-preserves-le-Fin 0 (succ-ℕ n) f pf = star
+leq-preserves-le-Fin (succ-ℕ m) 0 f pf = f (inr star)
+leq-preserves-le-Fin (succ-ℕ 0) (succ-ℕ n) f pf = star
+leq-preserves-le-Fin (succ-ℕ (succ-ℕ m)) (succ-ℕ n) f pf =
+  leq-preserves-le-Fin (succ-ℕ m) n
+    ( restriction-preserves-le-Fin (succ-ℕ m) n f pf)
+    ( preserves-le-restriction-preserves-le-Fin (succ-ℕ m) n f pf)
+```
+
+### Composition of strict inequality preserving maps
+
+```agda
+comp-preserves-le-Fin :
+  (m n o : ℕ)
+  (g : Fin n → Fin o)
+  (f : Fin m → Fin n) →
+  preserves-le-Fin m n f →
+  preserves-le-Fin n o g →
+  preserves-le-Fin m o (g ∘ f)
+comp-preserves-le-Fin m n o g f pf pg a b H =
+  pg (f a) (f b) (pf a b H)
+```

src/foundation.lagda.md

@@ -85,6 +85,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.continuations public
 open import foundation.contractible-maps public
 open import foundation.contractible-types public
 open import foundation.copartial-elements public