diff --git a/MIXFIX-OPERATORS.md b/MIXFIX-OPERATORS.md index a6d246d6c4..aa6021c8ef 100644 --- a/MIXFIX-OPERATORS.md +++ b/MIXFIX-OPERATORS.md @@ -153,7 +153,7 @@ Below, we outline a list of general rules when assigning associativities. associated regardless. For instance, one should never write ```agda - assoc : p ∙ (q ∙ r) ＝ p ∙ q ∙ r + assoc : p ∙ q ∙ r ＝ p ∙ (q ∙ r) ``` - **Unique well-typed associativity**. When an operator only has one well-typed @@ -163,20 +163,22 @@ Below, we outline a list of general rules when assigning associativities. ## Full table of assigned precedences -| Precedence level | Operators | -| ---------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | -| 50 | Unary non-parametric 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 | -| 15 | Parametric multiplicative operators like `_×_`,`_×∗_`, `_∧_`, `_∧∗_`, function composition operators like `_∘_`,`_∘∗_`, `_∘e_`, and `_∘iff_`, identification concatenation and whiskering operators like `_∙_`, `_∙h_`, `_·l_`, and `_·r_` | -| 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 non-parametric 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 `_→_` | diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index 7dedc2874e..8dfdb41987 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -27,6 +27,7 @@ open import elementary-number-theory.collatz-conjecture public open import elementary-number-theory.commutative-semiring-of-natural-numbers public open import elementary-number-theory.congruence-integers public open import elementary-number-theory.congruence-natural-numbers public +open import elementary-number-theory.cubes-natural-numbers public open import elementary-number-theory.decidable-dependent-function-types public open import elementary-number-theory.decidable-total-order-natural-numbers public open import elementary-number-theory.decidable-total-order-standard-finite-types public @@ -55,6 +56,7 @@ open import elementary-number-theory.greatest-common-divisor-integers public open import elementary-number-theory.greatest-common-divisor-natural-numbers public open import elementary-number-theory.group-of-integers public open import elementary-number-theory.half-integers public +open import elementary-number-theory.hardy-ramanujan-number public open import elementary-number-theory.inequality-integer-fractions public open import elementary-number-theory.inequality-integers public open import elementary-number-theory.inequality-natural-numbers public @@ -120,6 +122,7 @@ open import elementary-number-theory.strict-inequality-natural-numbers 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 +open import elementary-number-theory.taxicab-numbers public open import elementary-number-theory.telephone-numbers public open import elementary-number-theory.triangular-numbers public open import elementary-number-theory.twin-prime-conjecture public diff --git a/src/elementary-number-theory/cubes-natural-numbers.lagda.md b/src/elementary-number-theory/cubes-natural-numbers.lagda.md new file mode 100644 index 0000000000..b6fa0e8efc --- /dev/null +++ b/src/elementary-number-theory/cubes-natural-numbers.lagda.md @@ -0,0 +1,58 @@ +# Cubes of natural numbers + +```agda +module elementary-number-theory.cubes-natural-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.multiplication-natural-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.squares-natural-numbers + +open import foundation.dependent-pair-types +open import foundation.fibers-of-maps +open import foundation.universe-levels +``` + +
+ +## Idea + +The {{#concept "cube" Disambiguation="natural number"}} `n³` of a +[natural number](elementary-number-theory.natural-numbers.md) `n` is the triple +[product](elementary-number-theory.multiplication-natural-numbers.md) + +```text + n³ := n * n * n +``` + +of `n` with itself. + +## Definitions + +### Cubes of natural numbers + +```agda +cube-ℕ : ℕ → ℕ +cube-ℕ n = square-ℕ n *ℕ n +``` + +### The predicate of being a cube of natural numbers + +```agda +is-cube-ℕ : ℕ → UU lzero +is-cube-ℕ = fiber cube-ℕ +``` + +### The cubic root of cubic natural numbers + +```agda +cubic-root-ℕ : (n : ℕ) → is-cube-ℕ n → ℕ +cubic-root-ℕ n = pr1 +``` + +## See also + +- [Squares of natural numbers](elementary-number-theory.squares-natural-numbers.md) diff --git a/src/elementary-number-theory/hardy-ramanujan-number.lagda.md b/src/elementary-number-theory/hardy-ramanujan-number.lagda.md new file mode 100644 index 0000000000..de257db2f4 --- /dev/null +++ b/src/elementary-number-theory/hardy-ramanujan-number.lagda.md @@ -0,0 +1,73 @@ +# The Hardy-Ramanujan number + +```agda +module elementary-number-theory.hardy-ramanujan-number where +``` + +
Imports + +```agda +open import elementary-number-theory.inequality-natural-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.taxicab-numbers + +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.unit-type +``` + +
+ +## Idea + +The +{{#concept "Hardy-Ramanujan number" Agda=Hardy-Ramanujan-ℕ WD="1729" WDID=Q825176}} +is the number `1729`. This number is the second +[taxicab number](elementary-number-theory.taxicab-numbers.md), i.e., it is the +least natural number that can be written as a sum of cubes of positive natural +numbers in exactly two distinct ways. Specifically, we have the identifications + +```text + 1³ + 12³ ＝ 1729 and 9³ + 10³ ＝ 1729. +``` + +## Definition + +### The Hardy-Ramanujan number + +```agda +Hardy-Ramanujan-ℕ : ℕ +Hardy-Ramanujan-ℕ = 1729 +``` + +## Properties + +### Two decompositions of the Hardy-Ramanujan number into sums of cubes of two positive natural numbers + +```agda +first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ : + sum-of-cubes-decomposition-ℕ Hardy-Ramanujan-ℕ +pr1 first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ = + (1 , is-nonzero-one-ℕ) +pr1 (pr2 first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ) = + (12 , is-nonzero-succ-ℕ 11) +pr1 (pr2 (pr2 first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) = + star +pr2 (pr2 (pr2 first-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) = + refl + +second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ : + sum-of-cubes-decomposition-ℕ Hardy-Ramanujan-ℕ +pr1 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ = + (9 , is-nonzero-succ-ℕ 8) +pr1 (pr2 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ) = + (10 , is-nonzero-succ-ℕ 9) +pr1 (pr2 (pr2 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) = + star +pr2 (pr2 (pr2 second-sum-of-cubes-decomposition-Hardy-Ramanujan-ℕ)) = + refl +``` + +## External links + +- [1729 (number)]() at Wikipedia diff --git a/src/elementary-number-theory/multiplication-natural-numbers.lagda.md b/src/elementary-number-theory/multiplication-natural-numbers.lagda.md index 67a9323edd..bebd14dcb6 100644 --- a/src/elementary-number-theory/multiplication-natural-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-natural-numbers.lagda.md @@ -23,6 +23,19 @@ open import foundation.negated-equality +## Idea + +The {{#concept "multiplication" Disambiguation="natural numbers"}} operation on +the [natural numbers](elementary-number-theory.natural-numbers.md) is defined by +[iteratively](foundation.iterating-functions.md) applying +[addition](elementary-number-theory.addition-natural-numbers.md) of a number to +itself. More preciesly the number `m * n` is defined by adding the number `n` to +itself `m` times: + +```text + m * n = n + ⋯ + n (n added to itself m times). +``` + ## Definition ### Multiplication @@ -239,3 +252,8 @@ neq-mul-ℕ m n p = ( ( right-successor-law-mul-ℕ (succ-ℕ m) (succ-ℕ n)) ∙ ( ap ((succ-ℕ m) +ℕ_) (left-successor-law-mul-ℕ m (succ-ℕ n))))) ``` + +## See also + +- [Squares of natural numbers](elementary-number-theory.squares-natural-numbers.md) +- [Cubes of natural numbers](elementary-number-theory.cubes-natural-numbers.md) diff --git a/src/elementary-number-theory/squares-natural-numbers.lagda.md b/src/elementary-number-theory/squares-natural-numbers.lagda.md index 9c5715f443..e8490a8459 100644 --- a/src/elementary-number-theory/squares-natural-numbers.lagda.md +++ b/src/elementary-number-theory/squares-natural-numbers.lagda.md @@ -28,18 +28,37 @@ open import foundation-core.transport-along-identifications +## Idea + +The {{#concept "square" Disambiguation="natural number"}} `n²` of a +[natural number](elementary-number-theory.natural-numbers.md) `n` is the +[product](elementary-number-theory.multiplication-natural-numbers.md) + +```text + n² := n * n +``` + +of `n` with itself. + ## Definition +### Squares of natural numbers + ```agda square-ℕ : ℕ → ℕ square-ℕ n = mul-ℕ n n +``` -cube-ℕ : ℕ → ℕ -cube-ℕ n = (square-ℕ n) *ℕ n +### The predicate of being a square of a natural number +```agda is-square-ℕ : ℕ → UU lzero is-square-ℕ n = Σ ℕ (λ x → n ＝ square-ℕ x) +``` + +### The square root of a square natural number +```agda square-root-ℕ : (n : ℕ) → is-square-ℕ n → ℕ square-root-ℕ _ (root , _) = root ``` @@ -153,3 +172,7 @@ is-decidable-is-square-ℕ n = ( λ x → has-decidable-equality-ℕ n (square-ℕ x)) ( is-decidable-big-root n) ``` + +## See also + +- [Cubes of natural numbers](elementary-number-theory.cubes-natural-numbers.md) diff --git a/src/elementary-number-theory/taxicab-numbers.lagda.md b/src/elementary-number-theory/taxicab-numbers.lagda.md new file mode 100644 index 0000000000..78c1cc32bf --- /dev/null +++ b/src/elementary-number-theory/taxicab-numbers.lagda.md @@ -0,0 +1,104 @@ +# Taxicab numbers + +```agda +module elementary-number-theory.taxicab-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.cubes-natural-numbers +open import elementary-number-theory.inequality-natural-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-natural-numbers + +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.identity-types +open import foundation.universe-levels + +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +The `n`-th +{{#concept "taxicab number" Agda=is-taxicab-number-ℕ WD="taxicab number" WDID=Q1462591}} +`taxicab n` is the smallest +[natural number](elementary-number-theory.natural-numbers.md) `x` such that `x` +is a [sum](elementary-number-theory.addition-natural-numbers.md) of two +[cubes](elementary-number-theory.cubes-natural-numbers.md) in `n` +[distinct](foundation.negated-equality.md) ways. + +**Note:** The definition of taxicab numbers only considers sums of +[positive integers](elementary-number-theory.nonzero-natural-numbers.md). Note +that if `n` is a cube, i.e., if `n ＝ c³`, then the only solutions to the +equation + +```text + a³ + b³ = c³ +``` + +have either `a ＝ 0` or `b ＝ 0` by +[Fermat's last theorem](https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem). +Therefore `n` can be written in at least two different ways as a sum of cubes of +positive natural numbers if and only if it can be written in at least two +different ways as a sum of cubes of arbitary natural numbers. However, the class +of natural numbers that can be written in exactly one way as a sum of cubes is +different when we consider sums of cubes of positive natural numbers or sums of +cubes of arbitrary natural numbers. + +## Definitions + +### The type of decompositions of a natural number as a sum of cubes + +```agda +sum-of-cubes-decomposition-ℕ : ℕ → UU lzero +sum-of-cubes-decomposition-ℕ x = + Σ ( nonzero-ℕ) + ( λ y → + Σ ( nonzero-ℕ) + ( λ z → + ( leq-ℕ (nat-nonzero-ℕ y) (nat-nonzero-ℕ z)) × + ( cube-ℕ (nat-nonzero-ℕ y) +ℕ cube-ℕ (nat-nonzero-ℕ z) ＝ x))) +``` + +### The predicate of being a sum of two cubes in exactly `n` distinct ways + +A number `x` is a sum of cubes in `n` distinct ways if there is an equivalence + +```text + Fin n ≃ sum-of-cubes-decomposition-ℕ x +``` + +from the +[standard finite type](univalent-combinatorics.standard-finite-types.md) to the +type `sum-of-cubes-decomposition-ℕ x` of ways of writing `x` as a sum of cubes. + +```agda +is-sum-of-cubes-in-number-of-distinct-ways-ℕ : ℕ → ℕ → UU lzero +is-sum-of-cubes-in-number-of-distinct-ways-ℕ n x = + Fin n ≃ sum-of-cubes-decomposition-ℕ x +``` + +### The predicate of being the `n`-th taxicab number + +```agda +is-taxicab-number-ℕ : ℕ → ℕ → UU lzero +is-taxicab-number-ℕ n x = + is-sum-of-cubes-in-number-of-distinct-ways-ℕ n x × + ((y : ℕ) → is-sum-of-cubes-in-number-of-distinct-ways-ℕ n y → leq-ℕ x y) +``` + +## See also + +- [The Hardy-Ramanujan number](elementary-number-theory.hardy-ramanujan-number.md) + +## External links + +- [Taxicab numbers](https://en.wikipedia.org/wiki/Taxicab_number) at Wikipedia +- [Taxicab nubmers](https://oeis.org/A011541) at the OEIS. diff --git a/src/foundation-core/whiskering-homotopies.lagda.md b/src/foundation-core/whiskering-homotopies.lagda.md index e79337e4b3..29803206ab 100644 --- a/src/foundation-core/whiskering-homotopies.lagda.md +++ b/src/foundation-core/whiskering-homotopies.lagda.md @@ -51,38 +51,51 @@ font. For more details, see [How to install](HOWTO-INSTALL.md). ## Definitions -### Whiskering of homotopies +### Left whiskering of homotopies ```agda -htpy-left-whisk : - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} - (h : B → C) {f g : A → B} → f ~ g → (h ∘ f) ~ (h ∘ g) -htpy-left-whisk h H x = ap h (H x) +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} + where + + htpy-left-whisk : + (h : {x : A} → B x → C x) + {f g : (x : A) → B x} → f ~ g → h ∘ f ~ h ∘ g + htpy-left-whisk h H x = ap h (H x) -infixr 15 _·l_ -_·l_ = htpy-left-whisk + infixr 17 _·l_ + _·l_ = htpy-left-whisk +``` -htpy-right-whisk : - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : B → UU l3} - {g h : (y : B) → C y} (H : g ~ h) (f : A → B) → (g ∘ f) ~ (h ∘ f) -htpy-right-whisk H f x = H (f x) +### Right whiskering of homotopies -infixl 15 _·r_ -_·r_ = htpy-right-whisk +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3} + where + + htpy-right-whisk : + {g h : {x : A} (y : B x) → C x y} + (H : {x : A} → g {x} ~ h {x}) + (f : (x : A) → B x) → g ∘ f ~ h ∘ f + htpy-right-whisk H f x = H (f x) + + infixl 16 _·r_ + _·r_ = htpy-right-whisk ``` ### Horizontal composition of homotopies ```agda module _ - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} - {f f' : A → B} {g g' : B → C} + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} + {f f' : (x : A) → B x} {g g' : {x : A} → B x → C x} where - htpy-comp-horizontal : (f ~ f') → (g ~ g') → (g ∘ f) ~ (g' ∘ f') + htpy-comp-horizontal : f ~ f' → ({x : A} → g {x} ~ g' {x}) → g ∘ f ~ g' ∘ f' htpy-comp-horizontal F G = (g ·l F) ∙h (G ·r f') - htpy-comp-horizontal' : (f ~ f') → (g ~ g') → (g ∘ f) ~ (g' ∘ f') + htpy-comp-horizontal' : f ~ f' → ({x : A} → g {x} ~ g' {x}) → g ∘ f ~ g' ∘ f' htpy-comp-horizontal' F G = (G ·r f) ∙h (g' ·l F) ``` @@ -96,23 +109,37 @@ homotopy side. ```agda module _ - { l1 l2 : Level} {A : UU l1} {B : UU l2} + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where - left-unit-law-left-whisk-htpy : {f f' : A → B} → (H : f ~ f') → id ·l H ~ H + left-unit-law-left-whisk-htpy : + {f f' : (x : A) → B x} → (H : f ~ f') → id ·l H ~ H left-unit-law-left-whisk-htpy H x = ap-id (H x) +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} + where + right-unit-law-left-whisk-htpy : - { l3 : Level} {C : UU l3} {f : A → B} (g : B → C) → + {f : (x : A) → B x} (g : {x : A} → B x → C x) → g ·l refl-htpy {f = f} ~ refl-htpy right-unit-law-left-whisk-htpy g = refl-htpy +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3} + where + left-unit-law-right-whisk-htpy : - {l3 : Level} {C : UU l3} {g : B → C} (f : A → B) → + {g : {x : A} (y : B x) → C x y} (f : (x : A) → B x) → refl-htpy {f = g} ·r f ~ refl-htpy left-unit-law-right-whisk-htpy f = refl-htpy - right-unit-law-right-whisk-htpy : {f f' : A → B} → (H : f ~ f') → H ·r id ~ H +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + right-unit-law-right-whisk-htpy : + {f f' : (x : A) → B x} → (H : f ~ f') → H ·r id ~ H right-unit-law-right-whisk-htpy H = refl-htpy ``` @@ -120,71 +147,79 @@ module _ ```agda module _ - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} + {f f' : (x : A) → B x} (g : {x : A} → B x → C x) (H : f ~ f') where - left-whisk-inv-htpy : - {f f' : A → B} (g : B → C) (H : f ~ f') → - (g ·l (inv-htpy H)) ~ inv-htpy (g ·l H) - left-whisk-inv-htpy g H x = ap-inv g (H x) + left-whisk-inv-htpy : g ·l (inv-htpy H) ~ inv-htpy (g ·l H) + left-whisk-inv-htpy x = ap-inv g (H x) - inv-htpy-left-whisk-inv-htpy : - {f f' : A → B} (g : B → C) (H : f ~ f') → - inv-htpy (g ·l H) ~ (g ·l (inv-htpy H)) - inv-htpy-left-whisk-inv-htpy g H = - inv-htpy (left-whisk-inv-htpy g H) + inv-htpy-left-whisk-inv-htpy : inv-htpy (g ·l H) ~ g ·l (inv-htpy H) + inv-htpy-left-whisk-inv-htpy = inv-htpy left-whisk-inv-htpy - right-whisk-inv-htpy : - {g g' : B → C} (H : g ~ g') (f : A → B) → - ((inv-htpy H) ·r f) ~ (inv-htpy (H ·r f)) - right-whisk-inv-htpy H f = refl-htpy +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3} + {g g' : {x : A} (y : B x) → C x y} (H : {x : A} → g {x} ~ g' {x}) + (f : (x : A) → B x) + where - inv-htpy-right-whisk-inv-htpy : - {g g' : B → C} (H : g ~ g') (f : A → B) → - ((inv-htpy H) ·r f) ~ (inv-htpy (H ·r f)) - inv-htpy-right-whisk-inv-htpy H f = - inv-htpy (right-whisk-inv-htpy H f) + right-whisk-inv-htpy : inv-htpy H ·r f ~ inv-htpy (H ·r f) + right-whisk-inv-htpy = refl-htpy + + inv-htpy-right-whisk-inv-htpy : inv-htpy H ·r f ~ inv-htpy (H ·r f) + inv-htpy-right-whisk-inv-htpy = inv-htpy right-whisk-inv-htpy ``` ### Distributivity of whiskering over composition of homotopies ```agda module _ - { l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} where distributive-left-whisk-concat-htpy : - { f g h : A → B} (k : B → C) → + { f g h : (x : A) → B x} (k : {x : A} → B x → C x) → ( H : f ~ g) (K : g ~ h) → - ( k ·l (H ∙h K)) ~ ((k ·l H) ∙h (k ·l K)) + k ·l (H ∙h K) ~ (k ·l H) ∙h (k ·l K) distributive-left-whisk-concat-htpy k H K a = ap-concat k (H a) (K a) +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3} + (k : (x : A) → B x) {f g h : {x : A} (y : B x) → C x y} + (H : {x : A} → f {x} ~ g {x}) (K : {x : A} → g {x} ~ h {x}) + where + distributive-right-whisk-concat-htpy : - ( k : A → B) {f g h : B → C} → - ( H : f ~ g) (K : g ~ h) → - ( (H ∙h K) ·r k) ~ ((H ·r k) ∙h (K ·r k)) - distributive-right-whisk-concat-htpy k H K = refl-htpy + (H ∙h K) ·r k ~ (H ·r k) ∙h (K ·r k) + distributive-right-whisk-concat-htpy = refl-htpy ``` ### Associativity of whiskering and function composition ```agda module _ - { l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : A → UU l2} {C : A → UU l3} {D : A → UU l4} where associative-left-whisk-comp : - ( k : C → D) (h : B → C) {f g : A → B} → + ( k : {x : A} → C x → D x) (h : {x : A} → B x → C x) {f g : (x : A) → B x} ( H : f ~ g) → - ( k ·l (h ·l H)) ~ ((k ∘ h) ·l H) + k ·l (h ·l H) ~ (k ∘ h) ·l H associative-left-whisk-comp k h H x = inv (ap-comp k h (H x)) - associative-right-whisk-comp : - { f g : C → D} (h : B → C) (k : A → B) → - ( H : f ~ g) → - ( (H ·r h) ·r k) ~ (H ·r (h ∘ k)) - associative-right-whisk-comp h k H = refl-htpy +module _ + { l1 l2 l3 l4 : Level} + { A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3} + { D : (x : A) (y : B x) (z : C x y) → UU l4} + { f g : {x : A} {y : B x} (z : C x y) → D x y z} + ( h : {x : A} (y : B x) → C x y) (k : (x : A) → B x) + ( H : {x : A} {y : B x} → f {x} {y} ~ g {x} {y}) + where + + associative-right-whisk-comp : (H ·r h) ·r k ~ H ·r (h ∘ k) + associative-right-whisk-comp = refl-htpy ``` ### A coherence for homotopies to the identity function @@ -194,10 +229,10 @@ module _ {l : Level} {A : UU l} {f : A → A} (H : f ~ id) where - coh-htpy-id : (H ·r f) ~ (f ·l H) + coh-htpy-id : H ·r f ~ f ·l H coh-htpy-id x = is-injective-concat' (H x) (nat-htpy-id H (H x)) - inv-htpy-coh-htpy-id : (f ·l H) ~ (H ·r f) + inv-htpy-coh-htpy-id : f ·l H ~ H ·r f inv-htpy-coh-htpy-id = inv-htpy coh-htpy-id ``` @@ -205,15 +240,46 @@ module _ ```agda module _ - { l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} - { f g : A → B} + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} + {f g : (x : A) → B x} where ap-left-whisk-htpy : - ( h : B → C) {H H' : f ~ g} (α : H ~ H') → h ·l H ~ h ·l H' - ap-left-whisk-htpy h α x = ap (ap h) (α x) + (h : {x : A} → B x → C x) {H H' : f ~ g} (α : H ~ H') → h ·l H ~ h ·l H' + ap-left-whisk-htpy h α = (ap h) ·l α + +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3} + {f g : {x : A} (y : B x) → C x y} {H H' : {x : A} → f {x} ~ g {x}} + where ap-right-whisk-htpy : - { H H' : f ~ g} (α : H ~ H') (h : C → A) → H ·r h ~ H' ·r h + (α : {x : A} → H {x} ~ H' {x}) (h : (x : A) → B x) → H ·r h ~ H' ·r h ap-right-whisk-htpy α h = α ·r h ``` + +### The left and right whiskering operations commute + +We have the coherence + +```text + (h ·l H) ·r h' ~ h ·l (H ·r h') +``` + +and, in fact, this equation holds definitionally. + +```agda +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : A → UU l2} + {C : {x : A} → B x → UU l3} {D : {x : A} → B x → UU l4} + {f g : {x : A} (y : B x) → C y} + where + + coherence-left-right-whisk-htpy : + (h : {x : A} {y : B x} → C y → D y) + (H : {x : A} → f {x} ~ g {x}) + (h' : (x : A) → B x) → + (h ·l H) ·r h' ~ h ·l (H ·r h') + coherence-left-right-whisk-htpy h H h' = refl-htpy +``` diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 3ce72252c2..55a3c1bc23 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -68,6 +68,8 @@ open import foundation.constant-maps public open import foundation.constant-type-families public open import foundation.contractible-maps public open import foundation.contractible-types public +open import foundation.copartial-elements public +open import foundation.copartial-functions public open import foundation.coproduct-decompositions public open import foundation.coproduct-decompositions-subuniverse public open import foundation.coproduct-types public @@ -221,6 +223,8 @@ open import foundation.negation public open import foundation.noncontractible-types public open import foundation.pairs-of-distinct-elements public open import foundation.partial-elements public +open import foundation.partial-functions public +open import foundation.partial-sequences public open import foundation.partitions public open import foundation.path-algebra public open import foundation.path-split-maps public @@ -308,6 +312,8 @@ open import foundation.symmetric-operations public open import foundation.telescopes public open import foundation.tight-apartness-relations public open import foundation.torsorial-type-families public +open import foundation.total-partial-elements public +open import foundation.total-partial-functions public open import foundation.towers public open import foundation.transfinite-cocomposition-of-maps public open import foundation.transport-along-equivalences public diff --git a/src/foundation/copartial-elements.lagda.md b/src/foundation/copartial-elements.lagda.md new file mode 100644 index 0000000000..85cb76b1ce --- /dev/null +++ b/src/foundation/copartial-elements.lagda.md @@ -0,0 +1,141 @@ +# Copartial elements + +```agda +module foundation.copartial-elements where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.universe-levels + +open import foundation-core.propositions + +open import orthogonal-factorization-systems.closed-modalities +``` + +
+ +## Idea + +A {{#concept "copartial element" Agda=copartial-element}} of a type `A` is an +element of type + +```text + Σ (Q : Prop), A * Q +``` + +where the type `A * Q` is the +[join](synthetic-homotopy-theory.joins-of-types.md) of `Q` and `A`. We say that +a copartial element `(Q , u)` is +{{#concept "erased" Disambiguation="copartial element" Agda=is-erased-copartial-element}} +if the proposition `Q` holds. + +In order to compare copartial elements with +[partial elements](foundation.partial-elements.md), note that we have the +following [pullback squares](foundation.pullback-squares.md) + +```text + A -----> Σ (Q : Prop), A * Q 1 -----> Σ (P : Prop), (P → A) + | ⌟ | | ⌟ | + | | | | + V V V V + 1 -----------> Prop 1 -----------> Prop + F F + + 1 -----> Σ (Q : Prop), A * Q A -----> Σ (P : Prop), (P → A) + | ⌟ | | ⌟ | + | | | | + V V V V + 1 -----------> Prop 1 -----------> Prop + T T +``` + +Note that we make use of the +[closed modalities](orthogonal-factorization-systems.closed-modalities.md) +`A ↦ A * Q` in the formulation of copartial element, whereas the formulation of +partial elements makes use of the +[open modalities](orthogonal-factorization-systems.open-modalities.md). The +concepts of partial and copartial elements are dual in that sense. + +Alternatively, the type of copartial elements of a type `A` can be defined as +the [pushout-product](synthetic-homotopy-theory.pushout-products.md) + +```text + A 1 + | | + ! | □ | T + V V + 1 Prop +``` + +This point of view is useful in order to establish that copartial elements of +copartial elements induce copartial elements. Indeed, note that +`(A □ T) □ T ＝ A □ (T □ T)` by associativity of the pushout product, and that +`T` is a pushout-product algebra in the sense that + +```text + P Q x ↦ (P * Q , x) + 1 1 Σ (P Q : Prop), P * Q ---------------------> 1 + | | | | + T | □ | T = T □ T | | + V V V V + Prop Prop Prop² ------------------------------> Prop + P Q ↦ P * Q +``` + +By this [morphism of arrows](foundation.morphisms-arrows.md) it follows that +there is a morphism of arrows + +```text + join-copartial-element : (A □ T) □ T → A □ T, +``` + +i.e., that copartial copartial elements induce copartial elements. These +considerations allow us to compose +[copartial functions](foundation.copartial-functions.md). + +**Note:** The topic of copartial functions was not known to us in the +literature, and our formalization on this topic should be considered +experimental. + +## Definition + +### Copartial elements + +```agda +copartial-element : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2) +copartial-element l2 A = + Σ (Prop l2) (λ Q → operator-closed-modality Q A) + +module _ + {l1 l2 : Level} {A : UU l1} (a : copartial-element l2 A) + where + + is-erased-prop-copartial-element : Prop l2 + is-erased-prop-copartial-element = pr1 a + + is-erased-copartial-element : UU l2 + is-erased-copartial-element = + type-Prop is-erased-prop-copartial-element +``` + +### The unit of the copartial element operator + +```agda +module _ + {l1 : Level} {A : UU l1} (a : A) + where + + is-erased-prop-unit-copartial-element : Prop lzero + is-erased-prop-unit-copartial-element = empty-Prop + + is-erased-unit-copartial-element : UU lzero + is-erased-unit-copartial-element = empty + + unit-copartial-element : copartial-element lzero A + pr1 unit-copartial-element = is-erased-prop-unit-copartial-element + pr2 unit-copartial-element = unit-closed-modality empty-Prop a +``` diff --git a/src/foundation/copartial-functions.lagda.md b/src/foundation/copartial-functions.lagda.md new file mode 100644 index 0000000000..b09633c4ad --- /dev/null +++ b/src/foundation/copartial-functions.lagda.md @@ -0,0 +1,160 @@ +# Copartial functions + +```agda +module foundation.copartial-functions where +``` + +
Imports + +```agda +open import foundation.copartial-elements +open import foundation.propositions +open import foundation.universe-levels +``` + +
+ +## Idea + +A {{#concept "copartial function" Agda=copartial-function}} from `A` to `B` is a +map from `A` into the type of +[copartial elements](foundation.copartial-elements.md) of `B`. I.e., a copartial +function is a map + +```text + A → Σ (Q : Prop), B * Q +``` + +where `- * Q` is the +[closed modality](orthogonal-factorization-systems.closed-modalities.md), which +is defined by the [join operation](synthetic-homotopy-theory.joins-of-types.md). + +A value of a copartial function `f` at `a : A` is said to be +{{#concept "erased" Disambiguation="copartial function" Agda=is-erased-copartial-function}} +if the copartial element `f a` of `B` is erased. + +A copartial function is [equivalently](foundation-core.equivalences.md) +described as a [morphism of arrows](foundation.morphisms-arrows.md) + +```text + A B 1 + | | | + id | ⇒ | □ | T + V V V + A 1 Prop +``` + +where `□` is the +[pushout-product](synthetic-homotopy-theory.pushout-products.md). Indeed, the +domain of the pushout-product `B □ T` is the type of copartial elements of `B`. + +{{#concept "Composition" Disambiguation="copartial functions"}} of copartial +functions can be defined by + +```text + copartial-element (copartial-element C) + ∧ | + map-copartial-element g / | join-copartial-element + / V + A ----> copartial-element B copartial-element C + f +``` + +In this diagram, the map going up is defined by functoriality of the operation + +```text + X ↦ Σ (Q : Prop), X * Q +``` + +The map going down is defined by the join operation on copartial elements, i.e., +the pushout-product algebra structure of the map `T : 1 → Prop`. The main idea +behind composition of copartial functions is that a composite of copartial +function is erased on the union of the subtypes where each factor is erased. +Indeed, if `f` is erased at `a` or `map-copartial-eleemnt g` is erased at the +copartial element `f a` of `B`, then the composite of copartial functions +`g ∘ f` should be erased at `a`. + +**Note:** The topic of copartial functions was not known to us in the +literature, and our formalization on this topic should be considered +experimental. + +## Definitions + +### Copartial dependent functions + +```agda +copartial-dependent-function : + {l1 l2 : Level} (l3 : Level) (A : UU l1) → (A → UU l2) → + UU (l1 ⊔ l2 ⊔ lsuc l3) +copartial-dependent-function l3 A B = (x : A) → copartial-element l3 (B x) +``` + +### Copartial functions + +```agda +copartial-function : + {l1 l2 : Level} (l3 : Level) → UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ lsuc l3) +copartial-function l3 A B = copartial-dependent-function l3 A (λ _ → B) +``` + +### Erased values of copartial dependent functions + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} + (f : copartial-dependent-function l3 A B) (a : A) + where + + is-erased-prop-copartial-dependent-function : Prop l3 + is-erased-prop-copartial-dependent-function = + is-erased-prop-copartial-element (f a) + + is-erased-copartial-dependent-function : UU l3 + is-erased-copartial-dependent-function = is-erased-copartial-element (f a) +``` + +### Erased values of copartial functions + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : copartial-function l3 A B) + (a : A) + where + + is-erased-prop-copartial-function : Prop l3 + is-erased-prop-copartial-function = + is-erased-prop-copartial-dependent-function f a + + is-erased-copartial-function : UU l3 + is-erased-copartial-function = + is-erased-copartial-dependent-function f a +``` + +### Copartial dependent functions obtained from dependent functions + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) + where + + copartial-dependent-function-dependent-function : + copartial-dependent-function lzero A B + copartial-dependent-function-dependent-function a = + unit-copartial-element (f a) +``` + +### Copartial functions obtained from functions + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + copartial-function-function : copartial-function lzero A B + copartial-function-function = + copartial-dependent-function-dependent-function f +``` + +## See also + +- [Partial functions](foundation.partial-functions.md) diff --git a/src/foundation/partial-elements.lagda.md b/src/foundation/partial-elements.lagda.md index a66e1fdb39..ca67ef0cb8 100644 --- a/src/foundation/partial-elements.lagda.md +++ b/src/foundation/partial-elements.lagda.md @@ -18,24 +18,59 @@ open import foundation-core.propositions ## Idea -A **partial element** of `X` consists of a -[proposition](foundation-core.propositions.md) `P` and a map `P → X`. We say -that a partial element `(P, f)` is **defined** if the proposition `P` holds. +A {{#concept "partial element" Agda=partial-element}} of `X` consists of a +[proposition](foundation-core.propositions.md) `P` and a map `P → X`. That is, +the type of partial elements of `X` is defined to be + +```text + Σ (P : Prop), (P → X). +``` + +We say that a partial element `(P, f)` is +{{#concept "defined" Disambiguation="partial element"}} if the proposition `P` +holds. + +Alternatively, the type of partial elements of `X` can be descibed as the +codomain of the +[composition](species.composition-cauchy-series-species-of-types.md) + +```text + 1 ∅ ∅ + | | | + T | ∘ | = | + V V V + Prop X P T X +``` + +of [polynomial-endofunctors.md](trees.polynomial-endofunctors.md). Indeed, the +codomain of this composition operation of morphisms is the polynomial +endofunctor `P T` of the map `T : 1 → Prop` evaluated at `X`, which is exactly +the type of partial elements of `X`. + +## Definitions + +### Partial elements of a type ```agda partial-element : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2) partial-element l2 X = Σ (Prop l2) (λ P → type-Prop P → X) -is-defined-partial-element-Prop : - {l1 l2 : Level} {X : UU l1} (x : partial-element l2 X) → Prop l2 -is-defined-partial-element-Prop x = pr1 x +module _ + {l1 l2 : Level} {X : UU l1} (x : partial-element l2 X) + where + + is-defined-prop-partial-element : Prop l2 + is-defined-prop-partial-element = pr1 x + + is-defined-partial-element : UU l2 + is-defined-partial-element = type-Prop is-defined-prop-partial-element +``` -is-defined-partial-element : - {l1 l2 : Level} {X : UU l1} (x : partial-element l2 X) → UU l2 -is-defined-partial-element x = type-Prop (is-defined-partial-element-Prop x) +### The unit of the partial element operator +```agda unit-partial-element : - {l1 l2 : Level} {X : UU l1} → X → partial-element lzero X + {l1 : Level} {X : UU l1} → X → partial-element lzero X pr1 (unit-partial-element x) = unit-Prop pr2 (unit-partial-element x) y = x ``` @@ -46,3 +81,10 @@ pr2 (unit-partial-element x) y = x This remains to be shown. [#734](https://github.com/UniMath/agda-unimath/issues/734) + +## See also + +- [Copartial elements](foundation.copartial-elements.md) +- [Partial functions](foundation.partial-functions.md) +- [Partial sequences](foundation.partial-sequences.md) +- [Total partial functions](foundation.total-partial-functions.md) diff --git a/src/foundation/partial-functions.lagda.md b/src/foundation/partial-functions.lagda.md new file mode 100644 index 0000000000..48b08e0e37 --- /dev/null +++ b/src/foundation/partial-functions.lagda.md @@ -0,0 +1,129 @@ +# Partial functions + +```agda +module foundation.partial-functions where +``` + +
Imports + +```agda +open import foundation.partial-elements +open import foundation.propositions +open import foundation.universe-levels +``` + +
+ +## Idea + +A {{#concept "partial function"}} from `A` to `B` is a function from `A` into +the type of [partial elements](foundation.partial-elements.md) of `B`. In other +words, a partial function is a function + +```text + A → Σ (P : Prop), (P → B). +``` + +Given a partial function `f : A → B` and an element `a : A`, we say that `f` is +{{#concept "defined" Disambiguation="partial function"}} at `a` if the partial +element `f a` of `A` is defined. + +Partial functions can be described +[equivalently](foundation-core.equivalences.md) as +[morphisms of arrows](foundation.morphisms-arrows.md) + +```text + ∅ 1 ∅ + | | | + | ⇒ | ∘ | + V V V + A Prop B +``` + +where the composition operation is +[composition](species.composition-cauchy-series-species-of-types.md) of +[polynomial endofunctors](trees.polynomial-endofunctors.md). + +## Definitions + +### Partial dependent functions + +```agda +partial-dependent-function : + {l1 l2 : Level} (l3 : Level) (A : UU l1) (B : A → UU l2) → + UU (l1 ⊔ l2 ⊔ lsuc l3) +partial-dependent-function l3 A B = + (x : A) → partial-element l3 (B x) +``` + +### Partial functions + +```agda +partial-function : + {l1 l2 : Level} (l3 : Level) → UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ lsuc l3) +partial-function l3 A B = partial-dependent-function l3 A (λ _ → B) +``` + +### The predicate on partial dependent functions of being defined at an element in the domain + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} + (f : partial-dependent-function l3 A B) (a : A) + where + + is-defined-prop-partial-dependent-function : Prop l3 + is-defined-prop-partial-dependent-function = + is-defined-prop-partial-element (f a) + + is-defined-partial-dependent-function : UU l3 + is-defined-partial-dependent-function = + type-Prop is-defined-prop-partial-dependent-function +``` + +### The predicate on partial functions of being defined at an element in the domain + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : partial-function l3 A B) + (a : A) + where + + is-defined-prop-partial-function : Prop l3 + is-defined-prop-partial-function = + is-defined-prop-partial-dependent-function f a + + is-defined-partial-function : UU l3 + is-defined-partial-function = + is-defined-partial-dependent-function f a +``` + +### The partial dependent function obtained from a dependent function + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) + where + + partial-dependent-function-dependent-function : + partial-dependent-function lzero A B + partial-dependent-function-dependent-function a = + unit-partial-element (f a) +``` + +### The partial function obtained from a function + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + partial-function-function : partial-function lzero A B + partial-function-function = partial-dependent-function-dependent-function f +``` + +## See also + +- [Copartial functions](foundation.copartial-functions.md) +- [Partial elements](foundation.partial-elements.md) +- [Partial sequences](foundation.partial-sequences.md) diff --git a/src/foundation/partial-sequences.lagda.md b/src/foundation/partial-sequences.lagda.md new file mode 100644 index 0000000000..dd8e77715c --- /dev/null +++ b/src/foundation/partial-sequences.lagda.md @@ -0,0 +1,53 @@ +# Partial sequences + +```agda +module foundation.partial-sequences where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.partial-functions +open import foundation.propositions +open import foundation.universe-levels +``` + +
+ +## Idea + +A {{#concept "partial sequence"}} of elements of a type `A` is a +[partial function](foundation.partial-functions.md) from `ℕ` to `A`. In other +words, a partial sequence is a map + +```text + ℕ → Σ (P : Prop), (P → A) +``` + +from `ℕ` into the type of [partial elements](foundation.partial-elements.md) of +`A`. + +## Definitions + +### Partial sequences + +```agda +partial-sequence : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2) +partial-sequence l2 A = partial-function l2 ℕ A +``` + +### Defined elements of partial sequences + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (a : partial-sequence l2 A) + where + + is-defined-prop-partial-sequence : ℕ → Prop l2 + is-defined-prop-partial-sequence = is-defined-prop-partial-function a + + is-defined-partial-sequence : ℕ → UU l2 + is-defined-partial-sequence = is-defined-partial-function a +``` diff --git a/src/foundation/total-partial-elements.lagda.md b/src/foundation/total-partial-elements.lagda.md new file mode 100644 index 0000000000..16df4f4925 --- /dev/null +++ b/src/foundation/total-partial-elements.lagda.md @@ -0,0 +1,33 @@ +# Total partial elements + +```agda +module foundation.total-partial-elements where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.partial-elements +open import foundation.universe-levels +``` + +
+ +## Idea + +A [partial element](foundation.partial-elements.md) `a` of `A` is said to be +{{#concept "total" Disambiguation="partial element"}} if it is defined. The type +of total partial elements of `A` is +[equivalent](foundation-core.equivalences.md) to the type `A`. + +## Definitions + +### The type of total partial elements + +```agda +total-partial-element : + {l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2) +total-partial-element l2 A = + Σ (partial-element l2 A) is-defined-partial-element +``` diff --git a/src/foundation/total-partial-functions.lagda.md b/src/foundation/total-partial-functions.lagda.md new file mode 100644 index 0000000000..3e7c2e0660 --- /dev/null +++ b/src/foundation/total-partial-functions.lagda.md @@ -0,0 +1,51 @@ +# Total partial functions + +```agda +module foundation.total-partial-functions where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.partial-functions +open import foundation.propositions +open import foundation.universe-levels +``` + +
+ +## Idea + +A [partial function](foundation.partial-functions.md) `f : A → B` is said to be +{{#concept "total" Disambiguation="partial function" Agda=is-total-partial-function}} +if the [partial element](foundation.partial-elements.md) `f a` of `B` is defined +for every `a : A`. The type of total partial functions from `A` to `B` is +[equivalent](foundation-core.equivalences.md) to the type of +[functions](foundation-core.function-types.md) from `A` to `B`. + +## Definitions + +### The predicate of being a total partial function + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : partial-function l3 A B) + where + + is-total-prop-partial-function : Prop (l1 ⊔ l3) + is-total-prop-partial-function = + Π-Prop A (is-defined-prop-partial-function f) + + is-total-partial-function : UU (l1 ⊔ l3) + is-total-partial-function = type-Prop is-total-prop-partial-function +``` + +### The type of total partial functions + +```agda +total-partial-function : + {l1 l2 : Level} (l3 : Level) → UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ lsuc l3) +total-partial-function l3 A B = + Σ (partial-function l3 A B) is-total-partial-function +``` diff --git a/src/foundation/universal-property-equivalences.lagda.md b/src/foundation/universal-property-equivalences.lagda.md index 519a9a8bf4..fea8d6c9ce 100644 --- a/src/foundation/universal-property-equivalences.lagda.md +++ b/src/foundation/universal-property-equivalences.lagda.md @@ -105,3 +105,15 @@ module _ ( f) ( λ C → H (pr1 C)) ``` + +#### If dependent precomposition by `f` is an equivalence, then `f` is an equivalence + +```agda +abstract + is-equiv-is-equiv-precomp-Π : + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → + dependent-universal-property-equiv f → + is-equiv f + is-equiv-is-equiv-precomp-Π f H = + is-equiv-is-equiv-precomp f (is-equiv-precomp-is-equiv-precomp-Π f H) +``` diff --git a/src/orthogonal-factorization-systems/closed-modalities.lagda.md b/src/orthogonal-factorization-systems/closed-modalities.lagda.md index 0b18cf063c..7c79d77436 100644 --- a/src/orthogonal-factorization-systems/closed-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/closed-modalities.lagda.md @@ -38,11 +38,11 @@ call these the **closed modalities**. ```agda operator-closed-modality : - (l : Level) {lQ : Level} (Q : Prop lQ) → operator-modality l (l ⊔ lQ) -operator-closed-modality l Q A = A * type-Prop Q + {l lQ : Level} (Q : Prop lQ) → operator-modality l (l ⊔ lQ) +operator-closed-modality Q A = A * type-Prop Q unit-closed-modality : - {l lQ : Level} (Q : Prop lQ) → unit-modality (operator-closed-modality l Q) + {l lQ : Level} (Q : Prop lQ) → unit-modality (operator-closed-modality {l} Q) unit-closed-modality Q = inl-join is-closed-modal : @@ -63,7 +63,7 @@ module _ is-reflective-subuniverse-closed-modality : is-reflective-subuniverse {l ⊔ lQ} (is-closed-modal Q) pr1 is-reflective-subuniverse-closed-modality = - operator-closed-modality (l ⊔ lQ) Q + operator-closed-modality {l ⊔ lQ} Q pr1 (pr2 is-reflective-subuniverse-closed-modality) = unit-closed-modality Q pr1 (pr2 (pr2 is-reflective-subuniverse-closed-modality)) A q = diff --git a/src/synthetic-homotopy-theory/dependent-universal-property-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/dependent-universal-property-sequential-colimits.lagda.md index 7da1b9e746..3797fd704a 100644 --- a/src/synthetic-homotopy-theory/dependent-universal-property-sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-universal-property-sequential-colimits.lagda.md @@ -7,19 +7,30 @@ module synthetic-homotopy-theory.dependent-universal-property-sequential-colimit
Imports ```agda +open import foundation.action-on-identifications-functions +open import foundation.commuting-triangles-of-maps open import foundation.contractible-maps open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.fibers-of-maps +open import foundation.function-types open import foundation.functoriality-dependent-pair-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.precomposition-dependent-functions +open import foundation.precomposition-functions +open import foundation.subtype-identity-principle +open import foundation.universal-property-equivalences open import foundation.universe-levels open import synthetic-homotopy-theory.cocones-under-sequential-diagrams +open import synthetic-homotopy-theory.coforks open import synthetic-homotopy-theory.dependent-cocones-under-sequential-diagrams open import synthetic-homotopy-theory.dependent-coforks open import synthetic-homotopy-theory.dependent-universal-property-coequalizers open import synthetic-homotopy-theory.sequential-diagrams +open import synthetic-homotopy-theory.universal-property-coequalizers open import synthetic-homotopy-theory.universal-property-sequential-colimits ``` @@ -62,7 +73,7 @@ module _ module _ { l1 l2 l3 : Level} (A : sequential-diagram l1) {X : UU l2} ( c : cocone-sequential-diagram A X) {P : X → UU l3} - ( dup-sequential-colimit : + ( dup-c : dependent-universal-property-sequential-colimit A c) where @@ -70,7 +81,7 @@ module _ dependent-cocone-sequential-diagram A c P → ( x : X) → P x map-dependent-universal-property-sequential-colimit = - map-inv-is-equiv (dup-sequential-colimit P) + map-inv-is-equiv (dup-c P) ``` ## Properties @@ -81,7 +92,7 @@ module _ module _ { l1 l2 l3 : Level} (A : sequential-diagram l1) {X : UU l2} ( c : cocone-sequential-diagram A X) {P : X → UU l3} - ( dup-sequential-colimit : + ( dup-c : dependent-universal-property-sequential-colimit A c) ( d : dependent-cocone-sequential-diagram A c P) where @@ -90,17 +101,17 @@ module _ htpy-dependent-cocone-sequential-diagram A P ( dependent-cocone-map-sequential-diagram A c P ( map-dependent-universal-property-sequential-colimit A c - ( dup-sequential-colimit) + ( dup-c) ( d))) ( d) htpy-dependent-cocone-dependent-universal-property-sequential-colimit = htpy-eq-dependent-cocone-sequential-diagram A P ( dependent-cocone-map-sequential-diagram A c P ( map-dependent-universal-property-sequential-colimit A c - ( dup-sequential-colimit) + ( dup-c) ( d))) ( d) - ( is-section-map-inv-is-equiv (dup-sequential-colimit P) d) + ( is-section-map-inv-is-equiv (dup-c P) d) abstract uniqueness-dependent-universal-property-sequential-colimit : @@ -118,7 +129,7 @@ module _ extensionality-dependent-cocone-sequential-diagram A P ( dependent-cocone-map-sequential-diagram A c P h) ( d))) - ( is-contr-map-is-equiv (dup-sequential-colimit P) d) + ( is-contr-map-is-equiv (dup-c P) d) ``` ### Correspondence between dependent universal properties of sequential colimits and coequalizers @@ -162,7 +173,7 @@ module _ ( top-map-cofork-cocone-sequential-diagram A) ( cofork-cocone-sequential-diagram A c)) dependent-universal-property-coequalizer-dependent-universal-property-sequential-colimit - ( dup-sequential-colimit) + ( dup-c) ( P) = is-equiv-top-map-triangle ( dependent-cocone-map-sequential-diagram A c P) @@ -173,7 +184,7 @@ module _ ( cofork-cocone-sequential-diagram A c)) ( triangle-dependent-cocone-sequential-diagram-dependent-cofork A c P) ( is-equiv-dependent-cocone-sequential-diagram-dependent-cofork A c P) - ( dup-sequential-colimit P) + ( dup-c P) ``` ### The non-dependent and dependent universal properties of sequential colimits are logically equivalent @@ -188,7 +199,7 @@ module _ dependent-universal-property-sequential-colimit A c → universal-property-sequential-colimit A c universal-property-dependent-universal-property-sequential-colimit - ( dup-sequential-colimit) + ( dup-c) ( Y) = is-equiv-left-map-triangle ( cocone-map-sequential-diagram A c) @@ -196,7 +207,7 @@ module _ ( dependent-cocone-map-sequential-diagram A c (λ _ → Y)) ( triangle-compute-dependent-cocone-sequential-diagram-constant-family A c ( Y)) - ( dup-sequential-colimit (λ _ → Y)) + ( dup-c (λ _ → Y)) ( is-equiv-map-equiv ( compute-dependent-cocone-sequential-diagram-constant-family A c Y)) @@ -217,3 +228,75 @@ module _ ( c) ( up-sequential-diagram))) ``` + +### The 3-for-2 property of the dependent universal property of sequential colimits + +Given two cocones under a sequential diagram, one of which has the dependent +universal property of sequential colimits, and a map between their vertices, we +prove that the other has the dependent universal property if and only if the map +is an [equivalence](foundation.equivalences.md). + +```agda +module _ + { l1 l2 l3 : Level} (A : sequential-diagram l1) {X : UU l2} {Y : UU l3} + ( c : cocone-sequential-diagram A X) + ( c' : cocone-sequential-diagram A Y) + ( h : X → Y) + ( H : + htpy-cocone-sequential-diagram A (cocone-map-sequential-diagram A c h) c') + where + + abstract + is-equiv-dependent-universal-property-sequential-colimit-dependent-universal-property-sequential-colimit : + dependent-universal-property-sequential-colimit A c → + dependent-universal-property-sequential-colimit A c' → + is-equiv h + is-equiv-dependent-universal-property-sequential-colimit-dependent-universal-property-sequential-colimit + ( dup-c) + ( dup-c') = + is-equiv-universal-property-sequential-colimit-universal-property-sequential-colimit + ( A) + ( c) + ( c') + ( h) + ( H) + ( universal-property-dependent-universal-property-sequential-colimit + ( A) c dup-c) + ( universal-property-dependent-universal-property-sequential-colimit + ( A) c' dup-c') + + dependent-universal-property-sequential-colimit-is-equiv-dependent-universal-property-sequential-colimit : + dependent-universal-property-sequential-colimit A c → + is-equiv h → + dependent-universal-property-sequential-colimit A c' + dependent-universal-property-sequential-colimit-is-equiv-dependent-universal-property-sequential-colimit + ( dup-c) (is-equiv-h) = + dependent-universal-property-universal-property-sequential-colimit A c' + ( universal-property-sequential-colimit-is-equiv-universal-property-sequential-colimit + ( A) + ( c) + ( c') + ( h) + ( H) + ( universal-property-dependent-universal-property-sequential-colimit + ( A) c dup-c) + ( is-equiv-h)) + + dependent-universal-property-sequential-colimit-dependent-universal-property-sequential-colimit-is-equiv : + is-equiv h → + dependent-universal-property-sequential-colimit A c' → + dependent-universal-property-sequential-colimit A c + dependent-universal-property-sequential-colimit-dependent-universal-property-sequential-colimit-is-equiv + ( is-equiv-h) + ( dup-c') = + dependent-universal-property-universal-property-sequential-colimit A c + ( universal-property-sequential-colimit-universal-property-sequential-colimit-is-equiv + ( A) + ( c) + ( c') + ( h) + ( H) + ( is-equiv-h) + ( universal-property-dependent-universal-property-sequential-colimit + ( A) c' dup-c')) +``` diff --git a/src/synthetic-homotopy-theory/sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/sequential-colimits.lagda.md index 7906598769..04bd41ec62 100644 --- a/src/synthetic-homotopy-theory/sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/sequential-colimits.lagda.md @@ -16,6 +16,7 @@ open import foundation.function-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies +open import foundation.propositions open import foundation.universe-levels open import synthetic-homotopy-theory.cocones-under-sequential-diagrams @@ -160,6 +161,33 @@ module _ map-inv-equiv equiv-dup-standard-sequential-colimit ``` +### The small predicate of being a sequential colimit cocone + +The [proposition](foundation-core.propositions.md) `is-sequential-colimit` is +the assertion that the cogap map is an +[equivalence](foundation-core.equivalences.md). Note that this proposition is +[small](foundation-core.small-types.md), whereas +[the universal property](synthetic-homotopy-theory.universal-property-sequential-colimits.md) +is a large proposition. + +```agda +module _ + {l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2} + (c : cocone-sequential-diagram A X) + where + + is-sequential-colimit : UU (l1 ⊔ l2) + is-sequential-colimit = is-equiv (cogap-standard-sequential-colimit c) + + is-prop-is-sequential-colimit : is-prop is-sequential-colimit + is-prop-is-sequential-colimit = + is-property-is-equiv (cogap-standard-sequential-colimit c) + + is-sequential-colimit-Prop : Prop (l1 ⊔ l2) + pr1 is-sequential-colimit-Prop = is-sequential-colimit + pr2 is-sequential-colimit-Prop = is-prop-is-sequential-colimit +``` + ### Homotopies between maps from the standard sequential colimit Maps from the standard sequential colimit induce cocones under the sequential @@ -211,3 +239,70 @@ module _ htpy-htpy-out-of-standard-sequential-colimit = map-equiv (equiv-htpy-htpy-out-of-standard-sequential-colimit A f g) H ``` + +### A type satisfies `is-sequential-colimit` if and only if it has the (dependent) universal property of sequential colimits + +```agda +module _ + {l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2} + (c : cocone-sequential-diagram A X) + where + + universal-property-is-sequential-colimit : + is-sequential-colimit c → universal-property-sequential-colimit A c + universal-property-is-sequential-colimit = + universal-property-sequential-colimit-is-equiv-universal-property-sequential-colimit + ( A) + ( cocone-standard-sequential-colimit A) + ( c) + ( cogap-standard-sequential-colimit c) + ( htpy-cocone-universal-property-sequential-colimit A + ( cocone-standard-sequential-colimit A) + ( up-standard-sequential-colimit) + ( c)) + ( up-standard-sequential-colimit) + + dependent-universal-property-is-sequential-colimit : + is-sequential-colimit c → + dependent-universal-property-sequential-colimit A c + dependent-universal-property-is-sequential-colimit = + dependent-universal-property-sequential-colimit-is-equiv-dependent-universal-property-sequential-colimit + ( A) + ( cocone-standard-sequential-colimit A) + ( c) + ( cogap-standard-sequential-colimit c) + ( htpy-cocone-universal-property-sequential-colimit A + ( cocone-standard-sequential-colimit A) + ( up-standard-sequential-colimit) + ( c)) + ( dup-standard-sequential-colimit) + + is-sequential-colimit-universal-property : + universal-property-sequential-colimit A c → is-sequential-colimit c + is-sequential-colimit-universal-property = + is-equiv-universal-property-sequential-colimit-universal-property-sequential-colimit + ( A) + ( cocone-standard-sequential-colimit A) + ( c) + ( cogap-standard-sequential-colimit c) + ( htpy-cocone-universal-property-sequential-colimit A + ( cocone-standard-sequential-colimit A) + ( up-standard-sequential-colimit) + ( c)) + ( up-standard-sequential-colimit) + + is-sequential-colimit-dependent-universal-property : + dependent-universal-property-sequential-colimit A c → + is-sequential-colimit c + is-sequential-colimit-dependent-universal-property = + is-equiv-dependent-universal-property-sequential-colimit-dependent-universal-property-sequential-colimit + ( A) + ( cocone-standard-sequential-colimit A) + ( c) + ( cogap-standard-sequential-colimit c) + ( htpy-cocone-universal-property-sequential-colimit A + ( cocone-standard-sequential-colimit A) + ( up-standard-sequential-colimit) + ( c)) + ( dup-standard-sequential-colimit) +``` diff --git a/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md index 911d82d7c3..382dbbc023 100644 --- a/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md @@ -189,7 +189,7 @@ module _ ( up-sequential-colimit Y) ``` -### 3-for-2 property of sequential colimits +### The 3-for-2 property of the universal property of sequential colimits Given two cocones under a sequential diagram, one of which has the universal property of sequential colimits, and a map between their vertices, we prove that @@ -248,11 +248,11 @@ module _ ( up-sequential-colimit Z) ( up-sequential-colimit' Z)) - universal-property-sequential-colimit-is-equiv-universal-property-sequential-colomit : + universal-property-sequential-colimit-is-equiv-universal-property-sequential-colimit : universal-property-sequential-colimit A c → is-equiv h → universal-property-sequential-colimit A c' - universal-property-sequential-colimit-is-equiv-universal-property-sequential-colomit + universal-property-sequential-colimit-is-equiv-universal-property-sequential-colimit ( up-sequential-colimit) ( is-equiv-h) ( Z) =