From c8c9f89f0ec0d52168fcaf77023717c33ada68cb Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Sun, 28 Jan 2024 22:47:05 +0100 Subject: [PATCH] Span diagrams (#1007) This pull request contains the changes from #885 that don't touch `synthetic-homotopy-theory` or `structured-types`, except those changes that are necessary to make the library compile. This PR contains the following changes: - Disambigating between spans and span diagrams. The disambiguation is explained in the relevant files. - Developing infrastructure for spans and span diagrams, with the goal of making it useful for pushouts. - Add extensive informal explanations to all the new files and to relevant existing files. - Change `is-injective-map-equiv` to `is-injective-equiv`, because I needed the fact that `map-equiv` is an injective map somewhere. - Refactors binary type duality and generalises the handling of universes for some of the components of binary type duality. We note specifically by avoiding a proof by equivalence reasoning, it was a lot easier to get the underlying equivalences to do the expected thing. Proofs by equivalence reasoning are more suitable in proofs where the actual equivalence is of less importance, such as `abstract` proofs. - A note on equivalence reasoning was added to `foundation-core.equivalences.lagda.md` to record the previous point on the website. - During the development of #885 I have left a lot of `{{#concept }}` macros with unattributed `Agda` fields. The quickest way to clean that up was just to run through all places where the macro was used and see if there are any unattributed fields. So I did that throughout the library. This includes for files that I would otherwise not have touched, because it didn't make sense to break up my workflow just for them. Thanks for @VojtechStep for the idea of breaking down #885 into smaller pull requests. --- .../cubes-natural-numbers.lagda.md | 2 +- .../multiplication-natural-numbers.lagda.md | 6 +- .../squares-natural-numbers.lagda.md | 4 +- .../delooping-sign-homomorphism.lagda.md | 4 +- .../orbits-permutations.lagda.md | 4 +- ...ermutations-standard-finite-types.lagda.md | 4 +- .../transpositions.lagda.md | 24 +- src/foundation-core.lagda.md | 2 + .../commuting-squares-of-maps.lagda.md | 4 +- src/foundation-core/equivalences.lagda.md | 17 + ...oriality-dependent-function-types.lagda.md | 2 +- src/foundation-core/injective-maps.lagda.md | 4 +- .../operations-span-diagrams.lagda.md | 266 +++++++++++++++ src/foundation-core/operations-spans.lagda.md | 212 ++++++++++++ src/foundation-core/pullbacks.lagda.md | 9 +- .../universal-property-pullbacks.lagda.md | 2 +- src/foundation.lagda.md | 28 +- src/foundation/binary-type-duality.lagda.md | 271 +++++++++++++++ .../cartesian-morphisms-arrows.lagda.md | 2 +- .../commuting-cubes-of-maps.lagda.md | 2 +- ...md => cones-over-cospan-diagrams.lagda.md} | 21 +- .../constant-span-diagrams.lagda.md | 66 ++++ src/foundation/cospan-diagrams.lagda.md | 43 +++ src/foundation/cospans.lagda.md | 105 ++---- .../dependent-function-types.lagda.md | 81 +++++ src/foundation/dependent-homotopies.lagda.md | 3 +- .../descent-coproduct-types.lagda.md | 2 +- .../descent-dependent-pair-types.lagda.md | 2 +- src/foundation/descent-empty-types.lagda.md | 2 +- src/foundation/descent-equivalences.lagda.md | 2 +- .../diagonal-span-diagrams.lagda.md | 38 +++ src/foundation/embeddings.lagda.md | 2 +- .../equality-dependent-pair-types.lagda.md | 5 + src/foundation/equivalences-arrows.lagda.md | 232 +++++++------ src/foundation/equivalences-cospans.lagda.md | 108 ++++++ src/foundation/equivalences-maybe.lagda.md | 8 +- ...s-span-diagrams-families-of-types.lagda.md | 142 ++++++++ .../equivalences-span-diagrams.lagda.md | 321 ++++++++++++++++++ ...ivalences-spans-families-of-types.lagda.md | 158 +++++++++ src/foundation/equivalences-spans.lagda.md | 171 ++++++++++ src/foundation/equivalences.lagda.md | 12 +- src/foundation/fiber-inclusions.lagda.md | 2 +- src/foundation/fibered-maps.lagda.md | 2 +- src/foundation/fibers-of-maps.lagda.md | 2 +- src/foundation/function-types.lagda.md | 56 ++- .../functoriality-coproduct-types.lagda.md | 10 +- ...unctoriality-dependent-pair-types.lagda.md | 4 +- .../functoriality-fibers-of-maps.lagda.md | 2 +- .../functoriality-pullbacks.lagda.md | 11 +- src/foundation/involutions.lagda.md | 2 +- .../kernel-span-diagrams-of-maps.lagda.md | 74 ++++ src/foundation/morphisms-arrows.lagda.md | 100 +++++- .../morphisms-cospan-diagrams.lagda.md | 145 ++++++++ src/foundation/morphisms-cospans.lagda.md | 147 ++------ .../morphisms-span-diagrams.lagda.md | 182 ++++++++++ ...morphisms-spans-families-of-types.lagda.md | 210 ++++++++++++ src/foundation/morphisms-spans.lagda.md | 83 +++++ .../operations-span-diagrams.lagda.md | 168 +++++++++ ...perations-spans-families-of-types.lagda.md | 55 +++ src/foundation/operations-spans.lagda.md | 140 ++++++++ src/foundation/opposite-spans.lagda.md | 57 ++++ src/foundation/partial-functions.lagda.md | 11 +- src/foundation/partial-sequences.lagda.md | 6 +- ...mutations-spans-families-of-types.lagda.md | 46 +++ ...stcomposition-dependent-functions.lagda.md | 3 +- .../precomposition-functions.lagda.md | 20 +- .../precomposition-type-families.lagda.md | 2 +- src/foundation/pullback-squares.lagda.md | 2 +- src/foundation/pullbacks.lagda.md | 6 +- .../span-diagrams-families-of-types.lagda.md | 59 ++++ src/foundation/span-diagrams.lagda.md | 142 ++++++++ .../spans-families-of-types.lagda.md | 62 ++++ src/foundation/spans.lagda.md | 206 +++-------- .../terminal-spans-families-of-types.lagda.md | 45 +++ .../total-partial-elements.lagda.md | 4 +- .../transport-along-equivalences.lagda.md | 260 ++++++++------ .../transposition-span-diagrams.lagda.md | 55 +++ src/foundation/truncated-maps.lagda.md | 2 +- src/foundation/type-duality.lagda.md | 6 + src/foundation/univalence.lagda.md | 10 +- ...-property-cartesian-product-types.lagda.md | 2 +- ...property-dependent-function-types.lagda.md | 125 +++++++ ...property-family-of-fibers-of-maps.lagda.md | 6 +- ...universal-property-fiber-products.lagda.md | 2 +- .../universal-property-pullbacks.lagda.md | 2 +- .../acyclic-undirected-graphs.lagda.md | 5 +- ...tructures-on-standard-finite-sets.lagda.md | 7 +- .../cd-structures.lagda.md | 7 +- ...double-lifts-families-of-elements.lagda.md | 8 +- ...double-lifts-families-of-elements.lagda.md | 4 +- ...nsions-lifts-families-of-elements.lagda.md | 10 +- .../functoriality-pullback-hom.lagda.md | 8 +- .../lifts-families-of-elements.lagda.md | 9 +- .../pullback-hom.lagda.md | 2 +- .../26-descent.lagda.md | 2 +- .../acyclic-maps.lagda.md | 2 +- ...endent-pullback-property-pushouts.lagda.md | 2 +- .../dependent-suspension-structures.lagda.md | 2 +- .../flattening-lemma-coequalizers.lagda.md | 5 +- ...ttening-lemma-sequential-colimits.lagda.md | 4 +- .../pullback-property-pushouts.lagda.md | 6 +- .../retracts-of-sequential-diagrams.lagda.md | 5 +- .../suspension-structures.lagda.md | 2 +- .../truncated-acyclic-maps.lagda.md | 2 +- .../universal-property-pushouts.lagda.md | 2 +- .../2-element-types.lagda.md | 24 +- src/univalent-combinatorics/counting.lagda.md | 2 +- ...tations-complete-undirected-graph.lagda.md | 4 +- .../set-quotients-of-index-two.lagda.md | 16 +- tables/pullbacks.md | 6 +- 110 files changed, 4306 insertions(+), 769 deletions(-) create mode 100644 src/foundation-core/operations-span-diagrams.lagda.md create mode 100644 src/foundation-core/operations-spans.lagda.md create mode 100644 src/foundation/binary-type-duality.lagda.md rename src/foundation/{cones-over-cospans.lagda.md => cones-over-cospan-diagrams.lagda.md} (93%) create mode 100644 src/foundation/constant-span-diagrams.lagda.md create mode 100644 src/foundation/cospan-diagrams.lagda.md create mode 100644 src/foundation/dependent-function-types.lagda.md create mode 100644 src/foundation/diagonal-span-diagrams.lagda.md create mode 100644 src/foundation/equivalences-cospans.lagda.md create mode 100644 src/foundation/equivalences-span-diagrams-families-of-types.lagda.md create mode 100644 src/foundation/equivalences-span-diagrams.lagda.md create mode 100644 src/foundation/equivalences-spans-families-of-types.lagda.md create mode 100644 src/foundation/equivalences-spans.lagda.md create mode 100644 src/foundation/kernel-span-diagrams-of-maps.lagda.md create mode 100644 src/foundation/morphisms-cospan-diagrams.lagda.md create mode 100644 src/foundation/morphisms-span-diagrams.lagda.md create mode 100644 src/foundation/morphisms-spans-families-of-types.lagda.md create mode 100644 src/foundation/morphisms-spans.lagda.md create mode 100644 src/foundation/operations-span-diagrams.lagda.md create mode 100644 src/foundation/operations-spans-families-of-types.lagda.md create mode 100644 src/foundation/operations-spans.lagda.md create mode 100644 src/foundation/opposite-spans.lagda.md create mode 100644 src/foundation/permutations-spans-families-of-types.lagda.md create mode 100644 src/foundation/span-diagrams-families-of-types.lagda.md create mode 100644 src/foundation/span-diagrams.lagda.md create mode 100644 src/foundation/spans-families-of-types.lagda.md create mode 100644 src/foundation/terminal-spans-families-of-types.lagda.md create mode 100644 src/foundation/transposition-span-diagrams.lagda.md create mode 100644 src/foundation/universal-property-dependent-function-types.lagda.md diff --git a/src/elementary-number-theory/cubes-natural-numbers.lagda.md b/src/elementary-number-theory/cubes-natural-numbers.lagda.md index b6fa0e8efc..491369a597 100644 --- a/src/elementary-number-theory/cubes-natural-numbers.lagda.md +++ b/src/elementary-number-theory/cubes-natural-numbers.lagda.md @@ -20,7 +20,7 @@ open import foundation.universe-levels ## Idea -The {{#concept "cube" Disambiguation="natural number"}} `n³` of a +The {{#concept "cube" Disambiguation="natural number" Agda=cube-ℕ}} `n³` of a [natural number](elementary-number-theory.natural-numbers.md) `n` is the triple [product](elementary-number-theory.multiplication-natural-numbers.md) diff --git a/src/elementary-number-theory/multiplication-natural-numbers.lagda.md b/src/elementary-number-theory/multiplication-natural-numbers.lagda.md index bebd14dcb6..43f53a469c 100644 --- a/src/elementary-number-theory/multiplication-natural-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-natural-numbers.lagda.md @@ -25,9 +25,9 @@ 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 +The {{#concept "multiplication" Disambiguation="natural numbers" Agda=mul-ℕ}} +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: diff --git a/src/elementary-number-theory/squares-natural-numbers.lagda.md b/src/elementary-number-theory/squares-natural-numbers.lagda.md index e8490a8459..ce63c24575 100644 --- a/src/elementary-number-theory/squares-natural-numbers.lagda.md +++ b/src/elementary-number-theory/squares-natural-numbers.lagda.md @@ -30,8 +30,8 @@ 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 +The {{#concept "square" Disambiguation="natural number" Agda=square-ℕ}} `n²` of +a [natural number](elementary-number-theory.natural-numbers.md) `n` is the [product](elementary-number-theory.multiplication-natural-numbers.md) ```text diff --git a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md index 10c406c19e..ad20f2ba3d 100644 --- a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md +++ b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md @@ -614,7 +614,7 @@ module _ ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2)))) ( this-third-thing n p) ( map-quotient-loop-Fin n p (this-third-thing n p))) - ( is-injective-map-equiv (inv-equiv (that-thing n)) (q ∙ inv r)))) + ( is-injective-equiv (inv-equiv (that-thing n)) (q ∙ inv r)))) cases-eq-map-quotient-aut-Fin n p (inr ND) (inl (inr star)) (inr star) q r = ( ap ( map-equiv (that-thing n)) @@ -650,7 +650,7 @@ module _ ( R (n +ℕ 2) (raise-UU-Fin-Fin (n +ℕ 2)))) ( this-third-thing n p) ( map-quotient-loop-Fin n p (this-third-thing n p))) - ( is-injective-map-equiv (inv-equiv (that-thing n)) (q ∙ inv r)))) + ( is-injective-equiv (inv-equiv (that-thing n)) (q ∙ inv r)))) eq-map-quotient-aut-Fin : (n : ℕ) (p : type-Group (loop-group-Set (raise-Fin-Set l1 (n +ℕ 2)))) → diff --git a/src/finite-group-theory/orbits-permutations.lagda.md b/src/finite-group-theory/orbits-permutations.lagda.md index 2bfbdbd8cd..5aefefe130 100644 --- a/src/finite-group-theory/orbits-permutations.lagda.md +++ b/src/finite-group-theory/orbits-permutations.lagda.md @@ -281,7 +281,7 @@ module _ ( λ x → le-ℕ x first-point-min-repeating) ( equality-pred-second) ( le-min-reporting))) - ( is-injective-map-equiv + ( is-injective-equiv ( f) ( tr ( λ x → @@ -1900,7 +1900,7 @@ module _ ( inl k) section-h'-inl k (inl Q) R (inl Q') R' = ap inl - ( is-injective-map-equiv (equiv-count h) + ( is-injective-equiv (equiv-count h) ( ap ( λ f → map-equiv f (class (same-orbits-permutation-count g) a)) ( right-inverse-law-equiv (equiv-count h)) ∙ diff --git a/src/finite-group-theory/permutations-standard-finite-types.lagda.md b/src/finite-group-theory/permutations-standard-finite-types.lagda.md index b911b44a70..fe19ae1757 100644 --- a/src/finite-group-theory/permutations-standard-finite-types.lagda.md +++ b/src/finite-group-theory/permutations-standard-finite-types.lagda.md @@ -213,7 +213,7 @@ abstract ( neq-inr-inl) ( λ r → neq-inr-inl - ( is-injective-map-equiv f (p ∙ (r ∙ inv q)))) + ( is-injective-equiv f (p ∙ (r ∙ inv q)))) lemma : Id ( map-equiv @@ -404,7 +404,7 @@ abstract (succ-ℕ n) f (inr star) p (inl y) (inr star) q = ex-falso ( neq-inr-inl - ( is-injective-map-equiv f (p ∙ inv q))) + ( is-injective-equiv f (p ∙ inv q))) retraction-permutation-list-transpositions-Fin' (succ-ℕ n) f (inr star) p (inr star) z q = ap diff --git a/src/finite-group-theory/transpositions.lagda.md b/src/finite-group-theory/transpositions.lagda.md index 05cb5d0f7f..18e1b63420 100644 --- a/src/finite-group-theory/transpositions.lagda.md +++ b/src/finite-group-theory/transpositions.lagda.md @@ -403,29 +403,29 @@ module _ ( Id (pr1 two-elements-transposition) x) + ( Id (pr1 (pr2 two-elements-transposition)) x) cases-coprod-id-type-t x p h (inl (inr star)) (inl (inr star)) k3 K1 K2 K3 = - inl (ap pr1 (is-injective-map-equiv (inv-equiv h) (K2 ∙ inv K1))) + inl (ap pr1 (is-injective-equiv (inv-equiv h) (K2 ∙ inv K1))) cases-coprod-id-type-t x p h (inl (inr star)) (inr star) (inl (inr star)) K1 K2 K3 = - inr (ap pr1 (is-injective-map-equiv (inv-equiv h) (K3 ∙ inv K1))) + inr (ap pr1 (is-injective-equiv (inv-equiv h) (K3 ∙ inv K1))) cases-coprod-id-type-t x p h (inl (inr star)) (inr star) (inr star) K1 K2 K3 = ex-falso ( pr2 element-is-not-identity-map-transposition ( inv ( ap pr1 - ( is-injective-map-equiv (inv-equiv h) (K2 ∙ inv K3))))) + ( is-injective-equiv (inv-equiv h) (K2 ∙ inv K3))))) cases-coprod-id-type-t x p h (inr star) (inl (inr star)) (inl (inr star)) K1 K2 K3 = ex-falso ( pr2 element-is-not-identity-map-transposition ( inv ( ap pr1 - ( is-injective-map-equiv (inv-equiv h) (K2 ∙ inv K3))))) + ( is-injective-equiv (inv-equiv h) (K2 ∙ inv K3))))) cases-coprod-id-type-t x p h (inr star) (inl (inr star)) (inr star) K1 K2 K3 = - inr (ap pr1 (is-injective-map-equiv (inv-equiv h) (K3 ∙ inv K1))) + inr (ap pr1 (is-injective-equiv (inv-equiv h) (K3 ∙ inv K1))) cases-coprod-id-type-t x p h (inr star) (inr star) k3 K1 K2 K3 = - inl (ap pr1 (is-injective-map-equiv (inv-equiv h) (K2 ∙ inv K1))) + inl (ap pr1 (is-injective-equiv (inv-equiv h) (K2 ∙ inv K1))) coprod-id-type-t : (x : X) → type-Decidable-Prop (pr1 Y x) → ( Id (pr1 two-elements-transposition) x) + @@ -673,7 +673,7 @@ module _ pr1 (pr2 (pr1 (transposition-conjugation-equiv (pair P H)) x)) = is-prop-all-elements-equal (λ p1 p2 → - is-injective-map-equiv + is-injective-equiv ( inv-equiv ( compute-raise l4 (type-Decidable-Prop (P (map-inv-equiv e x))))) ( eq-is-prop (is-prop-type-Decidable-Prop (P (map-inv-equiv e x))))) @@ -781,7 +781,7 @@ module _ ( pair (Σ X (λ y → type-Decidable-Prop (pr1 t y))) (pr2 t)) { pair (map-inv-equiv e x) p} ( eq-pair-Σ - ( is-injective-map-equiv + ( is-injective-equiv ( e) ( inv (pr1 (pair-eq-Σ q)) ∙ ap @@ -1013,13 +1013,13 @@ eq-transposition-precomp-standard-2-Element-Decidable-Subtype pr1 (pr1 (standard-2-Element-Decidable-Subtype H np) z) f z (inl p) = inr - ( is-injective-map-equiv + ( is-injective-equiv ( standard-transposition H np) ( ( right-computation-standard-transposition H np) ∙ ( p))) f z (inr p) = inl - ( is-injective-map-equiv + ( is-injective-equiv ( standard-transposition H np) ( ( left-computation-standard-transposition H np) ∙ ( p))) @@ -1087,13 +1087,13 @@ eq-transposition-precomp-ineq-standard-2-Element-Decidable-Subtype pr1 (pr1 (standard-2-Element-Decidable-Subtype H np') u) f u (inl p) = inl - ( is-injective-map-equiv + ( is-injective-equiv ( standard-transposition H np) ( ( is-fixed-point-standard-transposition H np z nq1 nq3) ∙ ( p))) f u (inr p) = inr - ( is-injective-map-equiv + ( is-injective-equiv ( standard-transposition H np) ( ( is-fixed-point-standard-transposition H np w nq2 nq4) ∙ ( p))) diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md index 07e843af66..803e7912e1 100644 --- a/src/foundation-core.lagda.md +++ b/src/foundation-core.lagda.md @@ -36,6 +36,8 @@ open import foundation-core.identity-types public open import foundation-core.injective-maps public open import foundation-core.invertible-maps public open import foundation-core.negation public +open import foundation-core.operations-span-diagrams public +open import foundation-core.operations-spans public open import foundation-core.path-split-maps public open import foundation-core.postcomposition-functions public open import foundation-core.precomposition-dependent-functions public diff --git a/src/foundation-core/commuting-squares-of-maps.lagda.md b/src/foundation-core/commuting-squares-of-maps.lagda.md index 6dbe068045..e6834c6c95 100644 --- a/src/foundation-core/commuting-squares-of-maps.lagda.md +++ b/src/foundation-core/commuting-squares-of-maps.lagda.md @@ -219,6 +219,6 @@ module _ Several structures make essential use of commuting squares of maps: -- [Cones over cospans](foundation.cones-over-cospans.md) -- [Cocones under spans](synthetic-homotopy-theory.cocones-under-spans.md) +- [Cones over cospan diagrams](foundation.cones-over-cospan-diagrams.md) +- [Cocones under span diagrams](synthetic-homotopy-theory.cocones-under-spans.md) - [Morphisms of arrows](foundation.morphisms-arrows.md) diff --git a/src/foundation-core/equivalences.lagda.md b/src/foundation-core/equivalences.lagda.md index 43c1596431..4fdf05534e 100644 --- a/src/foundation-core/equivalences.lagda.md +++ b/src/foundation-core/equivalences.lagda.md @@ -714,6 +714,23 @@ equivalence-reasoning The equivalence constructed in this way is `equiv-1 ∘e (equiv-2 ∘e equiv-3)`, i.e., the equivivalence is associated fully to the right. +**Note.** In situations where it is important to have precise control over an +equivalence or its inverse, it is often better to avoid making use of +equivalence reasoning. For example, since many of the entries proving that a map +is an equivalence are marked as `abstract` in agda-unimath, the inverse of an +equivalence often does not compute to any map that one might expect the inverse +to be. If inverses of equivalences are used in equivalence reasoning, this +results in a composed equivalence that also does not compute to any expected +underlying map. + +Even if a proof by equivalence reasoning is clear to the human reader, +constructing equivalences by hand by constructing maps back and forth and two +homotopies witnessing that they are mutual inverses is often the most +straigtforward solution that gives the best expected computational behavior of +the constructed equivalence. In particular, if the underlying map or its inverse +are noteworthy maps, it is good practice to define them directly rather than as +underlying maps of equivalences constructed by equivalence reasoning. + ```agda infixl 1 equivalence-reasoning_ infixl 0 step-equivalence-reasoning diff --git a/src/foundation-core/functoriality-dependent-function-types.lagda.md b/src/foundation-core/functoriality-dependent-function-types.lagda.md index ca9dae1874..796a15da02 100644 --- a/src/foundation-core/functoriality-dependent-function-types.lagda.md +++ b/src/foundation-core/functoriality-dependent-function-types.lagda.md @@ -121,7 +121,7 @@ module _ ( map-inv-equiv (equiv-Π-equiv-family e)) ~ ( map-equiv (equiv-Π-equiv-family (λ x → inv-equiv (e x)))) compute-inv-equiv-Π-equiv-family e f = - is-injective-map-equiv + is-injective-equiv ( equiv-Π-equiv-family e) ( ( is-section-map-inv-equiv (equiv-Π-equiv-family e) f) ∙ ( eq-htpy (λ x → inv (is-section-map-inv-equiv (e x) (f x))))) diff --git a/src/foundation-core/injective-maps.lagda.md b/src/foundation-core/injective-maps.lagda.md index c3114d9239..1d9989847d 100644 --- a/src/foundation-core/injective-maps.lagda.md +++ b/src/foundation-core/injective-maps.lagda.md @@ -114,8 +114,8 @@ module _ ( is-retraction-map-inv-is-equiv H y)) abstract - is-injective-map-equiv : (e : A ≃ B) → is-injective (map-equiv e) - is-injective-map-equiv (pair f H) = is-injective-is-equiv H + is-injective-equiv : (e : A ≃ B) → is-injective (map-equiv e) + is-injective-equiv (pair f H) = is-injective-is-equiv H module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} diff --git a/src/foundation-core/operations-span-diagrams.lagda.md b/src/foundation-core/operations-span-diagrams.lagda.md new file mode 100644 index 0000000000..d80e62f1a5 --- /dev/null +++ b/src/foundation-core/operations-span-diagrams.lagda.md @@ -0,0 +1,266 @@ +# Operations on span diagrams + +```agda +module foundation-core.operations-span-diagrams where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.morphisms-arrows +open import foundation.operations-spans +open import foundation.span-diagrams +open import foundation.spans +open import foundation.universe-levels + +open import foundation-core.function-types +``` + +
+ +## Idea + +This file contains some operations on +[span diagrams](foundation.span-diagrams.md) that produce new span diagrams from +given span diagrams and possibly other data. + +## Definitions + +### Concatenating span diagrams and maps on both sides + +Consider a [span diagram](foundation.span-diagrams.md) `𝒮` given by + +```text + f g + A <----- S -----> B +``` + +and maps `i : A → A'` and `j : B → B'`. The +{{#concept "concatenation-span-diagram" Disambiguation="span diagram" Agda=concat-span-diagram}} +of `𝒮`, `i`, and `j` is the span diagram + +```text + i ∘ f j ∘ g + A' <------- S -------> B'. +``` + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + where + + concat-span-diagram : + (𝒮 : span-diagram l1 l2 l3) + {A' : UU l4} (f : domain-span-diagram 𝒮 → A') + {B' : UU l5} (g : codomain-span-diagram 𝒮 → B') → + span-diagram l4 l5 l3 + pr1 (concat-span-diagram 𝒮 {A'} f {B'} g) = + A' + pr1 (pr2 (concat-span-diagram 𝒮 {A'} f {B'} g)) = + B' + pr2 (pr2 (concat-span-diagram 𝒮 {A'} f {B'} g)) = + concat-span (span-span-diagram 𝒮) f g +``` + +### Concatenating span diagrams and maps on the left + +Consider a [span diagram](foundation.span-diagrams.md) `𝒮` given by + +```text + f g + A <----- S -----> B +``` + +and a map `i : A → A'`. The +{{#concept "left concatenation" Disambiguation="span diagram" Agda=left-concat-span-diagram}} +of `𝒮` and `i` is the span diagram + +```text + i ∘ f g + A' <------- S -----> B. +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} + where + + left-concat-span-diagram : + (𝒮 : span-diagram l1 l2 l3) {A' : UU l4} → + (domain-span-diagram 𝒮 → A') → span-diagram l4 l2 l3 + left-concat-span-diagram 𝒮 f = concat-span-diagram 𝒮 f id +``` + +### Concatenating span diagrams and maps on the right + +Consider a [span diagram](foundation.span-diagrams.md) `𝒮` given by + +```text + f g + A <----- S -----> B +``` + +and a map `j : B → B'`. The +{{#concept "right concatenation" Disambiguation="span diagram" Agda=right-concat-span-diagram}} +of `𝒮` by `j` is the span diagram + +```text + f j ∘ g + A' <----- S -------> B'. +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} + where + + right-concat-span-diagram : + (𝒮 : span-diagram l1 l2 l3) {B' : UU l4} → + (codomain-span-diagram 𝒮 → B') → span-diagram l1 l4 l3 + right-concat-span-diagram 𝒮 g = concat-span-diagram 𝒮 id g +``` + +### Concatenation of span diagrams and morphisms of arrows on the left + +Consider a span diagram `𝒮` given by + +```text + f g + A <----- S -----> B +``` + +and a [morphism of arrows](foundation.morphisms-arrows.md) `h : hom-arrow f' f` +as indicated in the diagram + +```text + f' + A' <---- S' + | | + h₀ | | h₁ + V V + A <----- S -----> B. + f g +``` + +Then we obtain a span diagram `A' <- S' -> B`. + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} (𝒮 : span-diagram l1 l2 l3) + {S' : UU l4} {A' : UU l5} (f' : S' → A') + (h : hom-arrow f' (left-map-span-diagram 𝒮)) + where + + domain-left-concat-hom-arrow-span-diagram : UU l5 + domain-left-concat-hom-arrow-span-diagram = A' + + codomain-left-concat-hom-arrow-span-diagram : UU l2 + codomain-left-concat-hom-arrow-span-diagram = codomain-span-diagram 𝒮 + + span-left-concat-hom-arrow-span-diagram : + span l4 + ( domain-left-concat-hom-arrow-span-diagram) + ( codomain-left-concat-hom-arrow-span-diagram) + span-left-concat-hom-arrow-span-diagram = + left-concat-hom-arrow-span + ( span-span-diagram 𝒮) + ( f') + ( h) + + left-concat-hom-arrow-span-diagram : span-diagram l5 l2 l4 + pr1 left-concat-hom-arrow-span-diagram = + domain-left-concat-hom-arrow-span-diagram + pr1 (pr2 left-concat-hom-arrow-span-diagram) = + codomain-left-concat-hom-arrow-span-diagram + pr2 (pr2 left-concat-hom-arrow-span-diagram) = + span-left-concat-hom-arrow-span-diagram + + spanning-type-left-concat-hom-arrow-span-diagram : UU l4 + spanning-type-left-concat-hom-arrow-span-diagram = + spanning-type-span-diagram left-concat-hom-arrow-span-diagram + + left-map-left-concat-hom-arrow-span-diagram : + spanning-type-left-concat-hom-arrow-span-diagram → + domain-left-concat-hom-arrow-span-diagram + left-map-left-concat-hom-arrow-span-diagram = + left-map-span-diagram left-concat-hom-arrow-span-diagram + + right-map-left-concat-hom-arrow-span-diagram : + spanning-type-left-concat-hom-arrow-span-diagram → + codomain-left-concat-hom-arrow-span-diagram + right-map-left-concat-hom-arrow-span-diagram = + right-map-span-diagram left-concat-hom-arrow-span-diagram +``` + +### Concatenation of span diagrams and morphisms of arrows on the right + +Consider a span diagram `𝒮` given by + +```text + f g + A <----- S -----> B +``` + +and a [morphism of arrows](foundation.morphisms-arrows.md) `h : hom-arrow g' g` +as indicated in the diagram + +```text + g' + S' ----> B' + | | + h₀ | | h₁ + V V + A <----- S -----> B. + f g +``` + +Then we obtain a span diagram `A <- S' -> B'`. + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} (𝒮 : span-diagram l1 l2 l3) + {S' : UU l4} {B' : UU l5} (g' : S' → B') + (h : hom-arrow g' (right-map-span-diagram 𝒮)) + where + + domain-right-concat-hom-arrow-span-diagram : UU l1 + domain-right-concat-hom-arrow-span-diagram = domain-span-diagram 𝒮 + + codomain-right-concat-hom-arrow-span-diagram : UU l5 + codomain-right-concat-hom-arrow-span-diagram = B' + + span-right-concat-hom-arrow-span-diagram : + span l4 + ( domain-right-concat-hom-arrow-span-diagram) + ( codomain-right-concat-hom-arrow-span-diagram) + span-right-concat-hom-arrow-span-diagram = + right-concat-hom-arrow-span + ( span-span-diagram 𝒮) + ( g') + ( h) + + right-concat-hom-arrow-span-diagram : span-diagram l1 l5 l4 + pr1 right-concat-hom-arrow-span-diagram = + domain-right-concat-hom-arrow-span-diagram + pr1 (pr2 right-concat-hom-arrow-span-diagram) = + codomain-right-concat-hom-arrow-span-diagram + pr2 (pr2 right-concat-hom-arrow-span-diagram) = + span-right-concat-hom-arrow-span-diagram + + spanning-type-right-concat-hom-arrow-span-diagram : UU l4 + spanning-type-right-concat-hom-arrow-span-diagram = + spanning-type-span-diagram right-concat-hom-arrow-span-diagram + + left-map-right-concat-hom-arrow-span-diagram : + spanning-type-right-concat-hom-arrow-span-diagram → + domain-right-concat-hom-arrow-span-diagram + left-map-right-concat-hom-arrow-span-diagram = + left-map-span-diagram right-concat-hom-arrow-span-diagram + + right-map-right-concat-hom-arrow-span-diagram : + spanning-type-right-concat-hom-arrow-span-diagram → + codomain-right-concat-hom-arrow-span-diagram + right-map-right-concat-hom-arrow-span-diagram = + right-map-span-diagram right-concat-hom-arrow-span-diagram +``` diff --git a/src/foundation-core/operations-spans.lagda.md b/src/foundation-core/operations-spans.lagda.md new file mode 100644 index 0000000000..33d70af2cf --- /dev/null +++ b/src/foundation-core/operations-spans.lagda.md @@ -0,0 +1,212 @@ +# Operations on spans + +```agda +module foundation-core.operations-spans where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.morphisms-arrows +open import foundation.spans +open import foundation.universe-levels + +open import foundation-core.function-types +``` + +
+ +## Idea + +This file contains some operations on [spans](foundation.spans.md) that produce +new spans from given spans and possibly other data. + +## Definitions + +### Concatenating spans and maps on both sides + +Consider a [span](foundation.spans.md) `s` given by + +```text + f g + A <----- S -----> B +``` + +and maps `i : A → A'` and `j : B → B'`. The +{{#concept "concatenation span" Disambiguation="span" Agda=concat-span}} of `i`, +`s`, and `j` is the span + +```text + i ∘ f j ∘ g + A' <------- S -------> B. +``` + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {A : UU l1} {A' : UU l2} + {B : UU l3} {B' : UU l4} + where + + concat-span : span l5 A B → (A → A') → (B → B') → span l5 A' B' + pr1 (concat-span s i j) = spanning-type-span s + pr1 (pr2 (concat-span s i j)) = i ∘ left-map-span s + pr2 (pr2 (concat-span s i j)) = j ∘ right-map-span s +``` + +### Concatenating spans and maps on the left + +Consider a [span](foundation.spans.md) `s` given by + +```text + f g + A <----- S -----> B +``` + +and a map `i : A → A'`. The +{{#concept "left concatenation" Disambiguation="span" Agda=left-concat-span}} of +`s` by `i` is the span + +```text + i ∘ f g + A' <------- S -----> B. +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {A' : UU l2} + {B : UU l3} + where + + left-concat-span : span l4 A B → (A → A') → span l4 A' B + left-concat-span s f = concat-span s f id +``` + +### Concatenating spans and maps on the right + +Consider a [span](foundation.spans.md) `s` given by + +```text + f g + A <----- S -----> B +``` + +and a map `j : B → B'`. The +{{#concept "right concatenation" Disambiguation="span" Agda=right-concat-span}} +of `s` by `j` is the span + +```text + f j ∘ g + A' <----- S -------> B. +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} + {B : UU l3} {B' : UU l4} + where + + right-concat-span : span l4 A B → (B → B') → span l4 A B' + right-concat-span s g = concat-span s id g +``` + +### Concatenating spans and morphisms of arrows on the left + +Consider a span `s` given by + +```text + f g + A <----- S -----> B +``` + +and a [morphism of arrows](foundation.morphisms-arrows.md) `h : hom-arrow f' f` +as indicated in the diagram + +```text + f' + A' <---- S' + | | + h₀ | | h₁ + V V + A <----- S -----> B. + f g +``` + +Then we obtain a span `A' <- S' -> B`. + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} (s : span l3 A B) + {S' : UU l4} {A' : UU l5} (f' : S' → A') (h : hom-arrow f' (left-map-span s)) + where + + spanning-type-left-concat-hom-arrow-span : UU l4 + spanning-type-left-concat-hom-arrow-span = S' + + left-map-left-concat-hom-arrow-span : + spanning-type-left-concat-hom-arrow-span → A' + left-map-left-concat-hom-arrow-span = f' + + right-map-left-concat-hom-arrow-span : + spanning-type-left-concat-hom-arrow-span → B + right-map-left-concat-hom-arrow-span = + right-map-span s ∘ map-domain-hom-arrow f' (left-map-span s) h + + left-concat-hom-arrow-span : span l4 A' B + pr1 left-concat-hom-arrow-span = spanning-type-left-concat-hom-arrow-span + pr1 (pr2 left-concat-hom-arrow-span) = left-map-left-concat-hom-arrow-span + pr2 (pr2 left-concat-hom-arrow-span) = right-map-left-concat-hom-arrow-span +``` + +### Concatenating spans and morphisms of arrows on the right + +Consider a span `s` given by + +```text + f g + A <----- S -----> B +``` + +and a [morphism of arrows](foundation.morphisms-arrows.md) `h : hom-arrow g' g` +as indicated in the diagram + +```text + g' + S' ----> B' + | | + h₀ | | h₁ + V V + A <----- S -----> B. + f g +``` + +Then we obtain a span `A <- S' -> B'`. + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} + (s : span l3 A B) + {S' : UU l4} {B' : UU l5} (g' : S' → B') + (h : hom-arrow g' (right-map-span s)) + where + + spanning-type-right-concat-hom-arrow-span : UU l4 + spanning-type-right-concat-hom-arrow-span = S' + + left-map-right-concat-hom-arrow-span : + spanning-type-right-concat-hom-arrow-span → A + left-map-right-concat-hom-arrow-span = + left-map-span s ∘ map-domain-hom-arrow g' (right-map-span s) h + + right-map-right-concat-hom-arrow-span : + spanning-type-right-concat-hom-arrow-span → B' + right-map-right-concat-hom-arrow-span = g' + + right-concat-hom-arrow-span : span l4 A B' + pr1 right-concat-hom-arrow-span = spanning-type-right-concat-hom-arrow-span + pr1 (pr2 right-concat-hom-arrow-span) = left-map-right-concat-hom-arrow-span + pr2 (pr2 right-concat-hom-arrow-span) = right-map-right-concat-hom-arrow-span +``` diff --git a/src/foundation-core/pullbacks.lagda.md b/src/foundation-core/pullbacks.lagda.md index a776424bfe..8477c73acb 100644 --- a/src/foundation-core/pullbacks.lagda.md +++ b/src/foundation-core/pullbacks.lagda.md @@ -8,7 +8,7 @@ module foundation-core.pullbacks where ```agda open import foundation.action-on-identifications-functions -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types open import foundation.functoriality-cartesian-product-types @@ -67,8 +67,8 @@ The standard pullback consists of [pairs](foundation.dependent-pair-types.md) A ×_X B := Σ (a : A) (b : B), (f a = g b). ``` -Thus the standard [cone](foundation.cones-over-cospans.md) consists of the -canonical projections. +Thus the standard [cone](foundation.cones-over-cospan-diagrams.md) consists of +the canonical projections. ## Definitions @@ -192,7 +192,8 @@ module _ { s t : standard-pullback f g} ( α : vertical-map-standard-pullback s = vertical-map-standard-pullback t) ( β : - horizontal-map-standard-pullback s = horizontal-map-standard-pullback t) → + horizontal-map-standard-pullback s = + horizontal-map-standard-pullback t) → ( ( ap f α ∙ coherence-square-standard-pullback t) = ( coherence-square-standard-pullback s ∙ ap g β)) → s = t diff --git a/src/foundation-core/universal-property-pullbacks.lagda.md b/src/foundation-core/universal-property-pullbacks.lagda.md index b1b3c95921..33f8cc5a4c 100644 --- a/src/foundation-core/universal-property-pullbacks.lagda.md +++ b/src/foundation-core/universal-property-pullbacks.lagda.md @@ -8,7 +8,7 @@ module foundation-core.universal-property-pullbacks where ```agda open import foundation.action-on-identifications-functions -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.postcomposition-functions open import foundation.universe-levels diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 1509e9ca13..1adc44d8a8 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -33,6 +33,7 @@ open import foundation.binary-operations-unordered-pairs-of-types public open import foundation.binary-reflecting-maps-equivalence-relations public open import foundation.binary-relations public open import foundation.binary-transport public +open import foundation.binary-type-duality public open import foundation.booleans public open import foundation.cantor-schroder-bernstein-escardo public open import foundation.cantors-diagonal-argument public @@ -60,7 +61,7 @@ open import foundation.complements public open import foundation.complements-subtypes public open import foundation.composite-maps-in-inverse-sequential-diagrams public open import foundation.composition-algebra public -open import foundation.cones-over-cospans public +open import foundation.cones-over-cospan-diagrams public open import foundation.cones-over-inverse-sequential-diagrams public open import foundation.conjunction public open import foundation.connected-components public @@ -68,6 +69,7 @@ open import foundation.connected-components-universes public open import foundation.connected-maps public 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.contractible-maps public open import foundation.contractible-types public @@ -77,6 +79,7 @@ open import foundation.coproduct-decompositions public open import foundation.coproduct-decompositions-subuniverse public open import foundation.coproduct-types public open import foundation.coslice public +open import foundation.cospan-diagrams public open import foundation.cospans public open import foundation.decidable-dependent-function-types public open import foundation.decidable-dependent-pair-types public @@ -92,6 +95,7 @@ open import foundation.dependent-binary-homotopies public open import foundation.dependent-binomial-theorem public open import foundation.dependent-epimorphisms public open import foundation.dependent-epimorphisms-with-respect-to-truncated-types public +open import foundation.dependent-function-types public open import foundation.dependent-homotopies public open import foundation.dependent-identifications public open import foundation.dependent-inverse-sequential-diagrams public @@ -104,6 +108,7 @@ open import foundation.descent-dependent-pair-types public open import foundation.descent-empty-types public open import foundation.descent-equivalences public open import foundation.diagonal-maps-of-types public +open import foundation.diagonal-span-diagrams public open import foundation.diagonals-of-maps public open import foundation.diagonals-of-morphisms-arrows public open import foundation.discrete-reflexive-relations public @@ -134,8 +139,13 @@ open import foundation.equivalence-injective-type-families public open import foundation.equivalence-relations public open import foundation.equivalences public open import foundation.equivalences-arrows public +open import foundation.equivalences-cospans public open import foundation.equivalences-inverse-sequential-diagrams public open import foundation.equivalences-maybe public +open import foundation.equivalences-span-diagrams public +open import foundation.equivalences-span-diagrams-families-of-types public +open import foundation.equivalences-spans public +open import foundation.equivalences-spans-families-of-types public open import foundation.exclusive-disjunction public open import foundation.existential-quantification public open import foundation.exponents-set-quotients public @@ -195,6 +205,7 @@ open import foundation.iterated-dependent-product-types public open import foundation.iterating-automorphisms public open import foundation.iterating-functions public open import foundation.iterating-involutions public +open import foundation.kernel-span-diagrams-of-maps public open import foundation.large-binary-relations public open import foundation.large-dependent-pair-types public open import foundation.large-homotopies public @@ -215,8 +226,12 @@ open import foundation.mere-equivalences public open import foundation.monomorphisms public open import foundation.morphisms-arrows public open import foundation.morphisms-binary-relations public +open import foundation.morphisms-cospan-diagrams public open import foundation.morphisms-cospans public open import foundation.morphisms-inverse-sequential-diagrams public +open import foundation.morphisms-span-diagrams public +open import foundation.morphisms-spans public +open import foundation.morphisms-spans-families-of-types public open import foundation.morphisms-twisted-arrows public open import foundation.multisubsets public open import foundation.multivariable-correspondences public @@ -229,6 +244,10 @@ open import foundation.multivariable-sections public open import foundation.negated-equality public open import foundation.negation public open import foundation.noncontractible-types public +open import foundation.operations-span-diagrams public +open import foundation.operations-spans public +open import foundation.operations-spans-families-of-types public +open import foundation.opposite-spans public open import foundation.pairs-of-distinct-elements public open import foundation.partial-elements public open import foundation.partial-functions public @@ -237,6 +256,7 @@ open import foundation.partitions public open import foundation.path-algebra public open import foundation.path-split-maps public open import foundation.perfect-images public +open import foundation.permutations-spans-families-of-types public open import foundation.pi-decompositions public open import foundation.pi-decompositions-subuniverse public open import foundation.pointed-torsorial-type-families public @@ -299,7 +319,10 @@ open import foundation.small-maps public open import foundation.small-types public open import foundation.small-universes public open import foundation.sorial-type-families public +open import foundation.span-diagrams public +open import foundation.span-diagrams-families-of-types public open import foundation.spans public +open import foundation.spans-families-of-types public open import foundation.split-surjective-maps public open import foundation.standard-apartness-relations public open import foundation.strongly-extensional-maps public @@ -319,6 +342,7 @@ open import foundation.symmetric-difference public open import foundation.symmetric-identity-types public open import foundation.symmetric-operations public open import foundation.telescopes public +open import foundation.terminal-spans-families-of-types public open import foundation.tight-apartness-relations public open import foundation.torsorial-type-families public open import foundation.total-partial-elements public @@ -328,6 +352,7 @@ open import foundation.transport-along-equivalences public open import foundation.transport-along-higher-identifications public open import foundation.transport-along-homotopies public open import foundation.transport-along-identifications public +open import foundation.transposition-span-diagrams public open import foundation.trivial-relaxed-sigma-decompositions public open import foundation.trivial-sigma-decompositions public open import foundation.truncated-equality public @@ -363,6 +388,7 @@ open import foundation.universal-property-booleans public open import foundation.universal-property-cartesian-product-types public open import foundation.universal-property-contractible-types public open import foundation.universal-property-coproduct-types public +open import foundation.universal-property-dependent-function-types public open import foundation.universal-property-dependent-pair-types public open import foundation.universal-property-empty-type public open import foundation.universal-property-equivalences public diff --git a/src/foundation/binary-type-duality.lagda.md b/src/foundation/binary-type-duality.lagda.md new file mode 100644 index 0000000000..20a23bc58d --- /dev/null +++ b/src/foundation/binary-type-duality.lagda.md @@ -0,0 +1,271 @@ +# Binary type duality + +```agda +module foundation.binary-type-duality where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.equivalences-spans +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.multivariable-homotopies +open import foundation.retractions +open import foundation.sections +open import foundation.spans +open import foundation.univalence +open import foundation.universe-levels + +open import foundation-core.cartesian-product-types +open import foundation-core.homotopies +open import foundation-core.identity-types +``` + +
+ +## Idea + +The principle of {{#concept "binary type duality" Agda=binary-type-duality}} +asserts that the type of [binary relations](foundation.binary-relations.md) +`A → B → 𝒰` is [equivalent](foundation-core.equivalences.md) to the type of +[binary spans](foundation.spans.md) from `A` to `B`. The binary type duality +principle is a binary version of the [type duality](foundation.type-duality.md) +principle, which asserts that type families over a type `A` are equivalently +described as maps into `A`, and makes essential use of the +[univalence axiom](foundation.univalence.md). + +The equivalence of binary type duality takes a binary relation `R : A → B → 𝒰` +to the span + +```text + A <----- Σ (a : A), Σ (b : B), R a b -----> B. +``` + +and its inverse takes a span `A <-f- S -g-> B` to the binary relation + +```text + a b ↦ Σ (s : S), (f s = a) × (g s = b). +``` + +## Definitions + +### The span associated to a binary relation + +Given a binary relation `R : A → B → 𝒰`, we obtain a span + +```text + A <----- Σ (a : A), Σ (b : B), R a b -----> B. +``` + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (R : A → B → UU l3) + where + + spanning-type-span-binary-relation : UU (l1 ⊔ l2 ⊔ l3) + spanning-type-span-binary-relation = Σ A (λ a → Σ B (λ b → R a b)) + + left-map-span-binary-relation : spanning-type-span-binary-relation → A + left-map-span-binary-relation = pr1 + + right-map-span-binary-relation : spanning-type-span-binary-relation → B + right-map-span-binary-relation = pr1 ∘ pr2 + + span-binary-relation : span (l1 ⊔ l2 ⊔ l3) A B + pr1 span-binary-relation = spanning-type-span-binary-relation + pr1 (pr2 span-binary-relation) = left-map-span-binary-relation + pr2 (pr2 span-binary-relation) = right-map-span-binary-relation +``` + +### The binary relation associated to a span + +Given a span + +```text + f g + A <----- S -----> B +``` + +we obtain the binary relation `a b ↦ Σ (s : S), (f s = a) × (g s = b)`. + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} + where + + binary-relation-span : span l3 A B → A → B → UU (l1 ⊔ l2 ⊔ l3) + binary-relation-span S a b = + Σ ( spanning-type-span S) + ( λ s → (left-map-span S s = a) × (right-map-span S s = b)) +``` + +## Properties + +### Any span `S` is equivalent to the span associated to the binary relation associated to `S` + +The construction of this equivalence of span diagrams is simply by pattern +matching all the way. + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (S : span l3 A B) + where + + map-equiv-spanning-type-span-binary-relation-span : + spanning-type-span S → + spanning-type-span-binary-relation (binary-relation-span S) + map-equiv-spanning-type-span-binary-relation-span s = + ( left-map-span S s , right-map-span S s , s , refl , refl) + + map-inv-equiv-spanning-type-span-binary-relation-span : + spanning-type-span-binary-relation (binary-relation-span S) → + spanning-type-span S + map-inv-equiv-spanning-type-span-binary-relation-span (a , b , s , _) = s + + is-section-map-inv-equiv-spanning-type-span-binary-relation-span : + is-section + ( map-equiv-spanning-type-span-binary-relation-span) + ( map-inv-equiv-spanning-type-span-binary-relation-span) + is-section-map-inv-equiv-spanning-type-span-binary-relation-span + ( ._ , ._ , s , refl , refl) = + refl + + is-retraction-map-inv-equiv-spanning-type-span-binary-relation-span : + is-retraction + ( map-equiv-spanning-type-span-binary-relation-span) + ( map-inv-equiv-spanning-type-span-binary-relation-span) + is-retraction-map-inv-equiv-spanning-type-span-binary-relation-span s = refl + + is-equiv-map-equiv-spanning-type-span-binary-relation-span : + is-equiv + ( map-equiv-spanning-type-span-binary-relation-span) + is-equiv-map-equiv-spanning-type-span-binary-relation-span = + is-equiv-is-invertible + ( map-inv-equiv-spanning-type-span-binary-relation-span) + ( is-section-map-inv-equiv-spanning-type-span-binary-relation-span) + ( is-retraction-map-inv-equiv-spanning-type-span-binary-relation-span) + + equiv-spanning-type-span-binary-relation-span : + spanning-type-span S ≃ + spanning-type-span-binary-relation (binary-relation-span S) + pr1 equiv-spanning-type-span-binary-relation-span = + map-equiv-spanning-type-span-binary-relation-span + pr2 equiv-spanning-type-span-binary-relation-span = + is-equiv-map-equiv-spanning-type-span-binary-relation-span + + equiv-span-binary-relation-span : + equiv-span S (span-binary-relation (binary-relation-span S)) + pr1 equiv-span-binary-relation-span = + equiv-spanning-type-span-binary-relation-span + pr1 (pr2 equiv-span-binary-relation-span) = + refl-htpy + pr2 (pr2 equiv-span-binary-relation-span) = + refl-htpy +``` + +### Any binary relation `R` is equivalent to the binary relation associated to the span associated to `R` + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (R : A → B → UU l3) + (a : A) (b : B) + where + + map-equiv-binary-relation-span-binary-relation : + R a b → binary-relation-span (span-binary-relation R) a b + map-equiv-binary-relation-span-binary-relation r = + ((a , b , r) , refl , refl) + + map-inv-equiv-binary-relation-span-binary-relation : + binary-relation-span (span-binary-relation R) a b → R a b + map-inv-equiv-binary-relation-span-binary-relation + ((.a , .b , r) , refl , refl) = + r + + is-section-map-inv-equiv-binary-relation-span-binary-relation : + is-section + ( map-equiv-binary-relation-span-binary-relation) + ( map-inv-equiv-binary-relation-span-binary-relation) + is-section-map-inv-equiv-binary-relation-span-binary-relation + ((.a , .b , r) , refl , refl) = + refl + + is-retraction-map-inv-equiv-binary-relation-span-binary-relation : + is-retraction + ( map-equiv-binary-relation-span-binary-relation) + ( map-inv-equiv-binary-relation-span-binary-relation) + is-retraction-map-inv-equiv-binary-relation-span-binary-relation r = refl + + is-equiv-map-equiv-binary-relation-span-binary-relation : + is-equiv map-equiv-binary-relation-span-binary-relation + is-equiv-map-equiv-binary-relation-span-binary-relation = + is-equiv-is-invertible + map-inv-equiv-binary-relation-span-binary-relation + is-section-map-inv-equiv-binary-relation-span-binary-relation + is-retraction-map-inv-equiv-binary-relation-span-binary-relation + + equiv-binary-relation-span-binary-relation : + R a b ≃ binary-relation-span (span-binary-relation R) a b + pr1 equiv-binary-relation-span-binary-relation = + map-equiv-binary-relation-span-binary-relation + pr2 equiv-binary-relation-span-binary-relation = + is-equiv-map-equiv-binary-relation-span-binary-relation +``` + +## Theorem + +### Binary spans are equivalent to binary relations + +```agda +module _ + {l1 l2 l3 : Level} (A : UU l1) (B : UU l2) + where + + is-section-binary-relation-span : + is-section + ( span-binary-relation {l3 = l1 ⊔ l2 ⊔ l3} {A} {B}) + ( binary-relation-span {l3 = l1 ⊔ l2 ⊔ l3} {A} {B}) + is-section-binary-relation-span S = + inv + ( eq-equiv-span + ( S) + ( span-binary-relation (binary-relation-span S)) + ( equiv-span-binary-relation-span S)) + + is-retraction-binary-relation-span : + is-retraction + ( span-binary-relation {l3 = l1 ⊔ l2 ⊔ l3} {A} {B}) + ( binary-relation-span {l3 = l1 ⊔ l2 ⊔ l3} {A} {B}) + is-retraction-binary-relation-span R = + inv + ( eq-multivariable-htpy 2 + ( λ a b → eq-equiv (equiv-binary-relation-span-binary-relation R a b))) + + is-equiv-span-binary-relation : + is-equiv (span-binary-relation {l3 = l1 ⊔ l2 ⊔ l3} {A} {B}) + is-equiv-span-binary-relation = + is-equiv-is-invertible + ( binary-relation-span) + ( is-section-binary-relation-span) + ( is-retraction-binary-relation-span) + + binary-type-duality : (A → B → UU (l1 ⊔ l2 ⊔ l3)) ≃ span (l1 ⊔ l2 ⊔ l3) A B + pr1 binary-type-duality = span-binary-relation + pr2 binary-type-duality = is-equiv-span-binary-relation + + is-equiv-binary-relation-span : + is-equiv (binary-relation-span {l3 = l1 ⊔ l2 ⊔ l3} {A} {B}) + is-equiv-binary-relation-span = + is-equiv-is-invertible + ( span-binary-relation) + ( is-retraction-binary-relation-span) + ( is-section-binary-relation-span) + + inv-binary-type-duality : + span (l1 ⊔ l2 ⊔ l3) A B ≃ (A → B → UU (l1 ⊔ l2 ⊔ l3)) + pr1 inv-binary-type-duality = binary-relation-span + pr2 inv-binary-type-duality = is-equiv-binary-relation-span +``` diff --git a/src/foundation/cartesian-morphisms-arrows.lagda.md b/src/foundation/cartesian-morphisms-arrows.lagda.md index e20aa4ce38..94fda98c74 100644 --- a/src/foundation/cartesian-morphisms-arrows.lagda.md +++ b/src/foundation/cartesian-morphisms-arrows.lagda.md @@ -7,7 +7,7 @@ module foundation.cartesian-morphisms-arrows where
Imports ```agda -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.fibers-of-maps open import foundation.morphisms-arrows diff --git a/src/foundation/commuting-cubes-of-maps.lagda.md b/src/foundation/commuting-cubes-of-maps.lagda.md index 5631efcdf6..9ffd6c5f80 100644 --- a/src/foundation/commuting-cubes-of-maps.lagda.md +++ b/src/foundation/commuting-cubes-of-maps.lagda.md @@ -10,7 +10,7 @@ module foundation.commuting-cubes-of-maps where open import foundation.action-on-identifications-functions open import foundation.commuting-hexagons-of-identifications open import foundation.commuting-squares-of-maps -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.homotopies open import foundation.universe-levels diff --git a/src/foundation/cones-over-cospans.lagda.md b/src/foundation/cones-over-cospan-diagrams.lagda.md similarity index 93% rename from src/foundation/cones-over-cospans.lagda.md rename to src/foundation/cones-over-cospan-diagrams.lagda.md index 79c663903f..e7aadaf37b 100644 --- a/src/foundation/cones-over-cospans.lagda.md +++ b/src/foundation/cones-over-cospan-diagrams.lagda.md @@ -1,7 +1,7 @@ -# Cones over cospans +# Cones over cospan diagrams ```agda -module foundation.cones-over-cospans where +module foundation.cones-over-cospan-diagrams where ```
Imports @@ -28,9 +28,10 @@ open import foundation-core.whiskering-homotopies ## Idea -A **cone over a [cospan](foundation.cospans.md)** `A -f-> X <-g- B` with domain -`C` is a triple `(p, q, H)` consisting of a map `p : C → A`, a map `q : C → B`, -and a homotopy `H` witnessing that the square +A {{#concept "cone" Disambiguation="cospan diagram" Agda=cone}} over a +[cospan diagram](foundation.cospans.md) `A -f-> X <-g- B` with domain `C` is a +triple `(p, q, H)` consisting of a map `p : C → A`, a map `q : C → B`, and a +[homotopy](foundation-core.homotopies.md) `H` witnessing that the square ```text q @@ -42,7 +43,7 @@ and a homotopy `H` witnessing that the square f ``` -commutes. +[commutes](foundation-core.commuting-squares-of-maps.md). ## Definitions @@ -81,7 +82,7 @@ module _ hom-arrow-cone' = transpose-hom-arrow vertical-map-cone g hom-arrow-cone ``` -### Dependent cones over cospans +### Dependent cones over cospan diagrams ```agda cone-family : @@ -100,7 +101,7 @@ cone-family {C = C} PX {f = f} {g} f' g' c PC = ( PC x) ``` -### Identifications of cones over cospans +### Identifications of cones over cospan diagram ```agda module _ @@ -154,7 +155,7 @@ module _ eq-htpy-cone c c' = map-inv-equiv (extensionality-cone c c') ``` -### Precomposing cones over cospans with a map +### Precomposing cones over cospan diagrams with a map ```agda module _ @@ -245,7 +246,7 @@ pr1 (pr2 (swap-cone f g c)) = vertical-map-cone f g c pr2 (pr2 (swap-cone f g c)) = inv-htpy (coherence-square-cone f g c) ``` -### Parallel cones over cospans +### Parallel cones over cospan diagrams ```agda module _ diff --git a/src/foundation/constant-span-diagrams.lagda.md b/src/foundation/constant-span-diagrams.lagda.md new file mode 100644 index 0000000000..eb2e81061d --- /dev/null +++ b/src/foundation/constant-span-diagrams.lagda.md @@ -0,0 +1,66 @@ +# Constant span diagrams + +```agda +module foundation.constant-span-diagrams where +``` + +
Imports + +```agda +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.span-diagrams +open import foundation.spans +open import foundation.universe-levels + +open import foundation-core.equivalences +``` + +
+ +## Idea + +The {{#concept "constant span diagram" Agda=constant-span-diagram}} at a type +`X` is the [span diagram](foundation.span-diagrams.md) + +```text + id id + X <----- X -----> X. +``` + +Alternatively, a span diagram + +```text + f g + A <----- S -----> B +``` + +is said to be constant if both `f` and `g` are +[equivalences](foundation-core.equivalences.md). + +## Definitions + +### Constant span diagrams at a type + +```agda +module _ + {l1 : Level} + where + + constant-span-diagram : UU l1 → span-diagram l1 l1 l1 + pr1 (constant-span-diagram X) = X + pr1 (pr2 (constant-span-diagram X)) = X + pr2 (pr2 (constant-span-diagram X)) = id-span +``` + +### The predicate of being a constant span diagram + +```agda +module _ + {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3) + where + + is-constant-span-diagram : UU (l1 ⊔ l2 ⊔ l3) + is-constant-span-diagram = + is-equiv (left-map-span-diagram 𝒮) × is-equiv (right-map-span-diagram 𝒮) +``` diff --git a/src/foundation/cospan-diagrams.lagda.md b/src/foundation/cospan-diagrams.lagda.md new file mode 100644 index 0000000000..a54f19b2c2 --- /dev/null +++ b/src/foundation/cospan-diagrams.lagda.md @@ -0,0 +1,43 @@ +# Cospan diagrams + +```agda +module foundation.cospan-diagrams where +``` + +
Imports + +```agda +open import foundation.cospans +open import foundation.dependent-pair-types +open import foundation.universe-levels +``` + +
+ +## Idea + +A {{#concept "cospan diagram" Agda=cospan-diagram}} consists of two types `A` +and `B` and a [cospan](foundation.cospans.md) `A -f-> X <-g- B` between them. + +## Definitions + +```agda +cospan-diagram : + (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) +cospan-diagram l1 l2 l3 = + Σ (UU l1) (λ A → Σ (UU l2) (cospan l3 A)) + +module _ + {l1 l2 l3 : Level} (c : cospan-diagram l1 l2 l3) + where + + left-type-cospan-diagram : UU l1 + left-type-cospan-diagram = pr1 c + + right-type-cospan-diagram : UU l2 + right-type-cospan-diagram = pr1 (pr2 c) + + cospan-cospan-diagram : + cospan l3 left-type-cospan-diagram right-type-cospan-diagram + cospan-cospan-diagram = pr2 (pr2 c) +``` diff --git a/src/foundation/cospans.lagda.md b/src/foundation/cospans.lagda.md index 1328e7dacd..045c95e8f5 100644 --- a/src/foundation/cospans.lagda.md +++ b/src/foundation/cospans.lagda.md @@ -27,14 +27,27 @@ open import foundation-core.torsorial-type-families ## Idea -A {{#concept "cospan" Disambiguation="types" Agda=cospan}} is a -[pair](foundation.dependent-pair-types.md) of functions with a common codomain +A {{#concept "cospan" Disambiguation="types" Agda=cospan}} from `A` to `B` +consists of a type `X` and maps `f : A → X` and `g : B → X`, as indicated in the +diagram ```text - f : A → X ← B : g. + f g + A -----> X <----- B ``` -## Definition +We disambiguate between cospans and +[cospan diagrams](foundation.cospan-diagrams.md). We consider a cospan from `A` +to `B` a morphism from `A` to `B` in the category of types and cospans between +them, whereas we consider cospan diagrams to be _objects_ in the category of +diagrams of types of the form `* <---- * ----> *`. Conceptually there is a +subtle, but important distinction between cospans and cospan diagrams. Cospan +diagrams are more suitable for functorial operations that take "cospans" as +input, but for which the functorial action takes a natural transformation, i.e., +a morphism of cospan diagrams, as input. Examples of this kind include +[pullbacks](foundation.pullbacks.md). + +## Definitions ### Cospans @@ -59,91 +72,13 @@ module _ right-map-cospan = pr2 (pr2 c) ``` -### Homomorphisms between cospans with fixed domains - -One notion of homomorphism of cospans `c` and `d` with common domains is a map -between their codomains so that the triangles on either side commute: - -```text - A ===== A - | | - v v - C ----> D - ^ ^ - | | - B ===== B -``` - -```agda -module _ - {l1 l2 : Level} {l : Level} {A : UU l1} {B : UU l2} - where - - coherence-hom-codomain-cospan : - (c d : cospan l A B) → - (codomain-cospan c → codomain-cospan d) → UU (l1 ⊔ l2 ⊔ l) - coherence-hom-codomain-cospan c d h = - ( coherence-triangle-maps (left-map-cospan d) h (left-map-cospan c)) × - ( coherence-triangle-maps (right-map-cospan d) h (right-map-cospan c)) - - hom-codomain-cospan : (c d : cospan l A B) → UU (l1 ⊔ l2 ⊔ l) - hom-codomain-cospan c d = - Σ ( codomain-cospan c → codomain-cospan d) - ( coherence-hom-codomain-cospan c d) -``` - -## Properties - -### Characterizing equality of cospans - -```agda -module _ - {l1 l2 : Level} (l : Level) (A : UU l1) (B : UU l2) - where - - htpy-cospan : (c d : cospan l A B) → UU (l1 ⊔ l2 ⊔ l) - htpy-cospan c d = - Σ ( codomain-cospan c ≃ codomain-cospan d) - ( λ e → coherence-hom-codomain-cospan c d (map-equiv e)) - - refl-htpy-cospan : (c : cospan l A B) → htpy-cospan c c - pr1 (refl-htpy-cospan c) = id-equiv - pr1 (pr2 (refl-htpy-cospan c)) = refl-htpy - pr2 (pr2 (refl-htpy-cospan c)) = refl-htpy - - htpy-eq-cospan : (c d : cospan l A B) → c = d → htpy-cospan c d - htpy-eq-cospan c .c refl = refl-htpy-cospan c - - is-torsorial-htpy-cospan : - (c : cospan l A B) → is-torsorial (htpy-cospan c) - is-torsorial-htpy-cospan c = - is-torsorial-Eq-structure - ( is-torsorial-equiv (pr1 c)) - ( codomain-cospan c , id-equiv) - ( is-torsorial-Eq-structure - ( is-torsorial-htpy' (left-map-cospan c)) - ( left-map-cospan c , refl-htpy) - (is-torsorial-htpy' (right-map-cospan c))) - - is-equiv-htpy-eq-cospan : - (c d : cospan l A B) → is-equiv (htpy-eq-cospan c d) - is-equiv-htpy-eq-cospan c = - fundamental-theorem-id (is-torsorial-htpy-cospan c) (htpy-eq-cospan c) - - extensionality-cospan : - (c d : cospan l A B) → (c = d) ≃ (htpy-cospan c d) - pr1 (extensionality-cospan c d) = htpy-eq-cospan c d - pr2 (extensionality-cospan c d) = is-equiv-htpy-eq-cospan c d - - eq-htpy-cospan : (c d : cospan l A B) → htpy-cospan c d → c = d - eq-htpy-cospan c d = map-inv-equiv (extensionality-cospan c d) -``` - ## See also - The formal dual of cospans is [spans](foundation.spans.md). +- [Pullbacks](foundation-core.pullbacks.md) are limits of + [cospan diagrams](foundation.cospan-diagrams.md). -## Table of files about pullbacks +### Table of files about pullbacks The following table lists files that are about pullbacks as a general concept. diff --git a/src/foundation/dependent-function-types.lagda.md b/src/foundation/dependent-function-types.lagda.md new file mode 100644 index 0000000000..51ebd0bde3 --- /dev/null +++ b/src/foundation/dependent-function-types.lagda.md @@ -0,0 +1,81 @@ +# Dependent function types + +```agda +module foundation.dependent-function-types where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.spans-families-of-types +open import foundation.terminal-spans-families-of-types +open import foundation.type-arithmetic-dependent-function-types +open import foundation.universal-property-dependent-function-types +open import foundation.universe-levels +``` + +
+ +## Idea + +Consider a family `B` of types over `A`. A {{#concept "dependent function"}} +that takes elements `x : A` to elements of type `B x` is an assignment of an +element `f x : B x` for each `x : A`. In Agda, dependent functions can be +written using `λ`-abstraction, i.e., using the syntax + +```text + λ x → f x. +``` + +Informally, we also use the notation `x ↦ f x` for the assignment of values of a +dependent function `f`. + +The type of dependent function `(x : A) → B x` is built in to the kernel of +Agda, and doesn't need to be introduced by us. The purpose of this file is to +record some properties of dependent function types. + +## Definitions + +### The structure of a span on a family of types on a dependent function type + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (B : A → UU l2) + where + + span-type-family-Π : span-type-family (l1 ⊔ l2) B + pr1 span-type-family-Π = (x : A) → B x + pr2 span-type-family-Π x f = f x +``` + +## Properties + +### Dependent function types satisfy the universal property of dependent function types + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (B : A → UU l2) + where + + abstract + universal-property-dependent-function-types-Π : + universal-property-dependent-function-types (span-type-family-Π B) + universal-property-dependent-function-types-Π T = is-equiv-swap-Π +``` + +### Dependent function types are terminal spans on families of types + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (B : A → UU l2) + where + + abstract + is-terminal-span-type-family-Π : + is-terminal-span-type-family (span-type-family-Π B) + is-terminal-span-type-family-Π = + is-terminal-universal-property-dependent-function-types + ( span-type-family-Π B) + ( universal-property-dependent-function-types-Π B) +``` diff --git a/src/foundation/dependent-homotopies.lagda.md b/src/foundation/dependent-homotopies.lagda.md index 27e973f0e3..eaac3938b5 100644 --- a/src/foundation/dependent-homotopies.lagda.md +++ b/src/foundation/dependent-homotopies.lagda.md @@ -26,7 +26,8 @@ functions `f g : (x : A) → B x`. Furthermore, consider a type family g' : (x : A) → C x (g x) ``` -A **dependent homotopy** from `f'` to `g'` over `H` is a family of +A {{#concept "dependent homotopy" Agda=dependent-homotopy}} from `f'` to `g'` +over `H` is a family of [dependent identifications](foundation-core.dependent-identifications.md) from `f' x` to `g' x` over `H x`. diff --git a/src/foundation/descent-coproduct-types.lagda.md b/src/foundation/descent-coproduct-types.lagda.md index 49319f7477..d0c3880ffc 100644 --- a/src/foundation/descent-coproduct-types.lagda.md +++ b/src/foundation/descent-coproduct-types.lagda.md @@ -8,7 +8,7 @@ module foundation.descent-coproduct-types where ```agda open import foundation.action-on-identifications-functions -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.functoriality-coproduct-types open import foundation.functoriality-fibers-of-maps diff --git a/src/foundation/descent-dependent-pair-types.lagda.md b/src/foundation/descent-dependent-pair-types.lagda.md index b111c50337..9f3cdfc133 100644 --- a/src/foundation/descent-dependent-pair-types.lagda.md +++ b/src/foundation/descent-dependent-pair-types.lagda.md @@ -7,7 +7,7 @@ module foundation.descent-dependent-pair-types where
Imports ```agda -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.functoriality-fibers-of-maps open import foundation.universe-levels diff --git a/src/foundation/descent-empty-types.lagda.md b/src/foundation/descent-empty-types.lagda.md index 4f80cf53a5..ca408517a6 100644 --- a/src/foundation/descent-empty-types.lagda.md +++ b/src/foundation/descent-empty-types.lagda.md @@ -7,7 +7,7 @@ module foundation.descent-empty-types where
Imports ```agda -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.universe-levels diff --git a/src/foundation/descent-equivalences.lagda.md b/src/foundation/descent-equivalences.lagda.md index c835b57cc9..108a879578 100644 --- a/src/foundation/descent-equivalences.lagda.md +++ b/src/foundation/descent-equivalences.lagda.md @@ -7,7 +7,7 @@ module foundation.descent-equivalences where
Imports ```agda -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-universal-property-equivalences open import foundation.equivalences open import foundation.functoriality-fibers-of-maps diff --git a/src/foundation/diagonal-span-diagrams.lagda.md b/src/foundation/diagonal-span-diagrams.lagda.md new file mode 100644 index 0000000000..bde07d12e9 --- /dev/null +++ b/src/foundation/diagonal-span-diagrams.lagda.md @@ -0,0 +1,38 @@ +# Diagonal span diagrams + +```agda +module foundation.diagonal-span-diagrams where +``` + +
Imports + +```agda +open import foundation.span-diagrams +open import foundation.universe-levels +``` + +
+ +## Idea + +Consider a map `f : A → B`. The +{{#concept "diagonal span diagram" Agda=diagonal-span-diagram}} of `f` is the +[span diagram](foundation.span-diagrams.md) + +```text + f f + B <----- A -----> B. +``` + +## Definitions + +### Diagonal span diagrams of maps + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + diagonal-span-diagram : span-diagram l2 l2 l1 + diagonal-span-diagram = make-span-diagram f f +``` diff --git a/src/foundation/embeddings.lagda.md b/src/foundation/embeddings.lagda.md index 24bac8e1e7..d231edfd31 100644 --- a/src/foundation/embeddings.lagda.md +++ b/src/foundation/embeddings.lagda.md @@ -11,7 +11,7 @@ open import foundation-core.embeddings public ```agda open import foundation.action-on-identifications-functions open import foundation.commuting-squares-of-maps -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.functoriality-cartesian-product-types diff --git a/src/foundation/equality-dependent-pair-types.lagda.md b/src/foundation/equality-dependent-pair-types.lagda.md index d162d8b671..cc60a621f4 100644 --- a/src/foundation/equality-dependent-pair-types.lagda.md +++ b/src/foundation/equality-dependent-pair-types.lagda.md @@ -90,6 +90,11 @@ module _ inv (eq-pair-Σ p p') = eq-pair-Σ (inv p) (inv-dependent-identification B p p') distributive-inv-eq-pair-Σ refl refl = refl + + distributive-inv-eq-pair-Σ-refl : + {x : A} {x' y' : B x} (p' : x' = y') → + inv (eq-pair-Σ refl p') = eq-pair-Σ {A = A} {B = B} refl (inv p') + distributive-inv-eq-pair-Σ-refl refl = refl ``` ### Computing `pair-eq-Σ` at an identification of the form `ap f p` diff --git a/src/foundation/equivalences-arrows.lagda.md b/src/foundation/equivalences-arrows.lagda.md index 000c4c22ef..1ffc0e07da 100644 --- a/src/foundation/equivalences-arrows.lagda.md +++ b/src/foundation/equivalences-arrows.lagda.md @@ -7,28 +7,18 @@ module foundation.equivalences-arrows where
Imports ```agda -open import foundation.action-on-identifications-functions open import foundation.cartesian-morphisms-arrows -open import foundation.commuting-squares-of-homotopies -open import foundation.commuting-squares-of-identifications open import foundation.commuting-squares-of-maps -open import foundation.commuting-triangles-of-identifications -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.equivalences -open import foundation.fundamental-theorem-of-identity-types -open import foundation.homotopy-induction +open import foundation.homotopies open import foundation.morphisms-arrows -open import foundation.path-algebra -open import foundation.structure-identity-principle +open import foundation.span-diagrams +open import foundation.spans open import foundation.universe-levels -open import foundation-core.cartesian-product-types -open import foundation-core.function-types -open import foundation-core.homotopies -open import foundation-core.identity-types -open import foundation-core.torsorial-type-families -open import foundation-core.whiskering-homotopies +open import foundation-core.propositions ```
@@ -40,41 +30,49 @@ function `g : X → Y` is a [morphism of arrows](foundation.morphisms-arrows.md) ```text i - A ----> X - | | - f | H | g - v v - B ----> Y + A -----> X + | ≃ | + f | | g + V ≃ V + B -----> Y j ``` -such that `i` and `j` are [equivalences](foundation-core.equivalences.md). +in which `i` and `j` are [equivalences](foundation-core.equivalences.md). ## Definitions -### The predicate of being an equivalence of arrows on morphisms of arrows +### The predicate of being an equivalence of arrows ```agda module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - (f : A → B) (g : X → Y) (α : hom-arrow f g) + (f : A → B) (g : X → Y) (h : hom-arrow f g) where + is-equiv-prop-hom-arrow : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4) + is-equiv-prop-hom-arrow = + prod-Prop + ( is-equiv-Prop (map-domain-hom-arrow f g h)) + ( is-equiv-Prop (map-codomain-hom-arrow f g h)) + is-equiv-hom-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) is-equiv-hom-arrow = - is-equiv (map-domain-hom-arrow f g α) × - is-equiv (map-codomain-hom-arrow f g α) + type-Prop is-equiv-prop-hom-arrow + + is-prop-is-equiv-hom-arrow : is-prop is-equiv-hom-arrow + is-prop-is-equiv-hom-arrow = is-prop-type-Prop is-equiv-prop-hom-arrow is-equiv-map-domain-is-equiv-hom-arrow : - is-equiv-hom-arrow → is-equiv (map-domain-hom-arrow f g α) + is-equiv-hom-arrow → is-equiv (map-domain-hom-arrow f g h) is-equiv-map-domain-is-equiv-hom-arrow = pr1 is-equiv-map-codomain-is-equiv-hom-arrow : - is-equiv-hom-arrow → is-equiv (map-codomain-hom-arrow f g α) + is-equiv-hom-arrow → is-equiv (map-codomain-hom-arrow f g h) is-equiv-map-codomain-is-equiv-hom-arrow = pr2 ``` -### The type of equivalences of arrows +### Equivalences of arrows ```agda module _ @@ -82,49 +80,62 @@ module _ (f : A → B) (g : X → Y) where + coherence-equiv-arrow : (A ≃ X) → (B ≃ Y) → UU (l1 ⊔ l4) + coherence-equiv-arrow i j = + coherence-hom-arrow f g (map-equiv i) (map-equiv j) + equiv-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) - equiv-arrow = Σ (hom-arrow f g) (is-equiv-hom-arrow f g) + equiv-arrow = + Σ (A ≃ X) (λ i → Σ (B ≃ Y) (coherence-equiv-arrow i)) -module _ - {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - (f : A → B) (g : X → Y) (α : equiv-arrow f g) - where + module _ + (e : equiv-arrow) + where - hom-arrow-equiv-arrow : hom-arrow f g - hom-arrow-equiv-arrow = pr1 α + equiv-domain-equiv-arrow : A ≃ X + equiv-domain-equiv-arrow = pr1 e - is-equiv-hom-arrow-equiv-arrow : is-equiv-hom-arrow f g hom-arrow-equiv-arrow - is-equiv-hom-arrow-equiv-arrow = pr2 α + map-domain-equiv-arrow : A → X + map-domain-equiv-arrow = map-equiv equiv-domain-equiv-arrow - map-domain-equiv-arrow : A → X - map-domain-equiv-arrow = map-domain-hom-arrow f g hom-arrow-equiv-arrow + is-equiv-map-domain-equiv-arrow : is-equiv map-domain-equiv-arrow + is-equiv-map-domain-equiv-arrow = + is-equiv-map-equiv equiv-domain-equiv-arrow - is-equiv-map-domain-equiv-arrow : is-equiv map-domain-equiv-arrow - is-equiv-map-domain-equiv-arrow = - is-equiv-map-domain-is-equiv-hom-arrow f g - ( hom-arrow-equiv-arrow) - ( is-equiv-hom-arrow-equiv-arrow) + equiv-codomain-equiv-arrow : B ≃ Y + equiv-codomain-equiv-arrow = pr1 (pr2 e) - equiv-domain-equiv-arrow : A ≃ X - pr1 equiv-domain-equiv-arrow = map-domain-equiv-arrow - pr2 equiv-domain-equiv-arrow = is-equiv-map-domain-equiv-arrow + map-codomain-equiv-arrow : B → Y + map-codomain-equiv-arrow = map-equiv equiv-codomain-equiv-arrow - map-codomain-equiv-arrow : B → Y - map-codomain-equiv-arrow = map-codomain-hom-arrow f g hom-arrow-equiv-arrow + is-equiv-map-codomain-equiv-arrow : is-equiv map-codomain-equiv-arrow + is-equiv-map-codomain-equiv-arrow = + is-equiv-map-equiv equiv-codomain-equiv-arrow - is-equiv-map-codomain-equiv-arrow : is-equiv map-codomain-equiv-arrow - is-equiv-map-codomain-equiv-arrow = - is-equiv-map-codomain-is-equiv-hom-arrow f g - ( hom-arrow-equiv-arrow) - ( is-equiv-hom-arrow-equiv-arrow) + coh-equiv-arrow : + coherence-equiv-arrow + ( equiv-domain-equiv-arrow) + ( equiv-codomain-equiv-arrow) + coh-equiv-arrow = pr2 (pr2 e) - equiv-codomain-equiv-arrow : B ≃ Y - pr1 equiv-codomain-equiv-arrow = map-codomain-equiv-arrow - pr2 equiv-codomain-equiv-arrow = is-equiv-map-codomain-equiv-arrow + hom-equiv-arrow : hom-arrow f g + pr1 hom-equiv-arrow = map-domain-equiv-arrow + pr1 (pr2 hom-equiv-arrow) = map-codomain-equiv-arrow + pr2 (pr2 hom-equiv-arrow) = coh-equiv-arrow - coh-equiv-arrow : - coherence-square-maps map-domain-equiv-arrow f g map-codomain-equiv-arrow - coh-equiv-arrow = coh-hom-arrow f g hom-arrow-equiv-arrow + is-equiv-equiv-arrow : is-equiv-hom-arrow f g hom-equiv-arrow + pr1 is-equiv-equiv-arrow = is-equiv-map-domain-equiv-arrow + pr2 is-equiv-equiv-arrow = is-equiv-map-codomain-equiv-arrow + + span-equiv-arrow : + span l1 B X + span-equiv-arrow = + span-hom-arrow f g hom-equiv-arrow + + span-diagram-equiv-arrow : span-diagram l2 l3 l1 + pr1 span-diagram-equiv-arrow = B + pr1 (pr2 span-diagram-equiv-arrow) = X + pr2 (pr2 span-diagram-equiv-arrow) = span-equiv-arrow ``` ### The identity equivalence of arrows @@ -135,9 +146,9 @@ module _ where id-equiv-arrow : equiv-arrow f f - pr1 id-equiv-arrow = id-hom-arrow - pr1 (pr2 id-equiv-arrow) = is-equiv-id - pr2 (pr2 id-equiv-arrow) = is-equiv-id + pr1 id-equiv-arrow = id-equiv + pr1 (pr2 id-equiv-arrow) = id-equiv + pr2 (pr2 id-equiv-arrow) = refl-htpy ``` ### Composition of equivalences of arrows @@ -150,23 +161,36 @@ module _ (b : equiv-arrow g h) (a : equiv-arrow f g) where + equiv-domain-comp-equiv-arrow : A ≃ U + equiv-domain-comp-equiv-arrow = + equiv-domain-equiv-arrow g h b ∘e equiv-domain-equiv-arrow f g a + + map-domain-comp-equiv-arrow : A → U + map-domain-comp-equiv-arrow = map-equiv equiv-domain-comp-equiv-arrow + + equiv-codomain-comp-equiv-arrow : B ≃ V + equiv-codomain-comp-equiv-arrow = + equiv-codomain-equiv-arrow g h b ∘e equiv-codomain-equiv-arrow f g a + + map-codomain-comp-equiv-arrow : B → V + map-codomain-comp-equiv-arrow = map-equiv equiv-codomain-comp-equiv-arrow + + coh-comp-equiv-arrow : + coherence-equiv-arrow f h + ( equiv-domain-comp-equiv-arrow) + ( equiv-codomain-comp-equiv-arrow) + coh-comp-equiv-arrow = + coh-comp-hom-arrow f g h + ( hom-equiv-arrow g h b) + ( hom-equiv-arrow f g a) + comp-equiv-arrow : equiv-arrow f h - pr1 comp-equiv-arrow = - comp-hom-arrow f g h - ( hom-arrow-equiv-arrow g h b) - ( hom-arrow-equiv-arrow f g a) - pr1 (pr2 comp-equiv-arrow) = - is-equiv-comp - ( map-domain-equiv-arrow g h b) - ( map-domain-equiv-arrow f g a) - ( is-equiv-map-domain-equiv-arrow f g a) - ( is-equiv-map-domain-equiv-arrow g h b) - pr2 (pr2 comp-equiv-arrow) = - is-equiv-comp - ( map-codomain-equiv-arrow g h b) - ( map-codomain-equiv-arrow f g a) - ( is-equiv-map-codomain-equiv-arrow f g a) - ( is-equiv-map-codomain-equiv-arrow g h b) + pr1 comp-equiv-arrow = equiv-domain-comp-equiv-arrow + pr1 (pr2 comp-equiv-arrow) = equiv-codomain-comp-equiv-arrow + pr2 (pr2 comp-equiv-arrow) = coh-comp-equiv-arrow + + hom-comp-equiv-arrow : hom-arrow f h + hom-comp-equiv-arrow = hom-equiv-arrow f h comp-equiv-arrow ``` ### Inverses of equivalences of arrows @@ -177,12 +201,23 @@ module _ (f : A → B) (g : X → Y) (α : equiv-arrow f g) where - hom-inv-equiv-arrow : hom-arrow g f - pr1 hom-inv-equiv-arrow = - map-inv-is-equiv (is-equiv-map-domain-equiv-arrow f g α) - pr1 (pr2 hom-inv-equiv-arrow) = - map-inv-is-equiv (is-equiv-map-codomain-equiv-arrow f g α) - pr2 (pr2 hom-inv-equiv-arrow) = + equiv-domain-inv-equiv-arrow : X ≃ A + equiv-domain-inv-equiv-arrow = inv-equiv (equiv-domain-equiv-arrow f g α) + + map-domain-inv-equiv-arrow : X → A + map-domain-inv-equiv-arrow = map-equiv equiv-domain-inv-equiv-arrow + + equiv-codomain-inv-equiv-arrow : Y ≃ B + equiv-codomain-inv-equiv-arrow = inv-equiv (equiv-codomain-equiv-arrow f g α) + + map-codomain-inv-equiv-arrow : Y → B + map-codomain-inv-equiv-arrow = map-equiv equiv-codomain-inv-equiv-arrow + + coh-inv-equiv-arrow : + coherence-equiv-arrow g f + ( equiv-domain-inv-equiv-arrow) + ( equiv-codomain-inv-equiv-arrow) + coh-inv-equiv-arrow = coherence-square-inv-horizontal ( equiv-domain-equiv-arrow f g α) ( f) @@ -190,15 +225,16 @@ module _ ( equiv-codomain-equiv-arrow f g α) ( coh-equiv-arrow f g α) - is-equiv-inv-equiv-arrow : is-equiv-hom-arrow g f hom-inv-equiv-arrow - pr1 is-equiv-inv-equiv-arrow = - is-equiv-map-inv-is-equiv (is-equiv-map-domain-equiv-arrow f g α) - pr2 is-equiv-inv-equiv-arrow = - is-equiv-map-inv-is-equiv (is-equiv-map-codomain-equiv-arrow f g α) - inv-equiv-arrow : equiv-arrow g f - pr1 inv-equiv-arrow = hom-inv-equiv-arrow - pr2 inv-equiv-arrow = is-equiv-inv-equiv-arrow + pr1 inv-equiv-arrow = equiv-domain-inv-equiv-arrow + pr1 (pr2 inv-equiv-arrow) = equiv-codomain-inv-equiv-arrow + pr2 (pr2 inv-equiv-arrow) = coh-inv-equiv-arrow + + hom-inv-equiv-arrow : hom-arrow g f + hom-inv-equiv-arrow = hom-equiv-arrow g f inv-equiv-arrow + + is-equiv-inv-equiv-arrow : is-equiv-hom-arrow g f hom-inv-equiv-arrow + is-equiv-inv-equiv-arrow = is-equiv-equiv-arrow g f inv-equiv-arrow ``` ### If a map is equivalent to an equivalence, then it is an equivalence @@ -241,16 +277,16 @@ module _ where is-cartesian-equiv-arrow : - is-cartesian-hom-arrow f g (hom-arrow-equiv-arrow f g α) + is-cartesian-hom-arrow f g (hom-equiv-arrow f g α) is-cartesian-equiv-arrow = is-pullback-is-equiv-horizontal-maps ( map-codomain-equiv-arrow f g α) ( g) - ( cone-hom-arrow f g (hom-arrow-equiv-arrow f g α)) + ( cone-hom-arrow f g (hom-equiv-arrow f g α)) ( is-equiv-map-codomain-equiv-arrow f g α) ( is-equiv-map-domain-equiv-arrow f g α) - cartesian-hom-arrow-equiv-arrow : cartesian-hom-arrow f g - pr1 cartesian-hom-arrow-equiv-arrow = hom-arrow-equiv-arrow f g α - pr2 cartesian-hom-arrow-equiv-arrow = is-cartesian-equiv-arrow + cartesian-hom-equiv-arrow : cartesian-hom-arrow f g + pr1 cartesian-hom-equiv-arrow = hom-equiv-arrow f g α + pr2 cartesian-hom-equiv-arrow = is-cartesian-equiv-arrow ``` diff --git a/src/foundation/equivalences-cospans.lagda.md b/src/foundation/equivalences-cospans.lagda.md new file mode 100644 index 0000000000..aea864d493 --- /dev/null +++ b/src/foundation/equivalences-cospans.lagda.md @@ -0,0 +1,108 @@ +# Equivalences of cospans + +```agda +module foundation.equivalences-cospans where +``` + +
Imports + +```agda +open import foundation.cospans +open import foundation.dependent-pair-types +open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopy-induction +open import foundation.morphisms-cospans +open import foundation.structure-identity-principle +open import foundation.univalence +open import foundation.universe-levels + +open import foundation-core.equivalences +open import foundation-core.homotopies +open import foundation-core.identity-types +open import foundation-core.torsorial-type-families +``` + +
+ +## Idea + +An {{#concept "equivalence of cospans" Agda=equiv-cospan}} from +[cospans](foundation.cospans.md) `(X , f , g)` to `(Y , h , k)` between types +`A` and `B` consists of an [equivalence](foundation-core.equivalences.md) +`e : X ≃ Y` such that the triangles + +```text + e e + X ----> Y X ----> Y + \ / \ / + f \ / h g \ / k + V V V V + A B +``` + +both [commute](foundation.commuting-triangles-of-maps.md). + +## Definitions + +### Equivalences of cospans + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} + where + + equiv-cospan : cospan l3 A B → cospan l4 A B → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + equiv-cospan c d = + Σ ( codomain-cospan c ≃ codomain-cospan d) + ( λ e → coherence-hom-cospan c d (map-equiv e)) +``` + +### The identity equivalence of cospans + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} + where + + id-equiv-cospan : (c : cospan l3 A B) → equiv-cospan c c + pr1 (id-equiv-cospan c) = id-equiv + pr1 (pr2 (id-equiv-cospan c)) = refl-htpy + pr2 (pr2 (id-equiv-cospan c)) = refl-htpy +``` + +## Properties + +### Characterizing equality of cospans + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} + where + + equiv-eq-cospan : (c d : cospan l3 A B) → c = d → equiv-cospan c d + equiv-eq-cospan c .c refl = id-equiv-cospan c + + is-torsorial-equiv-cospan : + (c : cospan l3 A B) → is-torsorial (equiv-cospan c) + is-torsorial-equiv-cospan c = + is-torsorial-Eq-structure + ( is-torsorial-equiv (pr1 c)) + ( codomain-cospan c , id-equiv) + ( is-torsorial-Eq-structure + ( is-torsorial-htpy' (left-map-cospan c)) + ( left-map-cospan c , refl-htpy) + ( is-torsorial-htpy' (right-map-cospan c))) + + is-equiv-equiv-eq-cospan : + (c d : cospan l3 A B) → is-equiv (equiv-eq-cospan c d) + is-equiv-equiv-eq-cospan c = + fundamental-theorem-id (is-torsorial-equiv-cospan c) (equiv-eq-cospan c) + + extensionality-cospan : + (c d : cospan l3 A B) → (c = d) ≃ (equiv-cospan c d) + pr1 (extensionality-cospan c d) = equiv-eq-cospan c d + pr2 (extensionality-cospan c d) = is-equiv-equiv-eq-cospan c d + + eq-equiv-cospan : (c d : cospan l3 A B) → equiv-cospan c d → c = d + eq-equiv-cospan c d = map-inv-equiv (extensionality-cospan c d) +``` diff --git a/src/foundation/equivalences-maybe.lagda.md b/src/foundation/equivalences-maybe.lagda.md index fea02e6755..5a38bc210b 100644 --- a/src/foundation/equivalences-maybe.lagda.md +++ b/src/foundation/equivalences-maybe.lagda.md @@ -84,7 +84,7 @@ abstract is-exception-Maybe (map-equiv e (inl x)) → is-not-exception-Maybe (map-equiv e exception-Maybe) is-not-exception-map-equiv-exception-Maybe e = - is-not-exception-injective-map-exception-Maybe (is-injective-map-equiv e) + is-not-exception-injective-map-exception-Maybe (is-injective-equiv e) abstract is-not-exception-emb-exception-Maybe : @@ -224,12 +224,12 @@ map-equiv-equiv-Maybe' : {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) (x : X) (u : Maybe Y) (p : map-equiv e (inl x) = u) → Y map-equiv-equiv-Maybe' e = - restrict-injective-map-Maybe' (is-injective-map-equiv e) + restrict-injective-map-Maybe' (is-injective-equiv e) map-equiv-equiv-Maybe : {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) → X → Y map-equiv-equiv-Maybe e = - restrict-injective-map-Maybe (is-injective-map-equiv e) + restrict-injective-map-Maybe (is-injective-equiv e) compute-map-equiv-equiv-is-exception-Maybe' : {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) (x : X) → @@ -237,7 +237,7 @@ compute-map-equiv-equiv-is-exception-Maybe' : is-exception-Maybe (map-equiv e (inl x)) → inl (map-equiv-equiv-Maybe' e x u p) = map-equiv e exception-Maybe compute-map-equiv-equiv-is-exception-Maybe' e = - compute-restrict-injective-map-is-exception-Maybe' (is-injective-map-equiv e) + compute-restrict-injective-map-is-exception-Maybe' (is-injective-equiv e) compute-map-equiv-equiv-is-exception-Maybe : {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : Maybe X ≃ Maybe Y) (x : X) → diff --git a/src/foundation/equivalences-span-diagrams-families-of-types.lagda.md b/src/foundation/equivalences-span-diagrams-families-of-types.lagda.md new file mode 100644 index 0000000000..f7f3f6fd3c --- /dev/null +++ b/src/foundation/equivalences-span-diagrams-families-of-types.lagda.md @@ -0,0 +1,142 @@ +# Equivalences of span diagrams on families of types + +```agda +module foundation.equivalences-span-diagrams-families-of-types where +``` + +
Imports + +```agda +open import foundation.commuting-squares-of-maps +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.equivalences-spans-families-of-types +open import foundation.homotopies +open import foundation.operations-spans-families-of-types +open import foundation.span-diagrams-families-of-types +open import foundation.universe-levels +``` + +
+ +## Idea + +An +{{#concept "equivalence of span diagrams on families of types" Agda=equiv-span-diagram-type-family}} +from a [span](foundation.spans-families-of-types.md) `(A , s)` of families of +types indexed by a type `I` to a span `(B , t)` indexed by `I` consists of a +[family of equivalences](foundation-core.families-of-equivalences.md) +`h : Aᵢ ≃ Bᵢ`, and an equivalence `e : S ≃ T` +[equipped](foundation.structure.md) with a family of +[homotopies](foundation-core.homotopies.md) witnessing that the square + +```text + e + S -----> T + | | + fᵢ | | gᵢ + V V + Aᵢ ----> Bᵢ + h +``` + +[commutes](foundation-core.commuting-squares-of-maps.md) for each `i : I`. + +## Definitions + +### Equivalences of span diagrams on families of types + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} {I : UU l1} + (S : span-diagram-type-family l2 l3 I) + (T : span-diagram-type-family l4 l5 I) + where + + equiv-span-diagram-type-family : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5) + equiv-span-diagram-type-family = + Σ ( (i : I) → + family-span-diagram-type-family S i ≃ + family-span-diagram-type-family T i) + ( λ e → + equiv-span-type-family + ( concat-span-hom-family-of-types + ( span-span-diagram-type-family S) + ( λ i → map-equiv (e i))) + ( span-span-diagram-type-family T)) + + module _ + (e : equiv-span-diagram-type-family) + where + + equiv-family-equiv-span-diagram-type-family : + (i : I) → + family-span-diagram-type-family S i ≃ + family-span-diagram-type-family T i + equiv-family-equiv-span-diagram-type-family = pr1 e + + map-family-equiv-span-diagram-type-family : + (i : I) → + family-span-diagram-type-family S i → + family-span-diagram-type-family T i + map-family-equiv-span-diagram-type-family i = + map-equiv (equiv-family-equiv-span-diagram-type-family i) + + equiv-span-equiv-span-diagram-type-family : + equiv-span-type-family + ( concat-span-hom-family-of-types + ( span-span-diagram-type-family S) + ( map-family-equiv-span-diagram-type-family)) + ( span-span-diagram-type-family T) + equiv-span-equiv-span-diagram-type-family = pr2 e + + spanning-equiv-equiv-span-diagram-type-family : + spanning-type-span-diagram-type-family S ≃ + spanning-type-span-diagram-type-family T + spanning-equiv-equiv-span-diagram-type-family = + equiv-equiv-span-type-family + ( concat-span-hom-family-of-types + ( span-span-diagram-type-family S) + ( map-family-equiv-span-diagram-type-family)) + ( span-span-diagram-type-family T) + ( equiv-span-equiv-span-diagram-type-family) + + spanning-map-equiv-span-diagram-type-family : + spanning-type-span-diagram-type-family S → + spanning-type-span-diagram-type-family T + spanning-map-equiv-span-diagram-type-family = + map-equiv spanning-equiv-equiv-span-diagram-type-family + + coherence-square-equiv-span-diagram-type-family : + (i : I) → + coherence-square-maps + ( spanning-map-equiv-span-diagram-type-family) + ( map-span-diagram-type-family S i) + ( map-span-diagram-type-family T i) + ( map-family-equiv-span-diagram-type-family i) + coherence-square-equiv-span-diagram-type-family = + triangle-equiv-span-type-family + ( concat-span-hom-family-of-types + ( span-span-diagram-type-family S) + ( map-family-equiv-span-diagram-type-family)) + ( span-span-diagram-type-family T) + ( equiv-span-equiv-span-diagram-type-family) +``` + +### Identity equivalences of spans diagrams on families of types + +```agda +module _ + {l1 l2 l3 : Level} {I : UU l1} {𝒮 : span-diagram-type-family l2 l3 I} + where + + id-equiv-span-diagram-type-family : + equiv-span-diagram-type-family 𝒮 𝒮 + pr1 id-equiv-span-diagram-type-family i = id-equiv + pr1 (pr2 id-equiv-span-diagram-type-family) = id-equiv + pr2 (pr2 id-equiv-span-diagram-type-family) i = refl-htpy +``` + +## See also + +- [Equivalences of spans on families of types](foundation.equivalences-spans-families-of-types.md) diff --git a/src/foundation/equivalences-span-diagrams.lagda.md b/src/foundation/equivalences-span-diagrams.lagda.md new file mode 100644 index 0000000000..b354b23fe6 --- /dev/null +++ b/src/foundation/equivalences-span-diagrams.lagda.md @@ -0,0 +1,321 @@ +# Equivalences of span diagrams + +```agda +module foundation.equivalences-span-diagrams where +``` + +
Imports + +```agda +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.equivalences-arrows +open import foundation.equivalences-spans +open import foundation.fundamental-theorem-of-identity-types +open import foundation.morphisms-span-diagrams +open import foundation.morphisms-spans +open import foundation.operations-spans +open import foundation.propositions +open import foundation.span-diagrams +open import foundation.structure-identity-principle +open import foundation.type-arithmetic-dependent-pair-types +open import foundation.univalence +open import foundation.universe-levels + +open import foundation-core.commuting-squares-of-maps +open import foundation-core.functoriality-dependent-pair-types +open import foundation-core.identity-types +open import foundation-core.torsorial-type-families +``` + +
+ +## Idea + +An {{#concept "equivalence of span diagrams" Agda=equiv-span-diagram}} from a +[span diagram](foundation.span-diagrams.md) `A <-f- S -g-> B` to a span diagram +`C <-h- T -k-> D` consists of [equivalences](foundation-core.equivalences.md) +`u : A ≃ C`, `v : B ≃ D`, and `w : S ≃ T` [equipped](foundation.structure.md) +with two [homotopies](foundation-core.homotopies.md) witnessing that the diagram + +```text + f g + A <----- S -----> B + | | | + u | | w | v + V V V + C <----- T -----> D + h k +``` + +[commutes](foundation-core.commuting-squares-of-maps.md). + +## Definitions + +### The predicate of being an equivalence of span diagrams + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (𝒮 : span-diagram l1 l2 l3) (𝒯 : span-diagram l4 l5 l6) + (f : hom-span-diagram 𝒮 𝒯) + where + + is-equiv-prop-hom-span-diagram : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) + is-equiv-prop-hom-span-diagram = + prod-Prop + ( is-equiv-Prop (map-domain-hom-span-diagram 𝒮 𝒯 f)) + ( prod-Prop + ( is-equiv-Prop (map-codomain-hom-span-diagram 𝒮 𝒯 f)) + ( is-equiv-Prop (spanning-map-hom-span-diagram 𝒮 𝒯 f))) + + is-equiv-hom-span-diagram : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) + is-equiv-hom-span-diagram = type-Prop is-equiv-prop-hom-span-diagram + + is-prop-is-equiv-hom-span-diagram : is-prop is-equiv-hom-span-diagram + is-prop-is-equiv-hom-span-diagram = + is-prop-type-Prop is-equiv-prop-hom-span-diagram +``` + +### Equivalences of span diagrams + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (𝒮 : span-diagram l1 l2 l3) (𝒯 : span-diagram l4 l5 l6) + where + + equiv-span-diagram : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) + equiv-span-diagram = + Σ ( domain-span-diagram 𝒮 ≃ domain-span-diagram 𝒯) + ( λ e → + Σ ( codomain-span-diagram 𝒮 ≃ codomain-span-diagram 𝒯) + ( λ f → + equiv-span + ( concat-span (span-span-diagram 𝒮) (map-equiv e) (map-equiv f)) + ( span-span-diagram 𝒯))) + + module _ + (e : equiv-span-diagram) + where + + equiv-domain-equiv-span-diagram : + domain-span-diagram 𝒮 ≃ domain-span-diagram 𝒯 + equiv-domain-equiv-span-diagram = pr1 e + + map-domain-equiv-span-diagram : + domain-span-diagram 𝒮 → domain-span-diagram 𝒯 + map-domain-equiv-span-diagram = map-equiv equiv-domain-equiv-span-diagram + + is-equiv-map-domain-equiv-span-diagram : + is-equiv map-domain-equiv-span-diagram + is-equiv-map-domain-equiv-span-diagram = + is-equiv-map-equiv equiv-domain-equiv-span-diagram + + equiv-codomain-equiv-span-diagram : + codomain-span-diagram 𝒮 ≃ codomain-span-diagram 𝒯 + equiv-codomain-equiv-span-diagram = pr1 (pr2 e) + + map-codomain-equiv-span-diagram : + codomain-span-diagram 𝒮 → codomain-span-diagram 𝒯 + map-codomain-equiv-span-diagram = + map-equiv equiv-codomain-equiv-span-diagram + + is-equiv-map-codomain-equiv-span-diagram : + is-equiv map-codomain-equiv-span-diagram + is-equiv-map-codomain-equiv-span-diagram = + is-equiv-map-equiv equiv-codomain-equiv-span-diagram + + equiv-span-equiv-span-diagram : + equiv-span + ( concat-span + ( span-span-diagram 𝒮) + ( map-domain-equiv-span-diagram) + ( map-codomain-equiv-span-diagram)) + ( span-span-diagram 𝒯) + equiv-span-equiv-span-diagram = + pr2 (pr2 e) + + spanning-equiv-equiv-span-diagram : + spanning-type-span-diagram 𝒮 ≃ spanning-type-span-diagram 𝒯 + spanning-equiv-equiv-span-diagram = + equiv-equiv-span + ( concat-span + ( span-span-diagram 𝒮) + ( map-domain-equiv-span-diagram) + ( map-codomain-equiv-span-diagram)) + ( span-span-diagram 𝒯) + ( equiv-span-equiv-span-diagram) + + spanning-map-equiv-span-diagram : + spanning-type-span-diagram 𝒮 → spanning-type-span-diagram 𝒯 + spanning-map-equiv-span-diagram = + map-equiv-span + ( concat-span + ( span-span-diagram 𝒮) + ( map-domain-equiv-span-diagram) + ( map-codomain-equiv-span-diagram)) + ( span-span-diagram 𝒯) + ( equiv-span-equiv-span-diagram) + + is-equiv-spanning-map-equiv-span-diagram : + is-equiv spanning-map-equiv-span-diagram + is-equiv-spanning-map-equiv-span-diagram = + is-equiv-equiv-span + ( concat-span + ( span-span-diagram 𝒮) + ( map-domain-equiv-span-diagram) + ( map-codomain-equiv-span-diagram)) + ( span-span-diagram 𝒯) + ( equiv-span-equiv-span-diagram) + + left-square-equiv-span-diagram : + coherence-square-maps + ( spanning-map-equiv-span-diagram) + ( left-map-span-diagram 𝒮) + ( left-map-span-diagram 𝒯) + ( map-domain-equiv-span-diagram) + left-square-equiv-span-diagram = + left-triangle-equiv-span + ( concat-span + ( span-span-diagram 𝒮) + ( map-domain-equiv-span-diagram) + ( map-codomain-equiv-span-diagram)) + ( span-span-diagram 𝒯) + ( equiv-span-equiv-span-diagram) + + equiv-left-arrow-equiv-span-diagram : + equiv-arrow (left-map-span-diagram 𝒮) (left-map-span-diagram 𝒯) + pr1 equiv-left-arrow-equiv-span-diagram = + spanning-equiv-equiv-span-diagram + pr1 (pr2 equiv-left-arrow-equiv-span-diagram) = + equiv-domain-equiv-span-diagram + pr2 (pr2 equiv-left-arrow-equiv-span-diagram) = + left-square-equiv-span-diagram + + right-square-equiv-span-diagram : + coherence-square-maps + ( spanning-map-equiv-span-diagram) + ( right-map-span-diagram 𝒮) + ( right-map-span-diagram 𝒯) + ( map-codomain-equiv-span-diagram) + right-square-equiv-span-diagram = + right-triangle-equiv-span + ( concat-span + ( span-span-diagram 𝒮) + ( map-domain-equiv-span-diagram) + ( map-codomain-equiv-span-diagram)) + ( span-span-diagram 𝒯) + ( equiv-span-equiv-span-diagram) + + equiv-right-arrow-equiv-span-diagram : + equiv-arrow (right-map-span-diagram 𝒮) (right-map-span-diagram 𝒯) + pr1 equiv-right-arrow-equiv-span-diagram = + spanning-equiv-equiv-span-diagram + pr1 (pr2 equiv-right-arrow-equiv-span-diagram) = + equiv-codomain-equiv-span-diagram + pr2 (pr2 equiv-right-arrow-equiv-span-diagram) = + right-square-equiv-span-diagram + + hom-span-equiv-span-diagram : + hom-span + ( concat-span + ( span-span-diagram 𝒮) + ( map-domain-equiv-span-diagram) + ( map-codomain-equiv-span-diagram)) + ( span-span-diagram 𝒯) + hom-span-equiv-span-diagram = + hom-equiv-span + ( concat-span + ( span-span-diagram 𝒮) + ( map-domain-equiv-span-diagram) + ( map-codomain-equiv-span-diagram)) + ( span-span-diagram 𝒯) + ( equiv-span-equiv-span-diagram) + + hom-equiv-span-diagram : hom-span-diagram 𝒮 𝒯 + pr1 hom-equiv-span-diagram = map-domain-equiv-span-diagram + pr1 (pr2 hom-equiv-span-diagram) = map-codomain-equiv-span-diagram + pr2 (pr2 hom-equiv-span-diagram) = hom-span-equiv-span-diagram + + is-equiv-equiv-span-diagram : + is-equiv-hom-span-diagram 𝒮 𝒯 hom-equiv-span-diagram + pr1 is-equiv-equiv-span-diagram = + is-equiv-map-domain-equiv-span-diagram + pr1 (pr2 is-equiv-equiv-span-diagram) = + is-equiv-map-codomain-equiv-span-diagram + pr2 (pr2 is-equiv-equiv-span-diagram) = + is-equiv-spanning-map-equiv-span-diagram + + compute-equiv-span-diagram : + Σ (hom-span-diagram 𝒮 𝒯) (is-equiv-hom-span-diagram 𝒮 𝒯) ≃ + equiv-span-diagram + compute-equiv-span-diagram = + ( equiv-tot + ( λ e → + ( equiv-tot + ( λ f → + compute-equiv-span + ( concat-span + ( span-span-diagram 𝒮) + ( map-equiv e) + ( map-equiv f)) + ( span-span-diagram 𝒯))) ∘e + ( interchange-Σ-Σ _))) ∘e + ( interchange-Σ-Σ _) +``` + +### The identity equivalence of span diagrams + +```agda +module _ + {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3) + where + + id-equiv-span-diagram : equiv-span-diagram 𝒮 𝒮 + pr1 id-equiv-span-diagram = id-equiv + pr1 (pr2 id-equiv-span-diagram) = id-equiv + pr2 (pr2 id-equiv-span-diagram) = id-equiv-span (span-span-diagram 𝒮) +``` + +## Properties + +### Extensionality of span diagrams + +Equality of span diagrams is equivalent to equivalences of span diagrams. + +```agda +module _ + {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3) + where + + equiv-eq-span-diagram : + (𝒯 : span-diagram l1 l2 l3) → 𝒮 = 𝒯 → equiv-span-diagram 𝒮 𝒯 + equiv-eq-span-diagram 𝒯 refl = id-equiv-span-diagram 𝒮 + + is-torsorial-equiv-span-diagram : + is-torsorial (equiv-span-diagram 𝒮) + is-torsorial-equiv-span-diagram = + is-torsorial-Eq-structure + ( is-torsorial-equiv (domain-span-diagram 𝒮)) + ( domain-span-diagram 𝒮 , id-equiv) + ( is-torsorial-Eq-structure + ( is-torsorial-equiv (codomain-span-diagram 𝒮)) + ( codomain-span-diagram 𝒮 , id-equiv) + ( is-torsorial-equiv-span (span-span-diagram 𝒮))) + + is-equiv-equiv-eq-span-diagram : + (𝒯 : span-diagram l1 l2 l3) → is-equiv (equiv-eq-span-diagram 𝒯) + is-equiv-equiv-eq-span-diagram = + fundamental-theorem-id is-torsorial-equiv-span-diagram equiv-eq-span-diagram + + extensionality-span-diagram : + (𝒯 : span-diagram l1 l2 l3) → (𝒮 = 𝒯) ≃ equiv-span-diagram 𝒮 𝒯 + pr1 (extensionality-span-diagram 𝒯) = equiv-eq-span-diagram 𝒯 + pr2 (extensionality-span-diagram 𝒯) = is-equiv-equiv-eq-span-diagram 𝒯 + + eq-equiv-span-diagram : + (𝒯 : span-diagram l1 l2 l3) → equiv-span-diagram 𝒮 𝒯 → 𝒮 = 𝒯 + eq-equiv-span-diagram 𝒯 = map-inv-equiv (extensionality-span-diagram 𝒯) +``` diff --git a/src/foundation/equivalences-spans-families-of-types.lagda.md b/src/foundation/equivalences-spans-families-of-types.lagda.md new file mode 100644 index 0000000000..0d6c5ebc6c --- /dev/null +++ b/src/foundation/equivalences-spans-families-of-types.lagda.md @@ -0,0 +1,158 @@ +# Equivalences of spans of families of types + +```agda +module foundation.equivalences-spans-families-of-types where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.equality-dependent-function-types +open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopies +open import foundation.homotopy-induction +open import foundation.identity-types +open import foundation.morphisms-spans-families-of-types +open import foundation.spans-families-of-types +open import foundation.structure-identity-principle +open import foundation.univalence +open import foundation.universe-levels + +open import foundation-core.commuting-triangles-of-maps +open import foundation-core.equivalences +open import foundation-core.torsorial-type-families +``` + +
+ +## Idea + +An +{{#concept "equivalence of spans on a family of types" Agda=equiv-span-type-family}} +from a [span](foundation.spans-families-of-types.md) `s` on `A : I → 𝒰` to a +span `t` on `A` consists of an [equivalence](foundation-core.equivalences.md) +`e : S ≃ T` [equipped](foundation.structure.md) with a family of +[homotopies](foundation-core.homotopies.md) witnessing that the triangle + +```text + e + S ----> T + \ / + \ / + V V + Aᵢ +``` + +[commutes](foundation.commuting-triangles-of-maps.md) for each `i : I`. + +## Definitions + +### Equivalences of spans of families of types + +```agda +module _ + {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} + (S : span-type-family l3 A) (T : span-type-family l4 A) + where + + equiv-span-type-family : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + equiv-span-type-family = + Σ ( spanning-type-span-type-family S ≃ + spanning-type-span-type-family T) + ( λ e → + (i : I) → + coherence-triangle-maps + ( map-span-type-family S i) + ( map-span-type-family T i) + ( map-equiv e)) + + module _ + (e : equiv-span-type-family) + where + + equiv-equiv-span-type-family : + spanning-type-span-type-family S ≃ + spanning-type-span-type-family T + equiv-equiv-span-type-family = pr1 e + + map-equiv-span-type-family : + spanning-type-span-type-family S → + spanning-type-span-type-family T + map-equiv-span-type-family = map-equiv equiv-equiv-span-type-family + + is-equiv-equiv-span-type-family : + is-equiv map-equiv-span-type-family + is-equiv-equiv-span-type-family = + is-equiv-map-equiv equiv-equiv-span-type-family + + triangle-equiv-span-type-family : + (i : I) → + coherence-triangle-maps + ( map-span-type-family S i) + ( map-span-type-family T i) + ( map-equiv-span-type-family) + triangle-equiv-span-type-family = pr2 e + + hom-equiv-span-type-family : hom-span-type-family S T + pr1 hom-equiv-span-type-family = map-equiv-span-type-family + pr2 hom-equiv-span-type-family = triangle-equiv-span-type-family +``` + +### Identity equivalences of spans of families of types + +```agda +module _ + {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} + {S : span-type-family l3 A} + where + + id-equiv-span-type-family : equiv-span-type-family S S + pr1 id-equiv-span-type-family = id-equiv + pr2 id-equiv-span-type-family i = refl-htpy +``` + +## Properties + +### Characterizing the identity type of the type of spans of families of types + +```agda +module _ + {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} (S : span-type-family l3 A) + where + + equiv-eq-span-type-family : + (T : span-type-family l3 A) → S = T → equiv-span-type-family S T + equiv-eq-span-type-family .S refl = id-equiv-span-type-family + + is-torsorial-equiv-span-type-family : + is-torsorial (equiv-span-type-family S) + is-torsorial-equiv-span-type-family = + is-torsorial-Eq-structure + ( is-torsorial-equiv _) + ( spanning-type-span-type-family S , id-equiv) + ( is-torsorial-Eq-Π (λ i → is-torsorial-htpy _)) + + is-equiv-equiv-eq-span-type-family : + (T : span-type-family l3 A) → is-equiv (equiv-eq-span-type-family T) + is-equiv-equiv-eq-span-type-family = + fundamental-theorem-id + ( is-torsorial-equiv-span-type-family) + ( equiv-eq-span-type-family) + + extensionality-span-type-family : + (T : span-type-family l3 A) → (S = T) ≃ equiv-span-type-family S T + pr1 (extensionality-span-type-family T) = + equiv-eq-span-type-family T + pr2 (extensionality-span-type-family T) = + is-equiv-equiv-eq-span-type-family T + + eq-equiv-span-type-family : + (T : span-type-family l3 A) → equiv-span-type-family S T → S = T + eq-equiv-span-type-family T = + map-inv-equiv (extensionality-span-type-family T) +``` + +## See also + +- [Equivalences of span diagrams on families of types](foundation.equivalences-span-diagrams-families-of-types.md) diff --git a/src/foundation/equivalences-spans.lagda.md b/src/foundation/equivalences-spans.lagda.md new file mode 100644 index 0000000000..4e804c318a --- /dev/null +++ b/src/foundation/equivalences-spans.lagda.md @@ -0,0 +1,171 @@ +# Equivalences of spans + +```agda +module foundation.equivalences-spans where +``` + +
Imports + +```agda +open import foundation.cartesian-product-types +open import foundation.commuting-squares-of-maps +open import foundation.dependent-pair-types +open import foundation.functoriality-dependent-pair-types +open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopy-induction +open import foundation.morphisms-spans +open import foundation.spans +open import foundation.structure-identity-principle +open import foundation.type-arithmetic-dependent-pair-types +open import foundation.univalence +open import foundation.universe-levels + +open import foundation-core.commuting-triangles-of-maps +open import foundation-core.equivalences +open import foundation-core.function-types +open import foundation-core.homotopies +open import foundation-core.identity-types +open import foundation-core.operations-spans +open import foundation-core.torsorial-type-families +``` + +
+ +## Idea + +A {{#concept "equivalence of spans" Agda=equiv-span}} from a +[span](foundation.spans.md) `A <-f- S -g-> B` to a span `A <-h- T -k-> B` +consists of an [equivalence](foundation-core.equivalences.md) `w : S ≃ T` +[equipped](foundation.structure.md) with two +[homotopies](foundation-core.homotopies.md) witnessing that the diagram + +```text + S + / | \ + f / | \ h + ∨ | ∨ + A |w B + ∧ | ∧ + h \ | / k + \ ∨ / + T +``` + +[commutes](foundation.commuting-triangles-of-maps.md). + +## Definitions + +### The predicate of being an equivalence of spans + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} + (s : span l3 A B) (t : span l4 A B) + where + + is-equiv-hom-span : hom-span s t → UU (l3 ⊔ l4) + is-equiv-hom-span f = is-equiv (map-hom-span s t f) +``` + +### Equivalences of spans + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} + (s : span l3 A B) (t : span l4 A B) + where + + left-coherence-equiv-span : + (spanning-type-span s ≃ spanning-type-span t) → UU (l1 ⊔ l3) + left-coherence-equiv-span e = + left-coherence-hom-span s t (map-equiv e) + + right-coherence-equiv-span : + (spanning-type-span s ≃ spanning-type-span t) → UU (l2 ⊔ l3) + right-coherence-equiv-span e = + right-coherence-hom-span s t (map-equiv e) + + coherence-equiv-span : + (spanning-type-span s ≃ spanning-type-span t) → UU (l1 ⊔ l2 ⊔ l3) + coherence-equiv-span e = coherence-hom-span s t (map-equiv e) + + equiv-span : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + equiv-span = + Σ ( spanning-type-span s ≃ spanning-type-span t) coherence-equiv-span + + equiv-equiv-span : equiv-span → spanning-type-span s ≃ spanning-type-span t + equiv-equiv-span = pr1 + + map-equiv-span : equiv-span → spanning-type-span s → spanning-type-span t + map-equiv-span e = map-equiv (equiv-equiv-span e) + + left-triangle-equiv-span : + (e : equiv-span) → left-coherence-hom-span s t (map-equiv-span e) + left-triangle-equiv-span e = pr1 (pr2 e) + + right-triangle-equiv-span : + (e : equiv-span) → right-coherence-hom-span s t (map-equiv-span e) + right-triangle-equiv-span e = pr2 (pr2 e) + + hom-equiv-span : equiv-span → hom-span s t + pr1 (hom-equiv-span e) = map-equiv-span e + pr1 (pr2 (hom-equiv-span e)) = left-triangle-equiv-span e + pr2 (pr2 (hom-equiv-span e)) = right-triangle-equiv-span e + + is-equiv-equiv-span : + (e : equiv-span) → is-equiv-hom-span s t (hom-equiv-span e) + is-equiv-equiv-span e = is-equiv-map-equiv (equiv-equiv-span e) + + compute-equiv-span : + Σ (hom-span s t) (is-equiv-hom-span s t) ≃ equiv-span + compute-equiv-span = equiv-right-swap-Σ +``` + +### The identity equivalence on a span + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} + where + + id-equiv-span : (s : span l3 A B) → equiv-span s s + pr1 (id-equiv-span s) = id-equiv + pr1 (pr2 (id-equiv-span s)) = refl-htpy + pr2 (pr2 (id-equiv-span s)) = refl-htpy +``` + +## Properties + +### Extensionality of spans + +Equality of spans is equivalent to equivalences of spans. + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} + where + + equiv-eq-span : (s t : span l3 A B) → s = t → equiv-span s t + equiv-eq-span s .s refl = id-equiv-span s + + is-torsorial-equiv-span : (s : span l3 A B) → is-torsorial (equiv-span s) + is-torsorial-equiv-span s = + is-torsorial-Eq-structure + ( is-torsorial-equiv (spanning-type-span s)) + ( spanning-type-span s , id-equiv) + ( is-torsorial-Eq-structure + ( is-torsorial-htpy (left-map-span s)) + ( left-map-span s , refl-htpy) + ( is-torsorial-htpy (right-map-span s))) + + is-equiv-equiv-eq-span : (c d : span l3 A B) → is-equiv (equiv-eq-span c d) + is-equiv-equiv-eq-span c = + fundamental-theorem-id (is-torsorial-equiv-span c) (equiv-eq-span c) + + extensionality-span : (c d : span l3 A B) → (c = d) ≃ (equiv-span c d) + pr1 (extensionality-span c d) = equiv-eq-span c d + pr2 (extensionality-span c d) = is-equiv-equiv-eq-span c d + + eq-equiv-span : (c d : span l3 A B) → equiv-span c d → c = d + eq-equiv-span c d = map-inv-equiv (extensionality-span c d) +``` diff --git a/src/foundation/equivalences.lagda.md b/src/foundation/equivalences.lagda.md index 0923096b18..e3e695b440 100644 --- a/src/foundation/equivalences.lagda.md +++ b/src/foundation/equivalences.lagda.md @@ -10,7 +10,7 @@ open import foundation-core.equivalences public ```agda open import foundation.action-on-identifications-functions -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.equivalence-extensionality open import foundation.functoriality-fibers-of-maps @@ -29,6 +29,7 @@ open import foundation-core.function-extensionality open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies +open import foundation-core.injective-maps open import foundation-core.propositions open import foundation-core.pullbacks open import foundation-core.retractions @@ -53,9 +54,12 @@ module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where + is-emb-equiv : (e : A ≃ B) → is-emb (map-equiv e) + is-emb-equiv e = is-emb-is-equiv (is-equiv-map-equiv e) + emb-equiv : (A ≃ B) → (A ↪ B) pr1 (emb-equiv e) = map-equiv e - pr2 (emb-equiv e) = is-emb-is-equiv (is-equiv-map-equiv e) + pr2 (emb-equiv e) = is-emb-equiv e ``` ### Transposing equalities along equivalences @@ -358,6 +362,10 @@ module _ is-emb (map-equiv {A = A} {B = B}) is-emb-map-equiv = is-emb-inclusion-subtype is-equiv-Prop + is-injective-map-equiv : + is-injective (map-equiv {A = A} {B = B}) + is-injective-map-equiv = is-injective-is-emb is-emb-map-equiv + emb-map-equiv : (A ≃ B) ↪ (A → B) pr1 emb-map-equiv = map-equiv pr2 emb-map-equiv = is-emb-map-equiv diff --git a/src/foundation/fiber-inclusions.lagda.md b/src/foundation/fiber-inclusions.lagda.md index a53c974f45..bd3ad4bed8 100644 --- a/src/foundation/fiber-inclusions.lagda.md +++ b/src/foundation/fiber-inclusions.lagda.md @@ -8,7 +8,7 @@ module foundation.fiber-inclusions where ```agda open import foundation.0-maps -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.faithful-maps open import foundation.fibers-of-maps diff --git a/src/foundation/fibered-maps.lagda.md b/src/foundation/fibered-maps.lagda.md index 73e852a3ea..986e91161f 100644 --- a/src/foundation/fibered-maps.lagda.md +++ b/src/foundation/fibered-maps.lagda.md @@ -7,7 +7,7 @@ module foundation.fibered-maps where
Imports ```agda -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopy-induction diff --git a/src/foundation/fibers-of-maps.lagda.md b/src/foundation/fibers-of-maps.lagda.md index e77588d386..17802bb955 100644 --- a/src/foundation/fibers-of-maps.lagda.md +++ b/src/foundation/fibers-of-maps.lagda.md @@ -10,7 +10,7 @@ open import foundation-core.fibers-of-maps public ```agda open import foundation.action-on-identifications-functions -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-arithmetic-unit-type diff --git a/src/foundation/function-types.lagda.md b/src/foundation/function-types.lagda.md index 752a2ebcf2..b1b6f7136f 100644 --- a/src/foundation/function-types.lagda.md +++ b/src/foundation/function-types.lagda.md @@ -30,6 +30,22 @@ open import foundation-core.transport-along-identifications ### Transport in a family of function types +Consider two type families `B` and `C` over `A`, an identification `p : x = y` +in `A` and two functions + +```text + f : B x → C x + g : B y → C y. +``` + +Then the type of dependent identifications from `f` to `g` over `p` can be +computed as + +```text + ((b : B x) → tr C p (f b) = g (tr B p b)) + ≃ dependent-identification (x ↦ B x → C x) f g. +``` + ```agda module _ {l1 l2 l3 : Level} {A : UU l1} {x y : A} (B : A → UU l2) (C : A → UU l3) @@ -43,18 +59,41 @@ module _ compute-dependent-identification-function-type : (p : x = y) (f : B x → C x) (g : B y → C y) → ((b : B x) → tr C p (f b) = g (tr B p b)) ≃ - (tr (λ a → B a → C a) p f = g) + dependent-identification (λ a → B a → C a) p f g compute-dependent-identification-function-type refl f g = inv-equiv equiv-funext map-compute-dependent-identification-function-type : (p : x = y) (f : B x → C x) (g : B y → C y) → ((b : B x) → tr C p (f b) = g (tr B p b)) → - (tr (λ a → B a → C a) p f = g) + dependent-identification (λ a → B a → C a) p f g map-compute-dependent-identification-function-type p f g = map-equiv (compute-dependent-identification-function-type p f g) ``` +### Transport in a family of function types with fixed codomain + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {x y : A} (B : A → UU l2) (C : UU l3) + where + + compute-dependent-identification-function-type-fixed-codomain : + (p : x = y) (f : B x → C) (g : B y → C) → + ((b : B x) → f b = g (tr B p b)) ≃ + dependent-identification (λ a → B a → C) p f g + compute-dependent-identification-function-type-fixed-codomain refl f g = + inv-equiv equiv-funext + + map-compute-dependent-identification-function-type-fixed-codomain : + (p : x = y) (f : B x → C) (g : B y → C) → + ((b : B x) → f b = g (tr B p b)) → + dependent-identification (λ a → B a → C) p f g + map-compute-dependent-identification-function-type-fixed-codomain p f g = + map-equiv + ( compute-dependent-identification-function-type-fixed-codomain p f g) +``` + ### Relation between `compute-dependent-identification-function-type` and `preserves-tr` ```agda @@ -148,19 +187,6 @@ module _ ( eq-htpy-refl-htpy (h (i s)))) ``` -### Composing families of functions - -```agda -module _ - {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} - {D : A → UU l4} - where - - dependent-comp : - ((a : A) → C a → D a) → ((a : A) → B a → C a) → (a : A) → B a → D a - dependent-comp g f a b = g a (f a b) -``` - ## See also ### Table of files about function types, composition, and equivalences diff --git a/src/foundation/functoriality-coproduct-types.lagda.md b/src/foundation/functoriality-coproduct-types.lagda.md index 342c95baa2..27ad94296a 100644 --- a/src/foundation/functoriality-coproduct-types.lagda.md +++ b/src/foundation/functoriality-coproduct-types.lagda.md @@ -297,17 +297,17 @@ module _ (x : A) (y : B) → map-equiv f (inl x) ≠ inr y equiv-coproduct-induce-equiv-disjoint f g p x y q = neq-inr-inl - ( is-injective-map-equiv f - ( ( p ( map-equiv (inv-equiv g) y)) ∙ - ( ap (λ z → inr (map-equiv z y)) (right-inverse-law-equiv g)) ∙ - ( inv q))) + ( is-injective-equiv f + ( ( p (map-equiv (inv-equiv g) y) ∙ + ( ( ap (λ z → inr (map-equiv z y)) (right-inverse-law-equiv g)) ∙ + ( inv q))))) inv-commutative-square-inr : (f : (A + B) ≃ (A + B)) (g : B ≃ B) (p : (b : B) → map-equiv f (inr b) = inr (map-equiv g b)) → (b : B) → map-inv-equiv f (inr b) = inr (map-inv-equiv g b) inv-commutative-square-inr f g p b = - is-injective-map-equiv f + is-injective-equiv f ( ( ap (λ z → map-equiv z (inr b)) (right-inverse-law-equiv f)) ∙ ( inv (ap (λ z → inr (map-equiv z b)) (right-inverse-law-equiv g))) ∙ ( inv (p (map-inv-equiv g b)))) diff --git a/src/foundation/functoriality-dependent-pair-types.lagda.md b/src/foundation/functoriality-dependent-pair-types.lagda.md index cdf87ea21b..cee7cc74a3 100644 --- a/src/foundation/functoriality-dependent-pair-types.lagda.md +++ b/src/foundation/functoriality-dependent-pair-types.lagda.md @@ -10,7 +10,7 @@ open import foundation-core.functoriality-dependent-pair-types public ```agda open import foundation.action-on-identifications-functions -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-homotopies open import foundation.dependent-pair-types open import foundation.type-arithmetic-dependent-pair-types @@ -526,7 +526,7 @@ module _ map-inv-equiv (equiv-tot e) ~ map-equiv (equiv-tot (λ x → inv-equiv (e x))) compute-inv-equiv-tot e (a , c) = - is-injective-map-equiv + is-injective-equiv ( equiv-tot e) ( ( is-section-map-inv-equiv (equiv-tot e) (a , c)) ∙ ( eq-pair-Σ refl (inv (is-section-map-inv-equiv (e a) c)))) diff --git a/src/foundation/functoriality-fibers-of-maps.lagda.md b/src/foundation/functoriality-fibers-of-maps.lagda.md index 1430ba9386..730d05b084 100644 --- a/src/foundation/functoriality-fibers-of-maps.lagda.md +++ b/src/foundation/functoriality-fibers-of-maps.lagda.md @@ -9,7 +9,7 @@ module foundation.functoriality-fibers-of-maps where ```agda open import foundation.action-on-identifications-functions open import foundation.commuting-squares-of-homotopies -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.morphisms-arrows open import foundation.universe-levels diff --git a/src/foundation/functoriality-pullbacks.lagda.md b/src/foundation/functoriality-pullbacks.lagda.md index c8c6533b7c..7d58bafd22 100644 --- a/src/foundation/functoriality-pullbacks.lagda.md +++ b/src/foundation/functoriality-pullbacks.lagda.md @@ -8,9 +8,9 @@ module foundation.functoriality-pullbacks where ```agda open import foundation.action-on-identifications-functions -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types -open import foundation.morphisms-cospans +open import foundation.morphisms-cospan-diagrams open import foundation.universe-levels open import foundation-core.equivalences @@ -37,7 +37,8 @@ module _ where map-standard-pullback : - hom-cospan f' g' f g → standard-pullback f' g' → standard-pullback f g + hom-cospan-diagram f' g' f g → + standard-pullback f' g' → standard-pullback f g pr1 (map-standard-pullback (hA , _) (a' , _)) = hA a' pr1 (pr2 (map-standard-pullback (hA , hB , _) (a' , b' , _))) = hB b' pr2 (pr2 (map-standard-pullback (hA , hB , hX , HA , HB) (a' , b' , p'))) = @@ -47,8 +48,8 @@ module _ {l4 l4' : Level} {C : UU l4} {C' : UU l4'} → (c : cone f g C) (c' : cone f' g' C') → is-pullback f g c → is-pullback f' g' c' → - hom-cospan f' g' f g → C' → C - map-is-pullback c c' is-pb-c _ h x = + hom-cospan-diagram f' g' f g → C' → C + map-is-pullback c c' is-pb-c is-pb-c' h x = map-inv-is-equiv is-pb-c (map-standard-pullback h (gap f' g' c' x)) ``` diff --git a/src/foundation/involutions.lagda.md b/src/foundation/involutions.lagda.md index 6ab1731b29..95839414db 100644 --- a/src/foundation/involutions.lagda.md +++ b/src/foundation/involutions.lagda.md @@ -99,7 +99,7 @@ htpy-own-inverse-is-involution : {l : Level} {A : UU l} {f : Aut A} → is-involution-aut f → map-inv-equiv f ~ map-equiv f htpy-own-inverse-is-involution {f = f} is-involution-f x = - is-injective-map-equiv f + is-injective-equiv f ( htpy-eq-equiv (right-inverse-law-equiv f) x ∙ inv (is-involution-f x)) diff --git a/src/foundation/kernel-span-diagrams-of-maps.lagda.md b/src/foundation/kernel-span-diagrams-of-maps.lagda.md new file mode 100644 index 0000000000..37d56efd8d --- /dev/null +++ b/src/foundation/kernel-span-diagrams-of-maps.lagda.md @@ -0,0 +1,74 @@ +# Kernel span diagrams of maps + +```agda +module foundation.kernel-span-diagrams-of-maps where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.span-diagrams +open import foundation.spans +open import foundation.universe-levels + +open import foundation-core.function-types +open import foundation-core.identity-types +``` + +
+ +## Idea + +Consider a map `f : A → B`. The +{{#concept "kernel span diagram" Disambiguation="map" Agda=kernel-span-diagram}} +of `f` is the [span diagram](foundation.span-diagrams.md) + +```text + pr1 pr1 ∘ pr2 + A <----- Σ (x y : A), f x = f y -----------> A. +``` + +We call this the kernel span diagram, since the pair `(pr1 , pr1 ∘ pr2)` is +often called the kernel pair of a map. + +## Definitions + +### Kernel span diagrams of maps + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + spanning-type-kernel-span : UU (l1 ⊔ l2) + spanning-type-kernel-span = + Σ A (λ x → Σ A (λ y → f x = f y)) + + left-map-kernel-span : + spanning-type-kernel-span → A + left-map-kernel-span = pr1 + + right-map-kernel-span : + spanning-type-kernel-span → A + right-map-kernel-span = pr1 ∘ pr2 + + kernel-span : span (l1 ⊔ l2) A A + pr1 kernel-span = + spanning-type-kernel-span + pr1 (pr2 kernel-span) = + left-map-kernel-span + pr2 (pr2 kernel-span) = + right-map-kernel-span + + domain-kernel-span-diagram : UU l1 + domain-kernel-span-diagram = A + + codomain-kernel-span-diagram : UU l1 + codomain-kernel-span-diagram = A + + kernel-span-diagram : span-diagram l1 l1 (l1 ⊔ l2) + pr1 kernel-span-diagram = domain-kernel-span-diagram + pr1 (pr2 kernel-span-diagram) = codomain-kernel-span-diagram + pr2 (pr2 kernel-span-diagram) = kernel-span +``` diff --git a/src/foundation/morphisms-arrows.lagda.md b/src/foundation/morphisms-arrows.lagda.md index dc339db174..6d5efae800 100644 --- a/src/foundation/morphisms-arrows.lagda.md +++ b/src/foundation/morphisms-arrows.lagda.md @@ -34,8 +34,9 @@ open import foundation-core.whiskering-homotopies ## Idea -A **morphism of arrows** from a function `f : A → B` to a function `g : X → Y` -is a triple `(i , j , H)` consisting of maps `i : A → X` and `j : B → Y` and a +A {{#concept "morphism of arrows" Agda=hom-arrow}} from a function `f : A → B` +to a function `g : X → Y` is a [triple](foundation.dependent-pair-types.md) +`(i , j , H)` consisting of maps `i : A → X` and `j : B → Y` and a [homotopy](foundation-core.homotopies.md) `H : j ∘ f ~ g ∘ i` witnessing that the square @@ -62,8 +63,11 @@ module _ (f : A → B) (g : X → Y) where + coherence-hom-arrow : (A → X) → (B → Y) → UU (l1 ⊔ l4) + coherence-hom-arrow i = coherence-square-maps i f g + hom-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) - hom-arrow = Σ (A → X) (λ i → Σ (B → Y) (coherence-square-maps i f g)) + hom-arrow = Σ (A → X) (λ i → Σ (B → Y) (coherence-hom-arrow i)) map-domain-hom-arrow : hom-arrow → A → X map-domain-hom-arrow = pr1 @@ -73,31 +77,81 @@ module _ coh-hom-arrow : (h : hom-arrow) → - coherence-square-maps - ( map-domain-hom-arrow h) - ( f) - ( g) - ( map-codomain-hom-arrow h) + coherence-hom-arrow (map-domain-hom-arrow h) (map-codomain-hom-arrow h) coh-hom-arrow = pr2 ∘ pr2 ``` ### Transposing morphisms of arrows +The {{#concept "transposition" Disambiguation="morphism of arrows"}} of a +morphism of arrows + +```text + i + A -----> X + | | + f | | g + V V + B -----> Y + j +``` + +is the morphism of arrows + +```text + f + A -----> B + | | + i | | j + V V + X -----> Y. + g +``` + ```agda module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} (f : A → B) (g : X → Y) (α : hom-arrow f g) where + map-domain-transpose-hom-arrow : A → B + map-domain-transpose-hom-arrow = f + + map-codomain-transpose-hom-arrow : X → Y + map-codomain-transpose-hom-arrow = g + + coh-transpose-hom-arrow : + coherence-hom-arrow + ( map-domain-hom-arrow f g α) + ( map-codomain-hom-arrow f g α) + ( map-domain-transpose-hom-arrow) + ( map-codomain-transpose-hom-arrow) + coh-transpose-hom-arrow = + inv-htpy (coh-hom-arrow f g α) + transpose-hom-arrow : hom-arrow (map-domain-hom-arrow f g α) (map-codomain-hom-arrow f g α) - pr1 transpose-hom-arrow = f - pr1 (pr2 transpose-hom-arrow) = g - pr2 (pr2 transpose-hom-arrow) = inv-htpy (coh-hom-arrow f g α) + pr1 transpose-hom-arrow = map-domain-transpose-hom-arrow + pr1 (pr2 transpose-hom-arrow) = map-codomain-transpose-hom-arrow + pr2 (pr2 transpose-hom-arrow) = coh-transpose-hom-arrow ``` ### The identity morphism of arrows +The identity morphism of arrows is defined as + +```text + id + A -----> A + | | + f | | f + V V + B -----> B + id +``` + +where the homotopy `id ∘ f ~ f ∘ id` is the reflexivity homotopy. + ```agda module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} @@ -124,7 +178,18 @@ Consider a commuting diagram of the form ``` Then the outer rectangle commutes by horizontal pasting of commuting squares of -maps. +maps. The {{#concept "composition" Disambiguation="morphism of arrows"}} of +`β : g → h` with `α : f → g` is therefore defined to be + +```text + β₀ ∘ α₀ + A ----------> U + | | + f | α □ β | h + V V + B ----------> V. + β₁ ∘ α₁ +``` ```agda module _ @@ -142,10 +207,8 @@ module _ map-codomain-hom-arrow g h b ∘ map-codomain-hom-arrow f g a coh-comp-hom-arrow : - coherence-square-maps + coherence-hom-arrow f h ( map-domain-comp-hom-arrow) - ( f) - ( h) ( map-codomain-comp-hom-arrow) coh-comp-hom-arrow = pasting-horizontal-coherence-square-maps @@ -170,9 +233,9 @@ module _ ### Homotopies of morphisms of arrows -A **homotopy of morphisms of arrows** from `(i , j , H)` to `(i' , j' , H')` is -a triple `(I , J , K)` consisting of homotopies `I : i ~ i'` and `J : j ~ j'` -and a homotopy `K` witnessing that the +A {{#concept "homotopy of morphisms of arrows"}} from `(i , j , H)` to +`(i' , j' , H')` is a triple `(I , J , K)` consisting of homotopies `I : i ~ i'` +and `J : j ~ j'` and a homotopy `K` witnessing that the [square of homotopies](foundation.commuting-squares-of-homotopies.md) ```text @@ -587,6 +650,7 @@ module _ ## See also +- [Equivalences of arrows](foundation.equivalences-arrows.md) - [Morphisms of twisted arrows](foundation.morphisms-twisted-arrows.md). - [Fibered maps](foundation.fibered-maps.md) for the same concept under a different name. diff --git a/src/foundation/morphisms-cospan-diagrams.lagda.md b/src/foundation/morphisms-cospan-diagrams.lagda.md new file mode 100644 index 0000000000..f5a8a9339a --- /dev/null +++ b/src/foundation/morphisms-cospan-diagrams.lagda.md @@ -0,0 +1,145 @@ +# Morphisms of cospan diagrams + +```agda +module foundation.morphisms-cospan-diagrams where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.universe-levels + +open import foundation-core.cartesian-product-types +open import foundation-core.function-types +open import foundation-core.homotopies +``` + +
+ +## Idea + +A {{#concept "morphism of cospan diagrams" Agda=hom-cospan-diagram}} is a +commuting diagram of the form + +```text + A -----> X <----- B + | | | + | | | + V V V + A' ----> X' <---- B'. +``` + +## Definitions + +### Morphisms of cospan diagrams + +```agda +hom-cospan-diagram : + {l1 l2 l3 l1' l2' l3' : Level} + {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) + {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} (f' : A' → X') (g' : B' → X') → + UU (l1 ⊔ l2 ⊔ l3 ⊔ l1' ⊔ l2' ⊔ l3') +hom-cospan-diagram {A = A} {B} {X} f g {A'} {B'} {X'} f' g' = + Σ ( A → A') + ( λ hA → + Σ ( B → B') + ( λ hB → + Σ ( X → X') + ( λ hX → (f' ∘ hA ~ hX ∘ f) × (g' ∘ hB ~ hX ∘ g)))) +``` + +### Identity morphisms of cospan diagrams + +```agda +id-hom-cospan-diagram : + {l1 l2 l3 l1' l2' l3' : Level} + {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) → + hom-cospan-diagram f g f g +pr1 (id-hom-cospan-diagram f g) = id +pr1 (pr2 (id-hom-cospan-diagram f g)) = id +pr1 (pr2 (pr2 (id-hom-cospan-diagram f g))) = id +pr1 (pr2 (pr2 (pr2 (id-hom-cospan-diagram f g)))) = refl-htpy +pr2 (pr2 (pr2 (pr2 (id-hom-cospan-diagram f g)))) = refl-htpy +``` + +### Rotating cospan diagrams of cospan diagrams + +```agda +cospan-hom-cospan-diagram-rotate : + {l1 l2 l3 l1' l2' l3' l1'' l2'' l3'' : Level} + {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) + {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} (f' : A' → X') (g' : B' → X') + {A'' : UU l1''} {B'' : UU l2''} {X'' : UU l3''} + (f'' : A'' → X'') (g'' : B'' → X'') + (h : hom-cospan-diagram f' g' f g) (h' : hom-cospan-diagram f'' g'' f g) → + hom-cospan-diagram (pr1 h) (pr1 h') (pr1 (pr2 (pr2 h))) (pr1 (pr2 (pr2 h'))) +pr1 + ( cospan-hom-cospan-diagram-rotate f g f' g' f'' g'' + ( hA , hB , hX , HA , HB) + ( hA' , hB' , hX' , HA' , HB')) = f' +pr1 + ( pr2 + ( cospan-hom-cospan-diagram-rotate f g f' g' f'' g'' + ( hA , hB , hX , HA , HB) + ( hA' , hB' , hX' , HA' , HB'))) = f'' +pr1 + ( pr2 + ( pr2 + ( cospan-hom-cospan-diagram-rotate f g f' g' f'' g'' + ( hA , hB , hX , HA , HB) + ( hA' , hB' , hX' , HA' , HB')))) = f +pr1 + ( pr2 + ( pr2 + ( pr2 + ( cospan-hom-cospan-diagram-rotate f g f' g' f'' g'' + ( hA , hB , hX , HA , HB) + ( hA' , hB' , hX' , HA' , HB'))))) = inv-htpy HA +pr2 + ( pr2 + ( pr2 + ( pr2 + ( cospan-hom-cospan-diagram-rotate f g f' g' f'' g'' + ( hA , hB , hX , HA , HB) + ( hA' , hB' , hX' , HA' , HB'))))) = inv-htpy HA' + +cospan-hom-cospan-diagram-rotate' : + {l1 l2 l3 l1' l2' l3' l1'' l2'' l3'' : Level} + {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) + {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} (f' : A' → X') (g' : B' → X') + {A'' : UU l1''} {B'' : UU l2''} {X'' : UU l3''} + (f'' : A'' → X'') (g'' : B'' → X'') + (h : hom-cospan-diagram f' g' f g) (h' : hom-cospan-diagram f'' g'' f g) → + hom-cospan-diagram + (pr1 (pr2 h)) (pr1 (pr2 h')) (pr1 (pr2 (pr2 h))) (pr1 (pr2 (pr2 h'))) +pr1 + ( cospan-hom-cospan-diagram-rotate' f g f' g' f'' g'' + ( hA , hB , hX , HA , HB) + ( hA' , hB' , hX' , HA' , HB')) = g' +pr1 + ( pr2 + ( cospan-hom-cospan-diagram-rotate' f g f' g' f'' g'' + ( hA , hB , hX , HA , HB) + ( hA' , hB' , hX' , HA' , HB'))) = g'' +pr1 + ( pr2 + ( pr2 + ( cospan-hom-cospan-diagram-rotate' f g f' g' f'' g'' + ( hA , hB , hX , HA , HB) + ( hA' , hB' , hX' , HA' , HB')))) = g +pr1 + ( pr2 + ( pr2 + ( pr2 + ( cospan-hom-cospan-diagram-rotate' f g f' g' f'' g'' + ( hA , hB , hX , HA , HB) + ( hA' , hB' , hX' , HA' , HB'))))) = inv-htpy HB +pr2 + ( pr2 + ( pr2 + ( pr2 + ( cospan-hom-cospan-diagram-rotate' f g f' g' f'' g'' + ( hA , hB , hX , HA , HB) + ( hA' , hB' , hX' , HA' , HB'))))) = inv-htpy HB' +``` diff --git a/src/foundation/morphisms-cospans.lagda.md b/src/foundation/morphisms-cospans.lagda.md index d8f07831fe..f90a01e478 100644 --- a/src/foundation/morphisms-cospans.lagda.md +++ b/src/foundation/morphisms-cospans.lagda.md @@ -7,138 +7,53 @@ module foundation.morphisms-cospans where
Imports ```agda +open import foundation.cartesian-product-types +open import foundation.cospans open import foundation.dependent-pair-types open import foundation.universe-levels -open import foundation-core.cartesian-product-types -open import foundation-core.function-types -open import foundation-core.homotopies +open import foundation-core.commuting-triangles-of-maps ```
## Idea -A **morphism of cospans** is a commuting diagram of the form +Consider two [cospans](foundation.cospans.md) `c := (X , f , g)` and +`d := (Y , h , k)` from `A` to `B`. A +{{#concept "morphism of cospans" Agda=hom-cospan}} from `c` to `d` consists of a +map `u : X → Y` equipped with [homotopies](foundation-core.homotopies.md) +witnessing that the two triangles ```text - A -----> X <----- B - | | | - | | | - V V V - A' ----> X' <---- B'. + u u + X ----> Y X ----> Y + \ / \ / + f \ / h g \ / k + V V V V + A B ``` +[commute](foundation.commuting-triangles-of-maps.md). + ## Definitions ### Morphisms of cospans ```agda -hom-cospan : - {l1 l2 l3 l1' l2' l3' : Level} - {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) - {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} (f' : A' → X') (g' : B' → X') → - UU (l1 ⊔ l2 ⊔ l3 ⊔ l1' ⊔ l2' ⊔ l3') -hom-cospan {A = A} {B} {X} f g {A'} {B'} {X'} f' g' = - Σ ( A → A') - ( λ hA → - Σ ( B → B') - ( λ hB → - Σ ( X → X') - ( λ hX → (f' ∘ hA ~ hX ∘ f) × (g' ∘ hB ~ hX ∘ g)))) -``` - -### Identity morphisms of cospans - -```agda -id-hom-cospan : - {l1 l2 l3 l1' l2' l3' : Level} - {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) → - hom-cospan f g f g -pr1 (id-hom-cospan f g) = id -pr1 (pr2 (id-hom-cospan f g)) = id -pr1 (pr2 (pr2 (id-hom-cospan f g))) = id -pr1 (pr2 (pr2 (pr2 (id-hom-cospan f g)))) = refl-htpy -pr2 (pr2 (pr2 (pr2 (id-hom-cospan f g)))) = refl-htpy -``` - -### Rotating cospans of cospans - -```agda -cospan-hom-cospan-rotate : - {l1 l2 l3 l1' l2' l3' l1'' l2'' l3'' : Level} - {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) - {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} (f' : A' → X') (g' : B' → X') - {A'' : UU l1''} {B'' : UU l2''} {X'' : UU l3''} - (f'' : A'' → X'') (g'' : B'' → X'') - (h : hom-cospan f' g' f g) (h' : hom-cospan f'' g'' f g) → - hom-cospan (pr1 h) (pr1 h') (pr1 (pr2 (pr2 h))) (pr1 (pr2 (pr2 h'))) -pr1 - ( cospan-hom-cospan-rotate f g f' g' f'' g'' - ( hA , hB , hX , HA , HB) - ( hA' , hB' , hX' , HA' , HB')) = f' -pr1 - ( pr2 - ( cospan-hom-cospan-rotate f g f' g' f'' g'' - ( hA , hB , hX , HA , HB) - ( hA' , hB' , hX' , HA' , HB'))) = f'' -pr1 - ( pr2 - ( pr2 - ( cospan-hom-cospan-rotate f g f' g' f'' g'' - ( hA , hB , hX , HA , HB) - ( hA' , hB' , hX' , HA' , HB')))) = f -pr1 - ( pr2 - ( pr2 - ( pr2 - ( cospan-hom-cospan-rotate f g f' g' f'' g'' - ( hA , hB , hX , HA , HB) - ( hA' , hB' , hX' , HA' , HB'))))) = inv-htpy HA -pr2 - ( pr2 - ( pr2 - ( pr2 - ( cospan-hom-cospan-rotate f g f' g' f'' g'' - ( hA , hB , hX , HA , HB) - ( hA' , hB' , hX' , HA' , HB'))))) = inv-htpy HA' - -cospan-hom-cospan-rotate' : - {l1 l2 l3 l1' l2' l3' l1'' l2'' l3'' : Level} - {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) - {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} (f' : A' → X') (g' : B' → X') - {A'' : UU l1''} {B'' : UU l2''} {X'' : UU l3''} - (f'' : A'' → X'') (g'' : B'' → X'') - (h : hom-cospan f' g' f g) (h' : hom-cospan f'' g'' f g) → - hom-cospan - (pr1 (pr2 h)) (pr1 (pr2 h')) (pr1 (pr2 (pr2 h))) (pr1 (pr2 (pr2 h'))) -pr1 - ( cospan-hom-cospan-rotate' f g f' g' f'' g'' - ( hA , hB , hX , HA , HB) - ( hA' , hB' , hX' , HA' , HB')) = g' -pr1 - ( pr2 - ( cospan-hom-cospan-rotate' f g f' g' f'' g'' - ( hA , hB , hX , HA , HB) - ( hA' , hB' , hX' , HA' , HB'))) = g'' -pr1 - ( pr2 - ( pr2 - ( cospan-hom-cospan-rotate' f g f' g' f'' g'' - ( hA , hB , hX , HA , HB) - ( hA' , hB' , hX' , HA' , HB')))) = g -pr1 - ( pr2 - ( pr2 - ( pr2 - ( cospan-hom-cospan-rotate' f g f' g' f'' g'' - ( hA , hB , hX , HA , HB) - ( hA' , hB' , hX' , HA' , HB'))))) = inv-htpy HB -pr2 - ( pr2 - ( pr2 - ( pr2 - ( cospan-hom-cospan-rotate' f g f' g' f'' g'' - ( hA , hB , hX , HA , HB) - ( hA' , hB' , hX' , HA' , HB'))))) = inv-htpy HB' +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} + (c : cospan l3 A B) (d : cospan l4 A B) + where + + coherence-hom-cospan : + (codomain-cospan c → codomain-cospan d) → UU (l1 ⊔ l2 ⊔ l4) + coherence-hom-cospan h = + ( coherence-triangle-maps (left-map-cospan d) h (left-map-cospan c)) × + ( coherence-triangle-maps (right-map-cospan d) h (right-map-cospan c)) + + hom-cospan : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + hom-cospan = + Σ ( codomain-cospan c → codomain-cospan d) + ( coherence-hom-cospan) ``` diff --git a/src/foundation/morphisms-span-diagrams.lagda.md b/src/foundation/morphisms-span-diagrams.lagda.md new file mode 100644 index 0000000000..7b5ba197e5 --- /dev/null +++ b/src/foundation/morphisms-span-diagrams.lagda.md @@ -0,0 +1,182 @@ +# Morphisms of span diagrams + +```agda +module foundation.morphisms-span-diagrams where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.morphisms-arrows +open import foundation.morphisms-spans +open import foundation.operations-spans +open import foundation.span-diagrams +open import foundation.universe-levels + +open import foundation-core.commuting-squares-of-maps +``` + +
+ +## Idea + +A {{#concept "morphism of span diagrams" Agda=hom-span-diagram}} from a +[span diagram](foundation.span-diagrams.md) `A <-f- S -g-> B` to a span diagram +`C <-h- T -k-> D` consists of maps `u : A → C`, `v : B → D`, and `w : S → T` +[equipped](foundation.structure.md) with two +[homotopies](foundation-core.homotopies.md) witnessing that the diagram + +```text + f g + A <----- S -----> B + | | | + u | | w | v + V V V + C <----- T -----> D + h k +``` + +[commutes](foundation-core.commuting-squares-of-maps.md). + +The definition of morphisms of span diagrams is given concisely in terms of the +notion of morphisms of spans. In the resulting definitions, the commuting +squares of morphisms of spans are oriented in the following way: + +- A homotopy + `map-domain-hom-span ∘ left-map-span s ~ left-map-span t ∘ spanning-map-hom-span` + witnessing that the square + + ```text + spanning-map-hom-span + S ----------------------> T + | | + left-map-span s | | left-map-span t + V V + A ----------------------> C + map-domain-hom-span + ``` + + commutes. + +- A homotopy + `map-domain-hom-span ∘ right-map-span s ~ right-map-span t ∘ spanning-map-hom-span` + witnessing that the square + + ```text + spanning-map-hom-span + S ----------------------> T + | | + right-map-span s | | right-map-span t + V V + B ----------------------> D + map-codomain-hom-span + ``` + + commutes. + +## Definitions + +### Morphisms of span diagrams + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (𝒮 : span-diagram l1 l2 l3) (𝒯 : span-diagram l4 l5 l6) + where + + hom-span-diagram : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) + hom-span-diagram = + Σ ( domain-span-diagram 𝒮 → domain-span-diagram 𝒯) + ( λ f → + Σ ( codomain-span-diagram 𝒮 → codomain-span-diagram 𝒯) + ( λ g → + hom-span + ( concat-span + ( span-span-diagram 𝒮) + ( f) + ( g)) + ( span-span-diagram 𝒯))) + +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (𝒮 : span-diagram l1 l2 l3) (𝒯 : span-diagram l4 l5 l6) + (f : hom-span-diagram 𝒮 𝒯) + where + + map-domain-hom-span-diagram : + domain-span-diagram 𝒮 → domain-span-diagram 𝒯 + map-domain-hom-span-diagram = pr1 f + + map-codomain-hom-span-diagram : + codomain-span-diagram 𝒮 → codomain-span-diagram 𝒯 + map-codomain-hom-span-diagram = pr1 (pr2 f) + + hom-span-hom-span-diagram : + hom-span + ( concat-span + ( span-span-diagram 𝒮) + ( map-domain-hom-span-diagram) + ( map-codomain-hom-span-diagram)) + ( span-span-diagram 𝒯) + hom-span-hom-span-diagram = pr2 (pr2 f) + + spanning-map-hom-span-diagram : + spanning-type-span-diagram 𝒮 → spanning-type-span-diagram 𝒯 + spanning-map-hom-span-diagram = + map-hom-span + ( concat-span + ( span-span-diagram 𝒮) + ( map-domain-hom-span-diagram) + ( map-codomain-hom-span-diagram)) + ( span-span-diagram 𝒯) + ( hom-span-hom-span-diagram) + + left-square-hom-span-diagram : + coherence-square-maps + ( spanning-map-hom-span-diagram) + ( left-map-span-diagram 𝒮) + ( left-map-span-diagram 𝒯) + ( map-domain-hom-span-diagram) + left-square-hom-span-diagram = + left-triangle-hom-span + ( concat-span + ( span-span-diagram 𝒮) + ( map-domain-hom-span-diagram) + ( map-codomain-hom-span-diagram)) + ( span-span-diagram 𝒯) + ( hom-span-hom-span-diagram) + + left-hom-arrow-hom-span-diagram : + hom-arrow (left-map-span-diagram 𝒮) (left-map-span-diagram 𝒯) + pr1 left-hom-arrow-hom-span-diagram = + spanning-map-hom-span-diagram + pr1 (pr2 left-hom-arrow-hom-span-diagram) = + map-domain-hom-span-diagram + pr2 (pr2 left-hom-arrow-hom-span-diagram) = + left-square-hom-span-diagram + + right-square-hom-span-diagram : + coherence-square-maps + ( spanning-map-hom-span-diagram) + ( right-map-span-diagram 𝒮) + ( right-map-span-diagram 𝒯) + ( map-codomain-hom-span-diagram) + right-square-hom-span-diagram = + right-triangle-hom-span + ( concat-span + ( span-span-diagram 𝒮) + ( map-domain-hom-span-diagram) + ( map-codomain-hom-span-diagram)) + ( span-span-diagram 𝒯) + ( hom-span-hom-span-diagram) + + right-hom-arrow-hom-span-diagram : + hom-arrow (right-map-span-diagram 𝒮) (right-map-span-diagram 𝒯) + pr1 right-hom-arrow-hom-span-diagram = + spanning-map-hom-span-diagram + pr1 (pr2 right-hom-arrow-hom-span-diagram) = + map-codomain-hom-span-diagram + pr2 (pr2 right-hom-arrow-hom-span-diagram) = + right-square-hom-span-diagram +``` diff --git a/src/foundation/morphisms-spans-families-of-types.lagda.md b/src/foundation/morphisms-spans-families-of-types.lagda.md new file mode 100644 index 0000000000..e8de109012 --- /dev/null +++ b/src/foundation/morphisms-spans-families-of-types.lagda.md @@ -0,0 +1,210 @@ +# Morphisms of spans on families of types + +```agda +module foundation.morphisms-spans-families-of-types where +``` + +
Imports + +```agda +open import foundation.commuting-triangles-of-homotopies +open import foundation.dependent-pair-types +open import foundation.equality-dependent-function-types +open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopy-induction +open import foundation.spans-families-of-types +open import foundation.structure-identity-principle +open import foundation.universe-levels +open import foundation.whiskering-homotopies + +open import foundation-core.commuting-triangles-of-maps +open import foundation-core.equivalences +open import foundation-core.homotopies +open import foundation-core.identity-types +open import foundation-core.torsorial-type-families +``` + +
+ +## Idea + +Consider two [spans](foundation.spans-families-of-types.md) `𝒮 := (S , f)` and +`𝒯 := (T , g)` on a family of types `A : I → 𝒰`. A +{{#concept "morphism" Disambiguation="span on a family of types" Agda=hom-span-type-family}} +from `𝒮` to `𝒯` consists of a map `h : S → T` and a +[homotopy](foundation-core.homotopies.md) witnessing that the triangle + +```text + h + S ----> T + \ / + f i \ / g i + ∨ ∨ + A i +``` + +[commutes](foundation-core.commuting-triangles-of-maps.md) for every `i : I`. + +## Definitions + +### Morphisms of spans on families of types + +```agda +module _ + {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} + (𝒮 : span-type-family l3 A) (𝒯 : span-type-family l4 A) + where + + hom-span-type-family : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + hom-span-type-family = + Σ ( spanning-type-span-type-family 𝒮 → + spanning-type-span-type-family 𝒯) + ( λ h → + (i : I) → + coherence-triangle-maps + ( map-span-type-family 𝒮 i) + ( map-span-type-family 𝒯 i) + ( h)) + +module _ + {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} + (𝒮 : span-type-family l3 A) (𝒯 : span-type-family l4 A) + (h : hom-span-type-family 𝒮 𝒯) + where + + map-hom-span-type-family : + spanning-type-span-type-family 𝒮 → + spanning-type-span-type-family 𝒯 + map-hom-span-type-family = pr1 h + + coherence-triangle-hom-span-type-family : + (i : I) → + coherence-triangle-maps + ( map-span-type-family 𝒮 i) + ( map-span-type-family 𝒯 i) + ( map-hom-span-type-family) + coherence-triangle-hom-span-type-family = + pr2 h +``` + +### Homotopies of morphisms of spans on families of types + +Consider two spans `𝒮 := (S , f)` and `𝒯 := (T , g)` on a family of types +`A : I → 𝒰`, and consider two morphisms `(h , H)` and `(k , K)` between them. A +{{#concept "homotopy" Disambiguation="morphism between spans on families of types" Agda=htpy-hom-span-type-family}} +is a pair `(α , β)` consisting of a homotopy + +```text + α : h ~ k +``` + +and a family `β` of homotopies witnessing that the triangle + +```text + f i + / \ + H i / β i \ K i + ∨ ∨ + (g i ∘ h) ------> (g i ∘ k) + g i · α +``` + +commutes for each `i : I`. + +```agda +module _ + {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} + (𝒮 : span-type-family l3 A) (𝒯 : span-type-family l4 A) + (h k : hom-span-type-family 𝒮 𝒯) + where + + coherence-htpy-hom-span-type-family : + map-hom-span-type-family 𝒮 𝒯 h ~ map-hom-span-type-family 𝒮 𝒯 k → + UU (l1 ⊔ l2 ⊔ l3) + coherence-htpy-hom-span-type-family α = + (i : I) → + coherence-triangle-homotopies' + ( coherence-triangle-hom-span-type-family 𝒮 𝒯 k i) + ( map-span-type-family 𝒯 i ·l α) + ( coherence-triangle-hom-span-type-family 𝒮 𝒯 h i) + + htpy-hom-span-type-family : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + htpy-hom-span-type-family = + Σ ( map-hom-span-type-family 𝒮 𝒯 h ~ map-hom-span-type-family 𝒮 𝒯 k) + ( coherence-htpy-hom-span-type-family) + + module _ + (α : htpy-hom-span-type-family) + where + + htpy-htpy-hom-span-type-family : + map-hom-span-type-family 𝒮 𝒯 h ~ map-hom-span-type-family 𝒮 𝒯 k + htpy-htpy-hom-span-type-family = pr1 α + + coh-htpy-hom-span-type-family : + coherence-htpy-hom-span-type-family htpy-htpy-hom-span-type-family + coh-htpy-hom-span-type-family = pr2 α +``` + +### The reflexivity homotopy on a morphism of spans on families of types + +```agda +module _ + {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} + (𝒮 : span-type-family l3 A) (𝒯 : span-type-family l4 A) + (h : hom-span-type-family 𝒮 𝒯) + where + + refl-htpy-hom-span-type-family : + htpy-hom-span-type-family 𝒮 𝒯 h h + pr1 refl-htpy-hom-span-type-family = refl-htpy + pr2 refl-htpy-hom-span-type-family i = right-unit-htpy +``` + +## Properties + +### Characterization of identifications of morphisms of spans on families of types + +```agda +module _ + {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} + (𝒮 : span-type-family l3 A) (𝒯 : span-type-family l4 A) + (h : hom-span-type-family 𝒮 𝒯) + where + + htpy-eq-hom-span-type-family : + (k : hom-span-type-family 𝒮 𝒯) → + h = k → htpy-hom-span-type-family 𝒮 𝒯 h k + htpy-eq-hom-span-type-family .h refl = + refl-htpy-hom-span-type-family 𝒮 𝒯 h + + is-torsorial-htpy-hom-span-type-family : + is-torsorial (htpy-hom-span-type-family 𝒮 𝒯 h) + is-torsorial-htpy-hom-span-type-family = + is-torsorial-Eq-structure + ( is-torsorial-htpy _) + ( map-hom-span-type-family 𝒮 𝒯 h , refl-htpy) + ( is-torsorial-Eq-Π (λ i → is-torsorial-htpy _)) + + is-equiv-htpy-eq-hom-span-type-family : + (k : hom-span-type-family 𝒮 𝒯) → + is-equiv (htpy-eq-hom-span-type-family k) + is-equiv-htpy-eq-hom-span-type-family = + fundamental-theorem-id + ( is-torsorial-htpy-hom-span-type-family) + ( htpy-eq-hom-span-type-family) + + extensionality-hom-span-type-family : + (k : hom-span-type-family 𝒮 𝒯) → + (h = k) ≃ htpy-hom-span-type-family 𝒮 𝒯 h k + pr1 (extensionality-hom-span-type-family k) = + htpy-eq-hom-span-type-family k + pr2 (extensionality-hom-span-type-family k) = + is-equiv-htpy-eq-hom-span-type-family k + + eq-htpy-hom-span-type-family : + (k : hom-span-type-family 𝒮 𝒯) → + htpy-hom-span-type-family 𝒮 𝒯 h k → h = k + eq-htpy-hom-span-type-family k = + map-inv-equiv (extensionality-hom-span-type-family k) +``` diff --git a/src/foundation/morphisms-spans.lagda.md b/src/foundation/morphisms-spans.lagda.md new file mode 100644 index 0000000000..700e1f771b --- /dev/null +++ b/src/foundation/morphisms-spans.lagda.md @@ -0,0 +1,83 @@ +# Morphisms of spans + +```agda +module foundation.morphisms-spans where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.spans +open import foundation.universe-levels + +open import foundation-core.cartesian-product-types +open import foundation-core.commuting-squares-of-maps +open import foundation-core.commuting-triangles-of-maps +open import foundation-core.operations-spans +``` + +
+ +## Idea + +A {{#concept "morphism of spans" Agda=hom-span}} from a +[span](foundation.spans.md) `A <-f- S -g-> B` to a span `A <-h- T -k-> B` +consists of a map `w : S → T` [equipped](foundation.structure.md) with two +[homotopies](foundation-core.homotopies.md) witnessing that the diagram + +```text + S + / | \ + f / | \ h + V | V + A |w B + ∧ | ∧ + h \ | / k + \ V / + T +``` + +[commutes](foundation.commuting-triangles-of-maps.md). + +## Definitions + +### Morphisms between spans + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} + (s : span l3 A B) (t : span l4 A B) + where + + left-coherence-hom-span : + (spanning-type-span s → spanning-type-span t) → UU (l1 ⊔ l3) + left-coherence-hom-span = + coherence-triangle-maps (left-map-span s) (left-map-span t) + + right-coherence-hom-span : + (spanning-type-span s → spanning-type-span t) → UU (l2 ⊔ l3) + right-coherence-hom-span = + coherence-triangle-maps (right-map-span s) (right-map-span t) + + coherence-hom-span : + (spanning-type-span s → spanning-type-span t) → UU (l1 ⊔ l2 ⊔ l3) + coherence-hom-span f = left-coherence-hom-span f × right-coherence-hom-span f + + hom-span : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + hom-span = Σ (spanning-type-span s → spanning-type-span t) coherence-hom-span + +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} + (s : span l3 A B) (t : span l4 A B) (f : hom-span s t) + where + + map-hom-span : spanning-type-span s → spanning-type-span t + map-hom-span = pr1 f + + left-triangle-hom-span : left-coherence-hom-span s t map-hom-span + left-triangle-hom-span = pr1 (pr2 f) + + right-triangle-hom-span : right-coherence-hom-span s t map-hom-span + right-triangle-hom-span = pr2 (pr2 f) +``` diff --git a/src/foundation/operations-span-diagrams.lagda.md b/src/foundation/operations-span-diagrams.lagda.md new file mode 100644 index 0000000000..f162990c4a --- /dev/null +++ b/src/foundation/operations-span-diagrams.lagda.md @@ -0,0 +1,168 @@ +# Operations on span diagrams + +```agda +module foundation.operations-span-diagrams where + +open import foundation-core.operations-span-diagrams public +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.equivalences-arrows +open import foundation.operations-spans +open import foundation.span-diagrams +open import foundation.spans +open import foundation.universe-levels +``` + +
+ +## Idea + +This file contains some further operations on +[span diagrams](foundation.span-diagrams.md) that produce new span diagrams from +given span diagrams and possibly other data. Previous operations on span +diagrams were defined in +[`foundation-core.operations-span-diagrams`](foundation-core.operations-span-diagrams.md). + +## Definitions + +### Concatenating span diagrams and equivalences of arrows on the left + +Consider a span diagram `𝒮` given by + +```text + f g + A <----- S -----> B +``` + +and an [equivalence of arrows](foundation.equivalences-arrows.md) +`h : equiv-arrow f' f` as indicated in the diagram + +```text + f' + A' <---- S' + | | + h₀ | ≃ ≃ | h₁ + V V + A <----- S -----> B. + f g +``` + +Then we obtain a span diagram `A' <- S' -> B`. + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} (𝒮 : span-diagram l1 l2 l3) + {S' : UU l4} {A' : UU l5} (f' : S' → A') + (h : equiv-arrow f' (left-map-span-diagram 𝒮)) + where + + domain-left-concat-equiv-arrow-span-diagram : UU l5 + domain-left-concat-equiv-arrow-span-diagram = A' + + codomain-left-concat-equiv-arrow-span-diagram : UU l2 + codomain-left-concat-equiv-arrow-span-diagram = codomain-span-diagram 𝒮 + + span-left-concat-equiv-arrow-span-diagram : + span l4 + ( domain-left-concat-equiv-arrow-span-diagram) + ( codomain-left-concat-equiv-arrow-span-diagram) + span-left-concat-equiv-arrow-span-diagram = + left-concat-equiv-arrow-span (span-span-diagram 𝒮) f' h + + left-concat-equiv-arrow-span-diagram : span-diagram l5 l2 l4 + pr1 left-concat-equiv-arrow-span-diagram = + domain-left-concat-equiv-arrow-span-diagram + pr1 (pr2 left-concat-equiv-arrow-span-diagram) = + codomain-left-concat-equiv-arrow-span-diagram + pr2 (pr2 left-concat-equiv-arrow-span-diagram) = + span-left-concat-equiv-arrow-span-diagram + + spanning-type-left-concat-equiv-arrow-span-diagram : UU l4 + spanning-type-left-concat-equiv-arrow-span-diagram = + spanning-type-span-diagram left-concat-equiv-arrow-span-diagram + + left-map-left-concat-equiv-arrow-span-diagram : + spanning-type-left-concat-equiv-arrow-span-diagram → + domain-left-concat-equiv-arrow-span-diagram + left-map-left-concat-equiv-arrow-span-diagram = + left-map-span-diagram left-concat-equiv-arrow-span-diagram + + right-map-left-concat-equiv-arrow-span-diagram : + spanning-type-left-concat-equiv-arrow-span-diagram → + codomain-left-concat-equiv-arrow-span-diagram + right-map-left-concat-equiv-arrow-span-diagram = + right-map-span-diagram left-concat-equiv-arrow-span-diagram +``` + +### Concatenating span diagrams and equivalences of arrows on the right + +Consider a span diagram `𝒮` given by + +```text + f g + A <----- S -----> B +``` + +and a [equivalence of arrows](foundation.equivalences-arrows.md) +`h : equiv-arrow g' g` as indicated in the diagram + +```text + g' + S' ----> B' + | | + h₀ | ≃ ≃ | h₁ + V V + A <----- S -----> B. + f g +``` + +Then we obtain a span diagram `A <- S' -> B'`. + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} (𝒮 : span-diagram l1 l2 l3) + {S' : UU l4} {B' : UU l5} (g' : S' → B') + (h : equiv-arrow g' (right-map-span-diagram 𝒮)) + where + + domain-right-concat-equiv-arrow-span-diagram : UU l1 + domain-right-concat-equiv-arrow-span-diagram = domain-span-diagram 𝒮 + + codomain-right-concat-equiv-arrow-span-diagram : UU l5 + codomain-right-concat-equiv-arrow-span-diagram = B' + + span-right-concat-equiv-arrow-span-diagram : + span l4 + ( domain-right-concat-equiv-arrow-span-diagram) + ( codomain-right-concat-equiv-arrow-span-diagram) + span-right-concat-equiv-arrow-span-diagram = + right-concat-equiv-arrow-span (span-span-diagram 𝒮) g' h + + right-concat-equiv-arrow-span-diagram : span-diagram l1 l5 l4 + pr1 right-concat-equiv-arrow-span-diagram = + domain-right-concat-equiv-arrow-span-diagram + pr1 (pr2 right-concat-equiv-arrow-span-diagram) = + codomain-right-concat-equiv-arrow-span-diagram + pr2 (pr2 right-concat-equiv-arrow-span-diagram) = + span-right-concat-equiv-arrow-span-diagram + + spanning-type-right-concat-equiv-arrow-span-diagram : UU l4 + spanning-type-right-concat-equiv-arrow-span-diagram = + spanning-type-span-diagram right-concat-equiv-arrow-span-diagram + + left-map-right-concat-equiv-arrow-span-diagram : + spanning-type-right-concat-equiv-arrow-span-diagram → + domain-right-concat-equiv-arrow-span-diagram + left-map-right-concat-equiv-arrow-span-diagram = + left-map-span-diagram right-concat-equiv-arrow-span-diagram + + right-map-right-concat-equiv-arrow-span-diagram : + spanning-type-right-concat-equiv-arrow-span-diagram → + codomain-right-concat-equiv-arrow-span-diagram + right-map-right-concat-equiv-arrow-span-diagram = + right-map-span-diagram right-concat-equiv-arrow-span-diagram +``` diff --git a/src/foundation/operations-spans-families-of-types.lagda.md b/src/foundation/operations-spans-families-of-types.lagda.md new file mode 100644 index 0000000000..b5924d1e21 --- /dev/null +++ b/src/foundation/operations-spans-families-of-types.lagda.md @@ -0,0 +1,55 @@ +# Operations on spans of families of types + +```agda +module foundation.operations-spans-families-of-types where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.spans-families-of-types +open import foundation.universe-levels + +open import foundation-core.function-types +``` + +
+ +## Idea + +This file contains a collection of operations that produce new +[spans of families of types](foundation.spans-families-of-types.md) from given +spans of families of types. + +## Definitions + +### Concatenation of spans and families of maps + +Consider a span `𝒮 := (S , s)` on a family of types `A : I → 𝒰` and consider a +family of maps `f : (i : I) → A i → B i`. Then we can concatenate the span `𝒮` +with the family of maps `f` to obtain the span `(S , λ i → f i ∘ s i)` on `B`. + +```agda +module _ + {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3} + (𝒮 : span-type-family l4 A) + (f : (i : I) → A i → B i) + where + + spanning-type-concat-span-hom-family-of-types : UU l4 + spanning-type-concat-span-hom-family-of-types = + spanning-type-span-type-family 𝒮 + + map-concat-span-hom-family-of-types : + (i : I) → spanning-type-concat-span-hom-family-of-types → B i + map-concat-span-hom-family-of-types i = + f i ∘ map-span-type-family 𝒮 i + + concat-span-hom-family-of-types : + span-type-family l4 B + pr1 concat-span-hom-family-of-types = + spanning-type-concat-span-hom-family-of-types + pr2 concat-span-hom-family-of-types = + map-concat-span-hom-family-of-types +``` diff --git a/src/foundation/operations-spans.lagda.md b/src/foundation/operations-spans.lagda.md new file mode 100644 index 0000000000..2963f46eae --- /dev/null +++ b/src/foundation/operations-spans.lagda.md @@ -0,0 +1,140 @@ +# Operations on spans + +```agda +module foundation.operations-spans where + +open import foundation-core.operations-spans public +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.equivalences-arrows +open import foundation.morphisms-arrows +open import foundation.spans +open import foundation.universe-levels + +open import foundation-core.function-types +``` + +
+ +## Idea + +This file contains some further operations on [spans](foundation.spans.md) that +produce new spans from given spans and possibly other data. Previous operations +on spans were defined in +[`foundation-core.operations-spans`](foundation-core.operations-spans.md). + +## Definitions + +### Concatenating spans and equivalences of arrows on the left + +Consider a span `s` given by + +```text + f g + A <----- S -----> B +``` + +and an [equivalence of arrows](foundation.equivalences-arrows.md) +`h : equiv-arrow f' f` as indicated in the diagram + +```text + f' + A' <---- S' + | | + h₀ | ≃ ≃ | h₁ + V V + A <----- S -----> B. + f g +``` + +Then we obtain a span `A' <- S' -> B`. + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} + (s : span l3 A B) + {S' : UU l4} {A' : UU l5} (f' : S' → A') + (h : equiv-arrow f' (left-map-span s)) + where + + spanning-type-left-concat-equiv-arrow-span : UU l4 + spanning-type-left-concat-equiv-arrow-span = S' + + left-map-left-concat-equiv-arrow-span : + spanning-type-left-concat-equiv-arrow-span → A' + left-map-left-concat-equiv-arrow-span = f' + + right-map-left-concat-equiv-arrow-span : + spanning-type-left-concat-equiv-arrow-span → B + right-map-left-concat-equiv-arrow-span = + ( right-map-span s) ∘ + ( map-domain-equiv-arrow f' (left-map-span s) h) + + left-concat-equiv-arrow-span : + span l4 A' B + pr1 left-concat-equiv-arrow-span = + spanning-type-left-concat-equiv-arrow-span + pr1 (pr2 left-concat-equiv-arrow-span) = + left-map-left-concat-equiv-arrow-span + pr2 (pr2 left-concat-equiv-arrow-span) = + right-map-left-concat-equiv-arrow-span +``` + +### Concatenating spans and equivalences of arrows on the right + +Consider a span `s` given by + +```text + f g + A <----- S -----> B +``` + +and a [morphism of arrows](foundation.morphisms-arrows.md) `h : hom-arrow g' g` +as indicated in the diagram + +```text + g' + S' ----> B' + | | + h₀ | ≃ ≃ | h₁ + V V + A <----- S -----> B. + f g +``` + +Then we obtain a span `A <- S' -> B'`. + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} + (s : span l3 A B) + {S' : UU l4} {B' : UU l5} (g' : S' → B') + (h : equiv-arrow g' (right-map-span s)) + where + + spanning-type-right-concat-equiv-arrow-span : UU l4 + spanning-type-right-concat-equiv-arrow-span = S' + + left-map-right-concat-equiv-arrow-span : + spanning-type-right-concat-equiv-arrow-span → A + left-map-right-concat-equiv-arrow-span = + ( left-map-span s) ∘ + ( map-domain-equiv-arrow g' (right-map-span s) h) + + right-map-right-concat-equiv-arrow-span : + spanning-type-right-concat-equiv-arrow-span → B' + right-map-right-concat-equiv-arrow-span = g' + + right-concat-equiv-arrow-span : + span l4 A B' + pr1 right-concat-equiv-arrow-span = + spanning-type-right-concat-equiv-arrow-span + pr1 (pr2 right-concat-equiv-arrow-span) = + left-map-right-concat-equiv-arrow-span + pr2 (pr2 right-concat-equiv-arrow-span) = + right-map-right-concat-equiv-arrow-span +``` diff --git a/src/foundation/opposite-spans.lagda.md b/src/foundation/opposite-spans.lagda.md new file mode 100644 index 0000000000..dba2196ab0 --- /dev/null +++ b/src/foundation/opposite-spans.lagda.md @@ -0,0 +1,57 @@ +# Opposite spans + +```agda +module foundation.opposite-spans where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.spans +open import foundation.universe-levels +``` + +
+ +## Idea + +Consider a [span](foundation.spans.md) `(S , f , g)` from `A` to `B`. The +{{#concept "opposite span" Agda=opposite-span}} of `(S , f , g)` is the span +`(S , g , f)` from `B` to `A`. In other words, the opposite of a span + +```text + f g + A <----- S -----> B +``` + +is the span + +```text + g f + B <----- S -----> A. +``` + +Recall that [binary type duality](foundation.binary-type-duality.md) shows that +spans are equivalent to [binary relations](foundation.binary-relations.md) from +`A` to `B`. The opposite of a span corresponds to the opposite of a binary +relation. + +## Definitions + +### The opposite of a span + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} + where + + opposite-span : span l3 A B → span l3 B A + pr1 (opposite-span s) = spanning-type-span s + pr1 (pr2 (opposite-span s)) = right-map-span s + pr2 (pr2 (opposite-span s)) = left-map-span s +``` + +## See also + +- [Transpositions of span diagrams](foundation.transposition-span-diagrams.md) diff --git a/src/foundation/partial-functions.lagda.md b/src/foundation/partial-functions.lagda.md index 25b80b1555..d11bd0d4ac 100644 --- a/src/foundation/partial-functions.lagda.md +++ b/src/foundation/partial-functions.lagda.md @@ -17,17 +17,18 @@ open import foundation-core.propositions ## 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 +A {{#concept "partial function" Agda=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. +{{#concept "defined" Disambiguation="partial function" Agda=is-defined-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 diff --git a/src/foundation/partial-sequences.lagda.md b/src/foundation/partial-sequences.lagda.md index ed0d7e2144..a45abe530c 100644 --- a/src/foundation/partial-sequences.lagda.md +++ b/src/foundation/partial-sequences.lagda.md @@ -19,9 +19,9 @@ open import foundation-core.propositions ## 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 +A {{#concept "partial sequence" Agda=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) diff --git a/src/foundation/permutations-spans-families-of-types.lagda.md b/src/foundation/permutations-spans-families-of-types.lagda.md new file mode 100644 index 0000000000..d69f488995 --- /dev/null +++ b/src/foundation/permutations-spans-families-of-types.lagda.md @@ -0,0 +1,46 @@ +# Permutations of spans of families of types + +```agda +module foundation.permutations-spans-families-of-types where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.spans-families-of-types +open import foundation.universe-levels + +open import foundation-core.equivalences +open import foundation-core.function-types +``` + +
+ +## Idea + +Permutations of spans of families of types are a generalization of the +[opposite](foundation.opposite-spans.md) of a +[binary span](foundation.spans.md). Consider a +[span](foundation.spans-families-of-types.md) `(S , f)` on a type family +`A : I → 𝒰` and an [equivalence](foundation-core.equivalences.md) `e : I ≃ I`. +Then the {{#concept "permutation" Disambiguation="spans of families of types"}} +is the span `(S , f ∘ e)` on the type family `A ∘ e`. + +## Definitions + +### Permutations of spans of families of types + +```agda +module _ + {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} + where + + permutation-span-type-family : + (e : I ≃ I) → span-type-family l3 A → + span-type-family l3 (A ∘ map-equiv e) + pr1 (permutation-span-type-family e s) = + spanning-type-span-type-family s + pr2 (permutation-span-type-family e s) i = + map-span-type-family s (map-equiv e i) +``` diff --git a/src/foundation/postcomposition-dependent-functions.lagda.md b/src/foundation/postcomposition-dependent-functions.lagda.md index b5eafce2fd..e48ec891fb 100644 --- a/src/foundation/postcomposition-dependent-functions.lagda.md +++ b/src/foundation/postcomposition-dependent-functions.lagda.md @@ -17,8 +17,7 @@ open import foundation-core.function-types ## Idea Given a type `A` and a dependent map `f : {a : A} → X a → Y a`, the -{{#concept "dependent -postcomposition function" Agda=postcomp-Π}} +{{#concept "dependent postcomposition function" Agda=postcomp-Π}} ```text f ∘ - : ((a : A) → X a) → ((a : A) → Y a) diff --git a/src/foundation/precomposition-functions.lagda.md b/src/foundation/precomposition-functions.lagda.md index b3e28081d2..69f45b2776 100644 --- a/src/foundation/precomposition-functions.lagda.md +++ b/src/foundation/precomposition-functions.lagda.md @@ -26,8 +26,6 @@ open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.retractions open import foundation-core.whiskering-homotopies - -open import synthetic-homotopy-theory.cocones-under-spans ```
@@ -107,6 +105,21 @@ module _ ### Computations of the fibers of `precomp` +The fiber of `- ∘ f : (B → X) → (A → X)` at `g ∘ f : B → X` is equivalent to the +type of maps `h : B → X` equipped with a homotopy witnessing that the square + +```text + f + A -----> B + | | + f | | h + V V + B -----> X + g +``` + +commutes. + ```agda module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) (X : UU l3) @@ -130,7 +143,8 @@ module _ compute-fiber-precomp g = compute-coherence-triangle-fiber-precomp (g ∘ f) compute-total-fiber-precomp : - Σ (B → X) (λ g → fiber (precomp f X) (g ∘ f)) ≃ cocone f f X + Σ ( B → X) (λ g → fiber (precomp f X) (g ∘ f)) ≃ + Σ (B → X) (λ u → Σ (B → X) (λ v → u ∘ f ~ v ∘ f)) compute-total-fiber-precomp = equiv-tot compute-fiber-precomp diagonal-into-fibers-precomp : diff --git a/src/foundation/precomposition-type-families.lagda.md b/src/foundation/precomposition-type-families.lagda.md index c257e0b17c..ef459249cf 100644 --- a/src/foundation/precomposition-type-families.lagda.md +++ b/src/foundation/precomposition-type-families.lagda.md @@ -22,7 +22,7 @@ open import foundation-core.whiskering-homotopies ## Idea Any map `f : A → B` induces a -{{#concept "precomposition operation" Disambiguation="type families"}} +{{#concept "precomposition operation" Disambiguation="type families" Agda=precomp-family}} ```text (B → 𝒰) → (A → 𝒰) diff --git a/src/foundation/pullback-squares.lagda.md b/src/foundation/pullback-squares.lagda.md index 47aa0b3886..c3e219be8e 100644 --- a/src/foundation/pullback-squares.lagda.md +++ b/src/foundation/pullback-squares.lagda.md @@ -7,7 +7,7 @@ module foundation.pullback-squares where
Imports ```agda -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.universe-levels diff --git a/src/foundation/pullbacks.lagda.md b/src/foundation/pullbacks.lagda.md index a4444e0ac5..64af30d769 100644 --- a/src/foundation/pullbacks.lagda.md +++ b/src/foundation/pullbacks.lagda.md @@ -11,7 +11,7 @@ open import foundation-core.pullbacks public ```agda open import foundation.action-on-identifications-functions open import foundation.commuting-cubes-of-maps -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.dependent-universal-property-equivalences @@ -78,8 +78,8 @@ The standard pullback consists of [pairs](foundation.dependent-pair-types.md) A ×_X B := Σ (a : A) (b : B), (f a = g b), ``` -thus the standard [cone](foundation.cones-over-cospans.md) consists of the -canonical projections. +thus the standard [cone](foundation.cones-over-cospan-diagrams.md) consists of +the canonical projections. ## Properties diff --git a/src/foundation/span-diagrams-families-of-types.lagda.md b/src/foundation/span-diagrams-families-of-types.lagda.md new file mode 100644 index 0000000000..7b999e0921 --- /dev/null +++ b/src/foundation/span-diagrams-families-of-types.lagda.md @@ -0,0 +1,59 @@ +# Span diagrams on families of types + +```agda +module foundation.span-diagrams-families-of-types where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.spans-families-of-types +open import foundation.universe-levels +``` + +
+ +## Idea + +A {{#concept "span diagram" Disambiguation="family of types"}} on a family of +types indexed by a type `I` consists of a type family `A : I → 𝒰`, and a +[span](foundation.spans-families-of-types.md) on the type family `A`. More +explicitly, a span diagram on a family of types indexed by `I` consists of a +type family `A : I → 𝒰`, a +{{#concept "spanning type" Disambiguation="span diagram on a family of types"}} +`S`, and a family of maps `f : (i : I) → S → A i`. + +## Definitions + +### Span diagrams of families of types + +```agda +span-diagram-type-family : + {l1 : Level} (l2 l3 : Level) → UU l1 → UU (l1 ⊔ lsuc l2 ⊔ lsuc l3) +span-diagram-type-family l2 l3 I = + Σ (I → UU l2) (λ A → span-type-family l3 A) + +module _ + {l1 l2 l3 : Level} {I : UU l1} (s : span-diagram-type-family l2 l3 I) + where + + family-span-diagram-type-family : I → UU l2 + family-span-diagram-type-family = pr1 s + + span-span-diagram-type-family : + span-type-family l3 family-span-diagram-type-family + span-span-diagram-type-family = pr2 s + + spanning-type-span-diagram-type-family : UU l3 + spanning-type-span-diagram-type-family = + spanning-type-span-type-family + ( span-span-diagram-type-family) + + map-span-diagram-type-family : + (i : I) → spanning-type-span-diagram-type-family → + family-span-diagram-type-family i + map-span-diagram-type-family = + map-span-type-family + ( span-span-diagram-type-family) +``` diff --git a/src/foundation/span-diagrams.lagda.md b/src/foundation/span-diagrams.lagda.md new file mode 100644 index 0000000000..3356a17241 --- /dev/null +++ b/src/foundation/span-diagrams.lagda.md @@ -0,0 +1,142 @@ +# Span diagrams + +```agda +module foundation.span-diagrams where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.morphisms-arrows +open import foundation.spans +open import foundation.universe-levels +``` + +
+ +## Idea + +A {{#concept "(binary) span diagram" Agda=span-diagram}} is a diagram of the +form + +```text + f g + A <----- S -----> B. +``` + +In other words, a span diagram consists of two types `A` and `B` and a +[span](foundation.spans.md) from `A` to `B`. + +We disambiguate between [spans](foundation.spans.md) and span diagrams. We +consider spans from `A` to `B` to be _morphisms_ from `A` to `B` in the category +of types and spans between them, whereas we consider span diagrams to be +_objects_ in the category of diagrams of types of the form `* <---- * ----> *`. +Conceptually there is a subtle, but important distinction between spans and span +diagrams. In [binary type duality](foundation.binary-type-duality.md) we show a +span from `A` to `B` is [equivalently](foundation-core.equivalences.md) +described as a [binary relation](foundation.binary-relations.md) from `A` to +`B`. On the other hand, span diagrams are more suitable for functorial +operations that take "spans" as input, but for which the functorial action takes +a natural transformation, i.e., a morphism of span diagrams, as input. Examples +of this kind include [pushouts](synthetic-homotopy-theory.pushouts.md). + +### (Binary) span diagrams + +```agda +span-diagram : (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) +span-diagram l1 l2 l3 = + Σ (UU l1) (λ A → Σ (UU l2) (λ B → span l3 A B)) + +module _ + {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3} + where + + make-span-diagram : + (S → A) → (S → B) → span-diagram l2 l3 l1 + pr1 (make-span-diagram f g) = A + pr1 (pr2 (make-span-diagram f g)) = B + pr1 (pr2 (pr2 (make-span-diagram f g))) = S + pr1 (pr2 (pr2 (pr2 (make-span-diagram f g)))) = f + pr2 (pr2 (pr2 (pr2 (make-span-diagram f g)))) = g + +module _ + {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3) + where + + domain-span-diagram : UU l1 + domain-span-diagram = pr1 𝒮 + + codomain-span-diagram : UU l2 + codomain-span-diagram = pr1 (pr2 𝒮) + + span-span-diagram : + span l3 domain-span-diagram codomain-span-diagram + span-span-diagram = pr2 (pr2 𝒮) + + spanning-type-span-diagram : UU l3 + spanning-type-span-diagram = + spanning-type-span span-span-diagram + + left-map-span-diagram : spanning-type-span-diagram → domain-span-diagram + left-map-span-diagram = + left-map-span span-span-diagram + + right-map-span-diagram : spanning-type-span-diagram → codomain-span-diagram + right-map-span-diagram = + right-map-span span-span-diagram +``` + +### The span diagram obtained from a morphism of arrows + +Given maps `f : A → B` and `g : X → Y` and a morphism of arrows `α : f → g`, the +span diagram associated to `α` is the span diagram + +```text + f α₀ + B <----- A -----> X. +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} + (f : A → B) (g : X → Y) (α : hom-arrow f g) + where + + domain-span-diagram-hom-arrow : UU l2 + domain-span-diagram-hom-arrow = B + + codomain-span-diagram-hom-arrow : UU l3 + codomain-span-diagram-hom-arrow = X + + spanning-type-hom-arrow : UU l1 + spanning-type-hom-arrow = A + + left-map-span-diagram-hom-arrow : + spanning-type-hom-arrow → domain-span-diagram-hom-arrow + left-map-span-diagram-hom-arrow = f + + right-map-span-diagram-hom-arrow : + spanning-type-hom-arrow → codomain-span-diagram-hom-arrow + right-map-span-diagram-hom-arrow = map-domain-hom-arrow f g α + + span-hom-arrow : + span l1 B X + pr1 span-hom-arrow = A + pr1 (pr2 span-hom-arrow) = left-map-span-diagram-hom-arrow + pr2 (pr2 span-hom-arrow) = right-map-span-diagram-hom-arrow + + span-diagram-hom-arrow : span-diagram l2 l3 l1 + pr1 span-diagram-hom-arrow = domain-span-diagram-hom-arrow + pr1 (pr2 span-diagram-hom-arrow) = codomain-span-diagram-hom-arrow + pr2 (pr2 span-diagram-hom-arrow) = span-hom-arrow +``` + +## See also + +- [Cospan diagrams](foundation.cospan-diagrams.md) +- [Diagonal span diagrams](foundation.diagonal-span-diagrams.md) +- [Extensions of span diagrams](foundation.operations-span-diagrams.md) +- [Kernel span diagrams of maps](foundation.kernel-span-diagrams-of-maps.md) +- [Spans of families of types](foundation.spans-families-of-types.md) +- [Transposition of span diagrams](foundation.transposition-span-diagrams.md) diff --git a/src/foundation/spans-families-of-types.lagda.md b/src/foundation/spans-families-of-types.lagda.md new file mode 100644 index 0000000000..9a6b00a030 --- /dev/null +++ b/src/foundation/spans-families-of-types.lagda.md @@ -0,0 +1,62 @@ +# Spans of families of types + +```agda +module foundation.spans-families-of-types where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.universe-levels + +open import foundation-core.equivalences +open import foundation-core.function-types +``` + +
+ +## Idea + +Consider a family of types `A i` indexed by `i : I`. A +{{#concept "span" Disambiguation="family of types" Agda=span-type-family}} on +`A` consists of a type `S` equipped with a family of maps + +```text + (i : I) → S → A i. +``` + +The type `S` is called the +{{#concept "spanning type" Disambiguation="span of family of types" Agda=spanning-type-span-type-family}} +of the span. + +## Definitions + +### Spans on families of types + +```agda +module _ + {l1 l2 : Level} (l3 : Level) {I : UU l1} (A : I → UU l2) + where + + span-type-family : UU (l1 ⊔ l2 ⊔ lsuc l3) + span-type-family = Σ (UU l3) (λ S → (i : I) → S → A i) + +module _ + {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} + (s : span-type-family l3 A) + where + + spanning-type-span-type-family : UU l3 + spanning-type-span-type-family = pr1 s + + map-span-type-family : + (i : I) → spanning-type-span-type-family → A i + map-span-type-family = pr2 s +``` + +## See also + +- [(Binary) spans](foundation.spans.md) +- [Span diagrams on families of types](foundation.span-diagrams-families-of-types.md) +- [Permutations of spans of on families of types](foundation.permutations-spans-families-of-types.md) diff --git a/src/foundation/spans.lagda.md b/src/foundation/spans.lagda.md index 045eb68435..385e0b9da2 100644 --- a/src/foundation/spans.lagda.md +++ b/src/foundation/spans.lagda.md @@ -8,197 +8,79 @@ module foundation.spans where ```agda open import foundation.dependent-pair-types -open import foundation.equivalences -open import foundation.fundamental-theorem-of-identity-types -open import foundation.homotopy-induction -open import foundation.structure-identity-principle -open import foundation.type-arithmetic-dependent-pair-types -open import foundation.type-duality -open import foundation.univalence -open import foundation.universal-property-dependent-pair-types open import foundation.universe-levels open import foundation-core.cartesian-product-types -open import foundation-core.commuting-triangles-of-maps -open import foundation-core.contractible-types open import foundation-core.function-types -open import foundation-core.functoriality-dependent-function-types -open import foundation-core.functoriality-dependent-pair-types -open import foundation-core.homotopies -open import foundation-core.identity-types -open import foundation-core.torsorial-type-families -open import foundation-core.type-theoretic-principle-of-choice ```
## Idea -A **span** is a pair of functions with a common domain. - -## Definition - -### Spans +A {{#concept "binary span" Agda=span}} from `A` to `B` consists of a +{{#concept "spanning type" Disambiguation="binary span" Agda=spanning-type-span}} +`S` and a [pair](foundation.dependent-pair-types.md) of functions `f : S → A` +and `g : S → B`. The types `A` and `B` in the specification of a binary span are +also referred to as the {{#concept "domain" Disambiguation="binary span"}} and +{{#concept "codomain" Disambiguation="binary span"}} of the span, respectively. + +In [`foundation.binary-type-duality`](foundation.binary-type-duality.md) we show +that [binary relations](foundation.binary-relations.md) are equivalently +described as spans of types. + +We disambiguate between spans and [span diagrams](foundation.span-diagrams.md). +We consider spans from `A` to `B` to be _morphisms_ from `A` to `B` in the +category of types and spans between them, whereas we consider span diagrams to +be _objects_ in the category of diagrams of types of the form +`* <---- * ----> *`. Conceptually there is a subtle, but important distinction +between spans and span diagrams. As mentioned previously, a span from `A` to `B` +is equivalently described as a binary relation from `A` to `B`. On the other +hand, span diagrams are more suitable for functorial operations that take +"spans" as input, but for which the functorial action takes a natural +transformation, i.e., a morphism of span diagrams, as input. Examples of this +kind include [pushouts](synthetic-homotopy-theory.pushouts.md). + +## Definitions + +### (Binary) spans ```agda span : - {l1 l2 : Level} (l : Level) (A : UU l1) (B : UU l2) → - UU (l1 ⊔ l2 ⊔ lsuc l) -span l A B = - Σ (UU l) (λ X → (X → A) × (X → B)) + {l1 l2 : Level} (l : Level) (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2 ⊔ lsuc l) +span l A B = Σ (UU l) (λ X → (X → A) × (X → B)) module _ - {l1 l2 : Level} {l : Level} {A : UU l1} {B : UU l2} (c : span l A B) + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} + (c : span l3 A B) where - domain-span : UU l - domain-span = pr1 c + spanning-type-span : UU l3 + spanning-type-span = pr1 c - left-map-span : domain-span → A + left-map-span : spanning-type-span → A left-map-span = pr1 (pr2 c) - right-map-span : domain-span → B + right-map-span : spanning-type-span → B right-map-span = pr2 (pr2 c) ``` -### Homomorphisms between spans with fixed codomains - -One notion of homomorphism of spans `c` and `d` with common codomains is a map -between their domains so that the triangles on either side commute: - -```text - A ===== A - ^ ^ - | | - C ----> D - | | - v v - B ===== B -``` - -```agda -module _ - {l1 l2 : Level} {l : Level} {A : UU l1} {B : UU l2} - where - - coherence-hom-domain-span : - (c d : span l A B) → (domain-span c → domain-span d) → UU (l1 ⊔ l2 ⊔ l) - coherence-hom-domain-span c d h = - ( coherence-triangle-maps (left-map-span c) (left-map-span d) h) × - ( coherence-triangle-maps (right-map-span c) (right-map-span d) h) - - hom-domain-span : (c d : span l A B) → UU (l1 ⊔ l2 ⊔ l) - hom-domain-span c d = - Σ (domain-span c → domain-span d) (coherence-hom-domain-span c d) -``` - -### Characterizing equality of spans - -```agda -module _ - {l1 l2 : Level} (l : Level) (A : UU l1) (B : UU l2) - where - - htpy-span : (c d : span l A B) → UU (l1 ⊔ l2 ⊔ l) - htpy-span c d = - Σ ( domain-span c ≃ domain-span d) - ( λ e → coherence-hom-domain-span c d (map-equiv e)) - - refl-htpy-span : (c : span l A B) → htpy-span c c - pr1 (refl-htpy-span c) = id-equiv - pr1 (pr2 (refl-htpy-span c)) = refl-htpy - pr2 (pr2 (refl-htpy-span c)) = refl-htpy - - htpy-eq-span : (c d : span l A B) → c = d → htpy-span c d - htpy-eq-span c .c refl = refl-htpy-span c - - is-torsorial-htpy-span : - (c : span l A B) → is-torsorial (htpy-span c) - is-torsorial-htpy-span c = - is-torsorial-Eq-structure - ( is-torsorial-equiv (pr1 c)) - ( domain-span c , id-equiv) - ( is-torsorial-Eq-structure - ( is-torsorial-htpy (left-map-span c)) - ( left-map-span c , refl-htpy) - (is-torsorial-htpy (right-map-span c))) - - is-equiv-htpy-eq-span : - (c d : span l A B) → is-equiv (htpy-eq-span c d) - is-equiv-htpy-eq-span c = - fundamental-theorem-id (is-torsorial-htpy-span c) (htpy-eq-span c) - - extensionality-span : - (c d : span l A B) → (c = d) ≃ (htpy-span c d) - pr1 (extensionality-span c d) = htpy-eq-span c d - pr2 (extensionality-span c d) = is-equiv-htpy-eq-span c d - - eq-htpy-span : (c d : span l A B) → htpy-span c d → c = d - eq-htpy-span c d = map-inv-equiv (extensionality-span c d) -``` - -### Spans are equivalent to binary relations - -Using the principles of [type duality](foundation.type-duality.md) and -[type theoretic principle of choice](foundation.type-theoretic-principle-of-choice.md), -we can show that the type of spans `A <-- S --> B` is -[equivalent](foundation.equivalences.md) to the type of type-valued binary -relations `A → B → 𝓤`. +### Identity spans ```agda module _ - { l1 l2 l : Level} (A : UU l1) (B : UU l2) + {l1 : Level} {X : UU l1} where - equiv-span-binary-relation : - ( A → B → UU (l1 ⊔ l2 ⊔ l)) ≃ span (l1 ⊔ l2 ⊔ l) A B - equiv-span-binary-relation = - ( associative-Σ (UU (l1 ⊔ l2 ⊔ l)) (λ X → X → A) (λ T → pr1 T → B)) ∘e - ( equiv-Σ (λ T → pr1 T → B) (equiv-Pr1 (l2 ⊔ l) A) (λ P → equiv-ind-Σ)) ∘e - ( distributive-Π-Σ) ∘e - ( equiv-Π-equiv-family - ( λ a → equiv-Pr1 (l1 ⊔ l) B)) - - span-binary-relation : - ( A → B → UU (l1 ⊔ l2 ⊔ l)) → span (l1 ⊔ l2 ⊔ l) A B - pr1 (span-binary-relation R) = Σ A (λ a → Σ B (λ b → R a b)) - pr1 (pr2 (span-binary-relation R)) = pr1 - pr2 (pr2 (span-binary-relation R)) = pr1 ∘ pr2 - - compute-span-binary-relation : - map-equiv equiv-span-binary-relation ~ span-binary-relation - compute-span-binary-relation = refl-htpy - - binary-relation-span : - span (l1 ⊔ l2 ⊔ l) A B → (A → B → UU (l1 ⊔ l2 ⊔ l)) - binary-relation-span S a b = - Σ ( domain-span S) - ( λ s → (left-map-span S s = a) × (right-map-span S s = b)) - - compute-binary-relation-span : - map-inv-equiv equiv-span-binary-relation ~ binary-relation-span - compute-binary-relation-span S = - inv - ( map-eq-transpose-equiv equiv-span-binary-relation - ( eq-htpy-span - ( l1 ⊔ l2 ⊔ l) - ( A) - ( B) - ( _) - ( _) - ( ( equiv-pr1 (λ s → is-torsorial-path (left-map-span S s))) ∘e - ( equiv-left-swap-Σ) ∘e - ( equiv-tot - ( λ a → - ( equiv-tot - ( λ s → - equiv-pr1 (λ _ → is-torsorial-path (right-map-span S s)) ∘e - equiv-left-swap-Σ)) ∘e - ( equiv-left-swap-Σ))) , - ( inv-htpy (pr1 ∘ pr2 ∘ pr2 ∘ pr2)) , - ( inv-htpy (pr2 ∘ pr2 ∘ pr2 ∘ pr2))))) + id-span : span l1 X X + pr1 id-span = X + pr1 (pr2 id-span) = id + pr2 (pr2 id-span) = id ``` ## See also -- The formal dual of spans is [cospans](foundation.cospans.md). +- [Binary type duality](foundation.binary-type-duality.md) +- [Cospans](foundation.cospans.md) +- [Span diagrams](foundation.span-diagrams.md) +- [Spans of families of types](foundation.spans-families-of-types.md) diff --git a/src/foundation/terminal-spans-families-of-types.lagda.md b/src/foundation/terminal-spans-families-of-types.lagda.md new file mode 100644 index 0000000000..6b08b3e90f --- /dev/null +++ b/src/foundation/terminal-spans-families-of-types.lagda.md @@ -0,0 +1,45 @@ +# Terminal spans on families of types + +```agda +module foundation.terminal-spans-families-of-types where +``` + +
Imports + +```agda +open import foundation.contractible-types +open import foundation.morphisms-spans-families-of-types +open import foundation.spans-families-of-types +open import foundation.universe-levels +``` + +
+ +## Idea + +A [span](foundation.spans-families-of-types.md) `𝒮` on a family of types +`A : I → 𝒰` is said to be +{{#concept "terminal" Disambiguation="span on a family of types" Agda=is-terminal-span-type-family}} +if for each span `𝒯` on `A` the type of +[morphisms of spans](foundation.morphisms-spans-families-of-types.md) `𝒯 → 𝒮` is +[contractible](foundation-core.contractible-types.md). + +## Definitions + +### The predicate of being a terminal span on a family of types + +```agda +module _ + {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} (𝒮 : span-type-family l3 A) + where + + is-terminal-span-type-family : UUω + is-terminal-span-type-family = + {l : Level} (𝒯 : span-type-family l A) → + is-contr (hom-span-type-family 𝒯 𝒮) +``` + +## See also + +- [The universal property of dependent function types](foundation.universal-property-dependent-function-types.md) + is equivalent to the condition of being a terminal span of families of types. diff --git a/src/foundation/total-partial-elements.lagda.md b/src/foundation/total-partial-elements.lagda.md index 16df4f4925..e12c7cd6f5 100644 --- a/src/foundation/total-partial-elements.lagda.md +++ b/src/foundation/total-partial-elements.lagda.md @@ -17,8 +17,8 @@ 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 +{{#concept "total" Disambiguation="partial element" Agda=total-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 diff --git a/src/foundation/transport-along-equivalences.lagda.md b/src/foundation/transport-along-equivalences.lagda.md index ba733e4e1d..102886ea06 100644 --- a/src/foundation/transport-along-equivalences.lagda.md +++ b/src/foundation/transport-along-equivalences.lagda.md @@ -13,14 +13,19 @@ open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.equivalence-extensionality open import foundation.equivalence-induction +open import foundation.equivalences open import foundation.transport-along-identifications open import foundation.univalence open import foundation.universe-levels -open import foundation-core.equivalences +open import foundation-core.commuting-triangles-of-maps +open import foundation-core.function-extensionality open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types +open import foundation-core.injective-maps +open import foundation-core.retractions +open import foundation-core.sections ```
@@ -30,8 +35,8 @@ open import foundation-core.identity-types Applying [transport along identifications](foundation-core.transport-along-identifications.md) to [identifications](foundation-core.identity-types.md) arising from the -[univalence axiom](foundation.univalence.md) gives us **transport along -equivalences**. +[univalence axiom](foundation.univalence.md) gives us +{{#concept "transport along equivalences" Agda=tr-equiv}}. Since transport defines [equivalences](foundation-core.equivalences.md) of [fibers](foundation-core.fibers-of-maps.md), this gives us an _action on @@ -41,123 +46,171 @@ to get another [action on equivalences](foundation.action-on-equivalences-functions.md), but luckily, these two notions coincide. -## Definition +## Definitions + +### Transporting along equivalences ```agda -map-tr-equiv : - {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} → - X ≃ Y → f X → f Y -map-tr-equiv f e = tr f (eq-equiv e) +module _ + {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} + where + + map-tr-equiv : X ≃ Y → f X → f Y + map-tr-equiv e = tr f (eq-equiv e) + + abstract + is-equiv-map-tr-equiv : (e : X ≃ Y) → is-equiv (map-tr-equiv e) + is-equiv-map-tr-equiv e = is-equiv-tr f (eq-equiv e) + + tr-equiv : X ≃ Y → f X ≃ f Y + pr1 (tr-equiv e) = map-tr-equiv e + pr2 (tr-equiv e) = is-equiv-map-tr-equiv e + + eq-tr-equiv : X ≃ Y → f X = f Y + eq-tr-equiv = eq-equiv ∘ tr-equiv +``` -is-equiv-map-tr-equiv : +### Transporting along inverse equivalences + +```agda +module _ {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} - (e : X ≃ Y) → is-equiv (map-tr-equiv f e) -is-equiv-map-tr-equiv f e = is-equiv-tr f (eq-equiv e) - -tr-equiv : - {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} → - X ≃ Y → f X ≃ f Y -pr1 (tr-equiv f e) = map-tr-equiv f e -pr2 (tr-equiv f e) = is-equiv-map-tr-equiv f e - -eq-tr-equiv : - {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} → - X ≃ Y → f X = f Y -eq-tr-equiv f = eq-equiv ∘ tr-equiv f + where + + map-tr-inv-equiv : X ≃ Y → f Y → f X + map-tr-inv-equiv e = tr f (eq-equiv (inv-equiv e)) + + abstract + is-equiv-map-tr-inv-equiv : (e : X ≃ Y) → is-equiv (map-tr-inv-equiv e) + is-equiv-map-tr-inv-equiv e = is-equiv-tr f (eq-equiv (inv-equiv e)) + + tr-inv-equiv : X ≃ Y → f Y ≃ f X + pr1 (tr-inv-equiv e) = map-tr-inv-equiv e + pr2 (tr-inv-equiv e) = is-equiv-map-tr-inv-equiv e + + eq-tr-inv-equiv : X ≃ Y → f Y = f X + eq-tr-inv-equiv = eq-equiv ∘ tr-inv-equiv ``` +## Properties + ### Transporting along `id-equiv` is the identity equivalence ```agda -compute-map-tr-equiv-id-equiv : - {l1 l2 : Level} (f : UU l1 → UU l2) {X : UU l1} → - map-tr-equiv f id-equiv = id -compute-map-tr-equiv-id-equiv f {X} = ap (tr f) (compute-eq-equiv-id-equiv X) - -compute-tr-equiv-id-equiv : - {l1 l2 : Level} (f : UU l1 → UU l2) {X : UU l1} → - tr-equiv f id-equiv = id-equiv -compute-tr-equiv-id-equiv f {X} = - (ap (equiv-tr f) (compute-eq-equiv-id-equiv X)) ∙ (equiv-tr-refl f) +module _ + {l1 l2 : Level} (f : UU l1 → UU l2) {X : UU l1} + where + + compute-map-tr-equiv-id-equiv : map-tr-equiv f id-equiv = id + compute-map-tr-equiv-id-equiv = ap (tr f) (compute-eq-equiv-id-equiv X) + + compute-tr-equiv-id-equiv : tr-equiv f id-equiv = id-equiv + compute-tr-equiv-id-equiv = + is-injective-map-equiv (ap (tr f) (compute-eq-equiv-id-equiv X)) ``` ### Transport along equivalences preserves composition of equivalences -```agda -distributive-map-tr-equiv-equiv-comp : - {l1 l2 : Level} (f : UU l1 → UU l2) - {X Y Z : UU l1} (e : X ≃ Y) (e' : Y ≃ Z) → - map-tr-equiv f (e' ∘e e) ~ (map-tr-equiv f e' ∘ map-tr-equiv f e) -distributive-map-tr-equiv-equiv-comp f e e' x = - ( ap (λ p → tr f p x) (inv (compute-eq-equiv-comp-equiv e e'))) ∙ - ( tr-concat (eq-equiv e) (eq-equiv e') x) +For any operation `f : 𝒰₁ → 𝒰₂` and any two composable equivalences `e : X ≃ Y` +and `e' : Y ≃ Z` in `𝒰₁` we obtain a commuting triangle + +```text + tr-equiv f e + f X ----------> f Y + \ / + tr-equiv f (e' ∘ e) \ / tr-equiv f e' + \ / + ∨ ∨ + f Z +``` -distributive-tr-equiv-equiv-comp : +```agda +module _ {l1 l2 : Level} (f : UU l1 → UU l2) - {X Y Z : UU l1} (e : X ≃ Y) (e' : Y ≃ Z) → - tr-equiv f (e' ∘e e) = (tr-equiv f e' ∘e tr-equiv f e) -distributive-tr-equiv-equiv-comp f e e' = - eq-htpy-equiv (distributive-map-tr-equiv-equiv-comp f e e') + {X Y Z : UU l1} (e : X ≃ Y) (e' : Y ≃ Z) + where + + distributive-map-tr-equiv-equiv-comp : + coherence-triangle-maps + ( map-tr-equiv f (e' ∘e e)) + ( map-tr-equiv f e') + ( map-tr-equiv f e) + distributive-map-tr-equiv-equiv-comp x = + ( inv (ap (λ p → tr f p x) (compute-eq-equiv-comp-equiv e e'))) ∙ + ( tr-concat (eq-equiv e) (eq-equiv e') x) + + distributive-tr-equiv-equiv-comp : + tr-equiv f (e' ∘e e) = tr-equiv f e' ∘e tr-equiv f e + distributive-tr-equiv-equiv-comp = + eq-htpy-equiv distributive-map-tr-equiv-equiv-comp ``` -### Transporting along an equivalence and its inverse is just the identity +### Transporting along an inverse equivalence is inverse to transporting along the original equivalence ```agda -is-section-map-tr-equiv : - {l1 l2 : Level} (f : UU l1 → UU l2) - {X Y : UU l1} (e : X ≃ Y) → - (map-tr-equiv f (inv-equiv e) ∘ map-tr-equiv f e) ~ id -is-section-map-tr-equiv f e x = - ( ap - ( λ p → tr f p (map-tr-equiv f e x)) - ( inv (commutativity-inv-eq-equiv e))) ∙ - ( is-retraction-inv-tr f (eq-equiv e) x) - -is-retraction-map-tr-equiv : +module _ {l1 l2 : Level} (f : UU l1 → UU l2) - {X Y : UU l1} (e : X ≃ Y) → - (map-tr-equiv f e ∘ map-tr-equiv f (inv-equiv e)) ~ id -is-retraction-map-tr-equiv f e x = - ( ap - ( map-tr-equiv f e ∘ (λ p → tr f p x)) - ( inv (commutativity-inv-eq-equiv e))) ∙ - ( is-section-inv-tr f (eq-equiv e) x) + {X Y : UU l1} (e : X ≃ Y) + where + + is-section-map-tr-inv-equiv : + is-section (map-tr-equiv f e) (map-tr-equiv f (inv-equiv e)) + is-section-map-tr-inv-equiv x = + ( inv + ( ap + ( map-tr-equiv f e ∘ (λ p → tr f p x)) + ( commutativity-inv-eq-equiv e))) ∙ + ( is-section-inv-tr f (eq-equiv e) x) + + is-retraction-map-tr-inv-equiv : + is-retraction (map-tr-equiv f e) (map-tr-equiv f (inv-equiv e)) + is-retraction-map-tr-inv-equiv x = + ( inv + ( ap + ( λ p → tr f p (map-tr-equiv f e x)) + ( commutativity-inv-eq-equiv e))) ∙ + ( is-retraction-inv-tr f (eq-equiv e) x) ``` ### Transposing transport along the inverse of an equivalence ```agda -eq-transpose-map-tr-equiv : +module _ {l1 l2 : Level} (f : UU l1 → UU l2) - {X Y : UU l1} (e : X ≃ Y) {u : f X} {v : f Y} → - v = map-tr-equiv f e u → map-tr-equiv f (inv-equiv e) v = u -eq-transpose-map-tr-equiv f e {u} p = - (ap (map-tr-equiv f (inv-equiv e)) p) ∙ (is-section-map-tr-equiv f e u) - -eq-transpose-map-tr-equiv' : - {l1 l2 : Level} (f : UU l1 → UU l2) - {X Y : UU l1} (e : X ≃ Y) {u : f X} {v : f Y} → - map-tr-equiv f e u = v → u = map-tr-equiv f (inv-equiv e) v -eq-transpose-map-tr-equiv' f e {u} p = - (inv (is-section-map-tr-equiv f e u)) ∙ (ap (map-tr-equiv f (inv-equiv e)) p) + {X Y : UU l1} (e : X ≃ Y) {u : f X} {v : f Y} + where + + eq-transpose-map-tr-equiv : + v = map-tr-equiv f e u → map-tr-equiv f (inv-equiv e) v = u + eq-transpose-map-tr-equiv p = + ap (map-tr-equiv f (inv-equiv e)) p ∙ is-retraction-map-tr-inv-equiv f e u + + eq-transpose-map-tr-equiv' : + map-tr-equiv f e u = v → u = map-tr-equiv f (inv-equiv e) v + eq-transpose-map-tr-equiv' p = + ( inv (is-retraction-map-tr-inv-equiv f e u)) ∙ + ( ap (map-tr-equiv f (inv-equiv e)) p) ``` ### Substitution law for transport along equivalences ```agda -substitution-map-tr-equiv : - {l1 l2 l3 : Level} (g : UU l2 → UU l3) (f : UU l1 → UU l2) {X Y : UU l1} - (e : X ≃ Y) → - map-tr-equiv g (action-equiv-family f e) ~ map-tr-equiv (g ∘ f) e -substitution-map-tr-equiv g f e X' = - ( ap (λ p → tr g p X') (is-retraction-eq-equiv (action-equiv-function f e))) ∙ - ( substitution-law-tr g f (eq-equiv e)) - -substitution-law-tr-equiv : +module _ {l1 l2 l3 : Level} (g : UU l2 → UU l3) (f : UU l1 → UU l2) {X Y : UU l1} - (e : X ≃ Y) → tr-equiv g (action-equiv-family f e) = tr-equiv (g ∘ f) e -substitution-law-tr-equiv g f e = - eq-htpy-equiv (substitution-map-tr-equiv g f e) + (e : X ≃ Y) + where + + substitution-map-tr-equiv : + map-tr-equiv g (action-equiv-family f e) ~ map-tr-equiv (g ∘ f) e + substitution-map-tr-equiv X' = + ( ap + ( λ p → tr g p X') + ( is-retraction-eq-equiv (action-equiv-function f e))) ∙ + ( substitution-law-tr g f (eq-equiv e)) + + substitution-law-tr-equiv : + tr-equiv g (action-equiv-family f e) = tr-equiv (g ∘ f) e + substitution-law-tr-equiv = eq-htpy-equiv substitution-map-tr-equiv ``` ### Transporting along the action on equivalences of a function @@ -178,18 +231,21 @@ compute-map-tr-equiv-action-equiv-family {D = D} f g {X} e X' = ### Transport along equivalences and the action on equivalences in the universe coincide ```agda -eq-tr-equiv-action-equiv-family : - {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} → - (e : X ≃ Y) → tr-equiv f e = action-equiv-family f e -eq-tr-equiv-action-equiv-family f {X} = - ind-equiv - ( λ Y e → tr-equiv f e = action-equiv-family f e) - ( compute-tr-equiv-id-equiv f ∙ - inv (compute-action-equiv-family-id-equiv f)) - -eq-map-tr-equiv-map-action-equiv-family : - {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} → - (e : X ≃ Y) → map-tr-equiv f e = map-action-equiv-family f e -eq-map-tr-equiv-map-action-equiv-family f e = - ap map-equiv (eq-tr-equiv-action-equiv-family f e) +module _ + {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1} (e : X ≃ Y) + where + + eq-tr-equiv-action-equiv-family : + tr-equiv f e = action-equiv-family f e + eq-tr-equiv-action-equiv-family = + ind-equiv + ( λ Y d → tr-equiv f d = action-equiv-family f d) + ( compute-tr-equiv-id-equiv f ∙ + inv (compute-action-equiv-family-id-equiv f)) + ( e) + + eq-map-tr-equiv-map-action-equiv-family : + map-tr-equiv f e = map-action-equiv-family f e + eq-map-tr-equiv-map-action-equiv-family = + ap map-equiv eq-tr-equiv-action-equiv-family ``` diff --git a/src/foundation/transposition-span-diagrams.lagda.md b/src/foundation/transposition-span-diagrams.lagda.md new file mode 100644 index 0000000000..1d9df617ee --- /dev/null +++ b/src/foundation/transposition-span-diagrams.lagda.md @@ -0,0 +1,55 @@ +# Transposition of span diagrams + +```agda +module foundation.transposition-span-diagrams where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.opposite-spans +open import foundation.span-diagrams +open import foundation.spans +open import foundation.universe-levels +``` + +
+ +## Idea + +The +{{#concept "trasposition" Disambiguation="span diagram" Agda=transposition-span-diagram}} +of a [span diagram](foundation.span-diagrams.md) + +```text + f g + A <----- S -----> B +``` + +is the span diagram + +```text + g f + B <----- S -----> A. +``` + +In other words, the transposition of a span diagram `(A , B , s)` is the span +diagram `(B , A , opposite-span s)` where `opposite-span s` is the +[opposite](foundation.opposite-spans.md) of the [span](foundation.spans.md) `s` +from `A` to `B`. + +## Definitions + +### Transposition of span diagrams + +```agda +module _ + {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3) + where + + transposition-span-diagram : span-diagram l2 l1 l3 + pr1 transposition-span-diagram = codomain-span-diagram 𝒮 + pr1 (pr2 transposition-span-diagram) = domain-span-diagram 𝒮 + pr2 (pr2 transposition-span-diagram) = opposite-span (span-span-diagram 𝒮) +``` diff --git a/src/foundation/truncated-maps.lagda.md b/src/foundation/truncated-maps.lagda.md index 105179f41a..5107b35a68 100644 --- a/src/foundation/truncated-maps.lagda.md +++ b/src/foundation/truncated-maps.lagda.md @@ -9,7 +9,7 @@ open import foundation-core.truncated-maps public
Imports ```agda -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.functoriality-fibers-of-maps open import foundation.universe-levels diff --git a/src/foundation/type-duality.lagda.md b/src/foundation/type-duality.lagda.md index 0523403a74..9010140341 100644 --- a/src/foundation/type-duality.lagda.md +++ b/src/foundation/type-duality.lagda.md @@ -307,3 +307,9 @@ fiber-Σ {l1} {l2} X A = ( is-small-lmax l2 X)) ∘e ( equiv-precomp (inv-equiv (equiv-is-small (is-small-lmax l2 X))) A) ``` + +## See also + +- In [`foundation.binary-type-duality`](foundation.binary-type-duality.md) we + show that [binary relations](foundation.binary-relations.md) are equivalently + described as [spans of types](foundation.spans.md). diff --git a/src/foundation/univalence.lagda.md b/src/foundation/univalence.lagda.md index 2deb627f00..1df7bab84c 100644 --- a/src/foundation/univalence.lagda.md +++ b/src/foundation/univalence.lagda.md @@ -96,6 +96,10 @@ equivalences out of a type `A` is contractible can therefore be stated more succinctly as the claim that the family of equivalences out of `A` is torsorial. ```agda +module _ + {l : Level} + where + abstract is-torsorial-equiv : (A : UU l) → is-torsorial (λ (X : UU l) → A ≃ X) @@ -164,7 +168,7 @@ compute-eq-equiv-comp-equiv : {l : Level} {A B C : UU l} (f : A ≃ B) (g : B ≃ C) → eq-equiv f ∙ eq-equiv g = eq-equiv (g ∘e f) compute-eq-equiv-comp-equiv f g = - is-injective-map-equiv + is-injective-equiv ( equiv-univalence) ( ( inv ( compute-equiv-eq-concat (eq-equiv f) (eq-equiv g))) ∙ ( ( ap @@ -179,7 +183,7 @@ compute-eq-equiv-comp-equiv f g = compute-equiv-eq-ap-inv : {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {x y : A} (p : x = y) → - map-equiv (equiv-eq (ap B (inv p)) ∘e (equiv-eq (ap B p))) ~ id + map-eq (ap B (inv p)) ∘ map-eq (ap B p) ~ id compute-equiv-eq-ap-inv refl = refl-htpy commutativity-inv-equiv-eq : @@ -191,7 +195,7 @@ commutativity-inv-eq-equiv : {l : Level} {A B : UU l} (f : A ≃ B) → inv (eq-equiv f) = eq-equiv (inv-equiv f) commutativity-inv-eq-equiv f = - is-injective-map-equiv + is-injective-equiv ( equiv-univalence) ( ( inv (commutativity-inv-equiv-eq (eq-equiv f))) ∙ ( ( ap diff --git a/src/foundation/universal-property-cartesian-product-types.lagda.md b/src/foundation/universal-property-cartesian-product-types.lagda.md index 7c68c09ab3..7bdb2ad2d4 100644 --- a/src/foundation/universal-property-cartesian-product-types.lagda.md +++ b/src/foundation/universal-property-cartesian-product-types.lagda.md @@ -7,7 +7,7 @@ module foundation.universal-property-cartesian-product-types where
Imports ```agda -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.unit-type open import foundation.universe-levels diff --git a/src/foundation/universal-property-dependent-function-types.lagda.md b/src/foundation/universal-property-dependent-function-types.lagda.md new file mode 100644 index 0000000000..c5a94e7de9 --- /dev/null +++ b/src/foundation/universal-property-dependent-function-types.lagda.md @@ -0,0 +1,125 @@ +# The universal property of dependent function types + +```agda +module foundation.universal-property-dependent-function-types where +``` + +
Imports + +```agda +open import foundation.contractible-maps +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.functoriality-dependent-function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.identity-types +open import foundation.spans-families-of-types +open import foundation.terminal-spans-families-of-types +open import foundation.universe-levels +``` + +
+ +## Idea + +Consider a family of types `B` over `A`. Then the dependent function type +`(a : A) → B a` naturally has the structure of a +[span](foundation.spans-families-of-types.md) on the family of types `B` over +`A`, where for each `a : A` the map + +```text + ((x : A) → B x) → B a +``` + +is given by evaluation at `a`. + +A span `𝒮 := (S , f)` is said to satisfy the +{{#concept "universal property of dependent function types" Agda=universal-property-dependent-function-types}} +if for any type `T` the map + +```text + (T → S) → ((x : A) → T → B x) +``` + +given by `h ↦ λ x t → f x (h t)` is an +[equivalence](foundation-core.equivalences.md). The dependent function type +`(x : A) → B x` equipped with the span structure defined above satisfies the +universal property of dependent function types. + +In +[`foundation.dependent-function-types`](foundation.dependent-function-types.md) +we show that dependent function types satisfy the universal property of +dependent function types. In this file we also show that the universal property +of dependent function types is equivalent to being a +[terminal span](foundation.terminal-spans-families-of-types.md) on the type +family `B`. + +## Definitions + +### The universal property of dependent function types + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (𝒮 : span-type-family l3 B) + where + + ev-span-type-family : + {l : Level} (T : UU l) → + (T → spanning-type-span-type-family 𝒮) → (x : A) → T → B x + ev-span-type-family T h x t = map-span-type-family 𝒮 x (h t) + + universal-property-dependent-function-types : UUω + universal-property-dependent-function-types = + {l : Level} (T : UU l) → is-equiv (ev-span-type-family T) +``` + +## Properties + +### A span on a family of types satisfies the universal property of dependent function types if and only if it is terminal + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (𝒮 : span-type-family l3 B) + where + + abstract + is-terminal-universal-property-dependent-function-types : + universal-property-dependent-function-types 𝒮 → + is-terminal-span-type-family 𝒮 + is-terminal-universal-property-dependent-function-types U 𝒯 = + is-contr-equiv' _ + ( equiv-tot + ( λ h → + ( equiv-Π-equiv-family + ( λ a → + ( equiv-Π-equiv-family (λ t → equiv-inv _ _)) ∘e + ( equiv-funext))) ∘e + ( equiv-funext))) + ( is-contr-map-is-equiv + ( U (spanning-type-span-type-family 𝒯)) + ( map-span-type-family 𝒯)) + + abstract + universal-property-dependent-function-types-is-terminal : + is-terminal-span-type-family 𝒮 → + universal-property-dependent-function-types 𝒮 + universal-property-dependent-function-types-is-terminal U T = + is-equiv-is-contr-map + ( λ g → + is-contr-equiv _ + ( equiv-tot + ( λ h → + ( equiv-Π-equiv-family + ( λ a → + ( equiv-Π-equiv-family (λ t → equiv-inv _ _)) ∘e + ( equiv-funext))) ∘e + ( equiv-funext))) + ( U (T , g))) +``` + +## See also + +- [Dependent function types](foundation.dependent-function-types.md) diff --git a/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md b/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md index 38d6def822..2d4e80b546 100644 --- a/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md +++ b/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md @@ -47,7 +47,7 @@ the type family `(fiber f) ∘ f : A → 𝒰`, which always has a section given We can uniquely characterize the family of fibers `fiber f : B → 𝒰` as the initial type family equipped with such a section. Explicitly, the -{{#concept "universal property of the family of fibers" Disambiguation="maps"}} +{{#concept "universal property of the family of fibers" Disambiguation="maps" Agda=universal-property-family-of-fibers}} `fiber f : B → 𝒰` of a map `f` is that the precomposition operation ```text @@ -92,8 +92,8 @@ for any binary type family `X : (b : B) → F b → 𝒰`. This evaluation map t binary family of elements of `X` to a [double lift](orthogonal-factorization-systems.double-lifts-families-of-elements.md) of `f` and `δ`. The -{{#concept "dependent universal property of the family of fibers of a map"}} `f` -asserts that this evaluation map is an equivalence. +{{#concept "dependent universal property of the family of fibers of a map" Agda=dependent-universal-property-family-of-fibers}} +`f` asserts that this evaluation map is an equivalence. ```agda module _ diff --git a/src/foundation/universal-property-fiber-products.lagda.md b/src/foundation/universal-property-fiber-products.lagda.md index 51957b589b..a666844b8a 100644 --- a/src/foundation/universal-property-fiber-products.lagda.md +++ b/src/foundation/universal-property-fiber-products.lagda.md @@ -7,7 +7,7 @@ module foundation.universal-property-fiber-products where
Imports ```agda -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types open import foundation.universe-levels diff --git a/src/foundation/universal-property-pullbacks.lagda.md b/src/foundation/universal-property-pullbacks.lagda.md index 64bcaf8830..9aab74f355 100644 --- a/src/foundation/universal-property-pullbacks.lagda.md +++ b/src/foundation/universal-property-pullbacks.lagda.md @@ -9,7 +9,7 @@ open import foundation-core.universal-property-pullbacks public
Imports ```agda -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.functoriality-cartesian-product-types diff --git a/src/graph-theory/acyclic-undirected-graphs.lagda.md b/src/graph-theory/acyclic-undirected-graphs.lagda.md index 029dbfd624..419d47ac09 100644 --- a/src/graph-theory/acyclic-undirected-graphs.lagda.md +++ b/src/graph-theory/acyclic-undirected-graphs.lagda.md @@ -18,8 +18,9 @@ open import graph-theory.undirected-graphs ## Idea -An {{#concept "acyclic undirected graph" WDID=Q3115453 WD="Acyclic graph"}} is -an [undirected graph](graph-theory.undirected-graphs.md) of which the +An +{{#concept "acyclic undirected graph" WDID=Q3115453 WD="Acyclic graph" Agda=is-acyclic-Undirected-Graph}} +is an [undirected graph](graph-theory.undirected-graphs.md) of which the [geometric realization](graph-theory.geometric-realizations-undirected-graphs.md) is [contractible](foundation-core.contractible-types.md). diff --git a/src/graph-theory/directed-graph-structures-on-standard-finite-sets.lagda.md b/src/graph-theory/directed-graph-structures-on-standard-finite-sets.lagda.md index 90c5e3d034..aaf64109e6 100644 --- a/src/graph-theory/directed-graph-structures-on-standard-finite-sets.lagda.md +++ b/src/graph-theory/directed-graph-structures-on-standard-finite-sets.lagda.md @@ -19,9 +19,10 @@ open import univalent-combinatorics.standard-finite-types ## Idea -A {{#concept "directed graph structure" WD="Directed graph" WDID=Q1137726}} on a -[standard finite set](univalent-combinatorics.standard-finite-types.md) `Fin n` -is a [binary type-valued relation](foundation.binary-relations.md) +A +{{#concept "directed graph structure" WD="Directed graph" WDID=Q1137726 Agda=structure-directed-graph-Fin}} +on a [standard finite set](univalent-combinatorics.standard-finite-types.md) +`Fin n` is a [binary type-valued relation](foundation.binary-relations.md) ```text Fin n → Fin n → 𝒰. diff --git a/src/orthogonal-factorization-systems/cd-structures.lagda.md b/src/orthogonal-factorization-systems/cd-structures.lagda.md index cfc9704567..6413398d29 100644 --- a/src/orthogonal-factorization-systems/cd-structures.lagda.md +++ b/src/orthogonal-factorization-systems/cd-structures.lagda.md @@ -18,7 +18,8 @@ open import foundation.universe-levels ## Idea A _cd-structure_ on a [category](category-theory.categories.md) consists of a -class `𝒟` of {{#concept "distinguished squares" Disambiguation="cd-structure"}} +class `𝒟` of +{{#concept "distinguished squares" Disambiguation="cd-structure" Agda=is-distinguished-square-cd-structure}} ```text i @@ -31,8 +32,8 @@ class `𝒟` of {{#concept "distinguished squares" Disambiguation="cd-structure" ``` On this page we will consider _internal_ cd-structures, i.e., cd-structure on -types. In other words, a {{#concept "cd-structure"}} is a family of -[subtypes](foundation-core.subtypes.md) +types. In other words, a {{#concept "cd-structure" Agda=cd-structure}} is a +family of [subtypes](foundation-core.subtypes.md) ```text (f : A → B) (g : X → Y) → hom-arrow f g → Prop, diff --git a/src/orthogonal-factorization-systems/double-lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/double-lifts-families-of-elements.lagda.md index acd8dc3b2d..54b283d49d 100644 --- a/src/orthogonal-factorization-systems/double-lifts-families-of-elements.lagda.md +++ b/src/orthogonal-factorization-systems/double-lifts-families-of-elements.lagda.md @@ -26,8 +26,8 @@ elements `a : (i : I) → A i` and consider a family of types Recall that `b` is also a [dependent lift](orthogonal-factorization-systems.lifts-families-of-elements.md) of the family of elements `a`. The type of -{{#concept "dependent double lifts" Disambiguation="family of elements"}} of `b` -and `a` to `C` is defined to be the type +{{#concept "dependent double lifts" Disambiguation="family of elements" Agda=dependent-double-lift-family-of-elements}} +of `b` and `a` to `C` is defined to be the type ```text (i : I) → C i (a i) (b i). @@ -38,8 +38,8 @@ lifts `a` and `b` to the type family `C`. The definition of (ordinary) double lifts is somewhat simpler: Given a lift `b` of `a : I → A` to a type family `B : A → 𝒰`, a -{{#concept "double lift" Disambiguation="families of elements"}} of `a` and `b` -to a type family +{{#concept "double lift" Disambiguation="families of elements" Agda=double-lift-family-of-elements}} +of `a` and `b` to a type family ```text C : (x : A) → B x → 𝒰 diff --git a/src/orthogonal-factorization-systems/extensions-double-lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/extensions-double-lifts-families-of-elements.lagda.md index 63ba294492..a577431bf1 100644 --- a/src/orthogonal-factorization-systems/extensions-double-lifts-families-of-elements.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-double-lifts-families-of-elements.lagda.md @@ -36,8 +36,8 @@ over `B` and a ``` of the lift `b` of `a`. An -{{#concept "extension" Disambiguation="dependent double family of elements"}} of -`b` to `A` consists of a family of elements +{{#concept "extension" Disambiguation="dependent double family of elements" Agda=extension-dependent-double-lift-family-of-elements}} +of `b` to `A` consists of a family of elements `f : (i : I) (x : A i) (y : B i x) → C i x y` equipped with a [homotopy](foundation-core.homotopies.md) witnessing that the [identification](foundation-core.identity-types.md) `f i (a i) (b i) = c i` diff --git a/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md index 6d5980be63..5c8a20cb5d 100644 --- a/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md +++ b/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md @@ -32,9 +32,9 @@ Consider a family of elements `a : I → A`, a type family `B` over `A` and a ``` of the family of elements `a`. An -{{#concept "extension" Disambiguation="family of elements"}} of `b` to `A` -consists of a family of elements `f : (x : A) → B x` equipped with a -[homotopy](foundation-core.homotopies.md) `f ∘ a ~ b`. +{{#concept "extension" Disambiguation="family of elements" Agda=extension-lift-family-of-elements}} +of `b` to `A` consists of a family of elements `f : (x : A) → B x` equipped with +a [homotopy](foundation-core.homotopies.md) `f ∘ a ~ b`. More generally, given a family of elements `a : (i : I) → A i`, a type family `B` over `A`, and a dependent lift @@ -44,8 +44,8 @@ More generally, given a family of elements `a : (i : I) → A i`, a type family ``` of the family of elements `A`, a -{{#concet "dependent extension" Disambiguation"family of elements"}} of `b` to -`A` consists of a family of elements +{{#concept "dependent extension" Disambiguation"family of elements" Agda=extension-dependent-lift-family-of-elements}} +of `b` to `A` consists of a family of elements ```text f : (i : I) (x : A i) → B i x diff --git a/src/orthogonal-factorization-systems/functoriality-pullback-hom.lagda.md b/src/orthogonal-factorization-systems/functoriality-pullback-hom.lagda.md index 91560febe5..df19e9ca89 100644 --- a/src/orthogonal-factorization-systems/functoriality-pullback-hom.lagda.md +++ b/src/orthogonal-factorization-systems/functoriality-pullback-hom.lagda.md @@ -10,7 +10,7 @@ module orthogonal-factorization-systems.functoriality-pullback-hom where open import foundation.fibered-maps open import foundation.function-types open import foundation.functoriality-pullbacks -open import foundation.morphisms-cospans +open import foundation.morphisms-cospan-diagrams open import foundation.postcomposition-functions open import foundation.precomposition-functions open import foundation.universe-levels @@ -40,7 +40,11 @@ module _ where map-pullback-hom : - hom-cospan (precomp f' Y') (postcomp A' g') (precomp f Y) (postcomp A g) → + hom-cospan-diagram + ( precomp f' Y') + ( postcomp A' g') + ( precomp f Y) + ( postcomp A g) → fibered-map f' g' → fibered-map f g map-pullback-hom = map-is-pullback diff --git a/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md index c0e5399585..9df8289124 100644 --- a/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md +++ b/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md @@ -31,8 +31,9 @@ Consider a type family and a family of elements `a : (i : I) → A i`. -A {{#concept "dependent lift" Disambiguation="family of elements"}} of the -family of elements `a` to the type family `B` is a family of elements +A +{{#concept "dependent lift" Disambiguation="family of elements" Agda=dependent-lift-family-of-elements}} +of the family of elements `a` to the type family `B` is a family of elements ```text (i : I) → B i (a i). @@ -40,8 +41,8 @@ family of elements `a` to the type family `B` is a family of elements An important special case occurs when `a : I → A` is a family of elements of a fixed type `A`, and `B` is a type family over `A`. In this case, a -{{#concept "lift" Disambiguation="family of elements"}} of the family of -elements `a` is a family of elements +{{#concept "lift" Disambiguation="family of elements" Agda=lift-family-of-elements}} +of the family of elements `a` is a family of elements ```text (i : I) → B (a i). diff --git a/src/orthogonal-factorization-systems/pullback-hom.lagda.md b/src/orthogonal-factorization-systems/pullback-hom.lagda.md index 073c337dc7..3a9d93683b 100644 --- a/src/orthogonal-factorization-systems/pullback-hom.lagda.md +++ b/src/orthogonal-factorization-systems/pullback-hom.lagda.md @@ -8,7 +8,7 @@ module orthogonal-factorization-systems.pullback-hom where ```agda open import foundation.action-on-identifications-functions -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.fibered-maps diff --git a/src/synthetic-homotopy-theory/26-descent.lagda.md b/src/synthetic-homotopy-theory/26-descent.lagda.md index 79e084feb2..5edcfe315e 100644 --- a/src/synthetic-homotopy-theory/26-descent.lagda.md +++ b/src/synthetic-homotopy-theory/26-descent.lagda.md @@ -10,7 +10,7 @@ module synthetic-homotopy-theory.26-descent where open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions open import foundation.commuting-squares-of-maps -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.constant-type-families open import foundation.contractible-maps open import foundation.contractible-types diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md index 16b4fef745..2d2b34123b 100644 --- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md +++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md @@ -9,7 +9,7 @@ module synthetic-homotopy-theory.acyclic-maps where ```agda open import foundation.action-on-identifications-functions open import foundation.cartesian-product-types -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.constant-maps open import foundation.contractible-maps open import foundation.contractible-types diff --git a/src/synthetic-homotopy-theory/dependent-pullback-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/dependent-pullback-property-pushouts.lagda.md index 2ff8d22e32..dbf09337bb 100644 --- a/src/synthetic-homotopy-theory/dependent-pullback-property-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-pullback-property-pushouts.lagda.md @@ -9,7 +9,7 @@ module synthetic-homotopy-theory.dependent-pullback-property-pushouts where ```agda open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.constant-type-families open import foundation.dependent-pair-types open import foundation.function-extensionality diff --git a/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md b/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md index d58496f31d..8000b52d60 100644 --- a/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md @@ -200,7 +200,7 @@ module _ dependent-cocone-dependent-suspension-structure htpy-map-inv-equiv-dependent-suspension-structure-suspension-cocone-cocone-dependent-cocone-dependent-suspension-structure ( d) = - is-injective-map-equiv + is-injective-equiv ( equiv-dependent-suspension-structure-suspension-cocone) ( is-section-map-inv-equiv ( equiv-dependent-suspension-structure-suspension-cocone) diff --git a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md index 1b37a284fb..18e760552b 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md @@ -31,8 +31,9 @@ open import synthetic-homotopy-theory.universal-property-pushouts ## Idea -The {{#concept "flattening lemma" Disambiguation="coequalizers"}} for -[coequalizers](synthetic-homotopy-theory.coequalizers.md) states that +The +{{#concept "flattening lemma" Disambiguation="coequalizers" Agda=flattening-lemma-coequalizer}} +for [coequalizers](synthetic-homotopy-theory.coequalizers.md) states that coequalizers commute with [dependent pair types](foundation.dependent-pair-types.md). More precisely, given a coequalizer diff --git a/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md index a628dbf880..60a39e8867 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-sequential-colimits.lagda.md @@ -33,7 +33,9 @@ open import synthetic-homotopy-theory.universal-property-sequential-colimits ## Idea -The {{#concept "flattening lemma" Disambiguation="sequential colimits"}} for +The +{{#concept "flattening lemma" Disambiguation="sequential colimits" Agda=flattening-lemma-sequential-colimit}} +for [sequential colimits](synthetic-homotopy-theory.universal-property-sequential-colimits.md) states that sequential colimits commute with [dependent pair types](foundation.dependent-pair-types.md). Specifically, given diff --git a/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md index 7ee4a8e6ba..101aa4e199 100644 --- a/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/pullback-property-pushouts.lagda.md @@ -8,7 +8,7 @@ module synthetic-homotopy-theory.pullback-property-pushouts where ```agda open import foundation.commuting-squares-of-maps -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.function-types open import foundation.precomposition-functions @@ -38,8 +38,8 @@ pushout of `S` if and only if the square ``` is a [pullback square](foundation.pullback-squares.md) for every type `Y`. -Below, we first define the [cone](foundation.cones-over-cospans.md) of this -[commuting square](foundation.commuting-squares-of-maps.md), and then we +Below, we first define the [cone](foundation.cones-over-cospan-diagrams.md) of +this [commuting square](foundation.commuting-squares-of-maps.md), and then we introduce the type `pullback-property-pushout`, which states that the above square is a [pullback](foundation-core.universal-property-pullbacks.md). diff --git a/src/synthetic-homotopy-theory/retracts-of-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/retracts-of-sequential-diagrams.lagda.md index 33a6e0ae22..13ad9399bb 100644 --- a/src/synthetic-homotopy-theory/retracts-of-sequential-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/retracts-of-sequential-diagrams.lagda.md @@ -29,8 +29,9 @@ open import synthetic-homotopy-theory.sequential-diagrams ## Idea -A {{#concept "retract" Disambiguation="sequential diagram"}} of sequential -diagrams `A` of `B` is a +A +{{#concept "retract" Disambiguation="sequential diagram" Agda=retract-sequential-diagram}} +of sequential diagrams `A` of `B` is a [morphism of sequential diagrams](synthetic-homotopy-theory.morphisms-sequential-diagrams.md) `B → A` that is a retraction. diff --git a/src/synthetic-homotopy-theory/suspension-structures.lagda.md b/src/synthetic-homotopy-theory/suspension-structures.lagda.md index 9ded1e1dee..6a3e59877e 100644 --- a/src/synthetic-homotopy-theory/suspension-structures.lagda.md +++ b/src/synthetic-homotopy-theory/suspension-structures.lagda.md @@ -241,7 +241,7 @@ module _ extensionality-suspension-structure-refl-htpy-suspension-structure : eq-htpy-suspension-structure refl-htpy-suspension-structure = refl extensionality-suspension-structure-refl-htpy-suspension-structure = - is-injective-map-equiv + is-injective-equiv ( extensionality-suspension-structure c c) ( is-section-map-inv-equiv ( extensionality-suspension-structure c c) diff --git a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md index f9e9f7385a..ac4e4cb5b7 100644 --- a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md +++ b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md @@ -9,7 +9,7 @@ module synthetic-homotopy-theory.truncated-acyclic-maps where ```agda open import foundation.action-on-identifications-functions open import foundation.cartesian-product-types -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.connected-maps open import foundation.connected-types open import foundation.constant-maps diff --git a/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md index 61273f1b7b..4211aa87a6 100644 --- a/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md @@ -12,7 +12,7 @@ module synthetic-homotopy-theory.universal-property-pushouts where open import foundation.action-on-identifications-functions open import foundation.commuting-cubes-of-maps open import foundation.commuting-squares-of-maps -open import foundation.cones-over-cospans +open import foundation.cones-over-cospan-diagrams open import foundation.contractible-maps open import foundation.contractible-types open import foundation.dependent-pair-types diff --git a/src/univalent-combinatorics/2-element-types.lagda.md b/src/univalent-combinatorics/2-element-types.lagda.md index 7501caf687..b15edfc919 100644 --- a/src/univalent-combinatorics/2-element-types.lagda.md +++ b/src/univalent-combinatorics/2-element-types.lagda.md @@ -238,7 +238,7 @@ abstract (inl (inr star)) (inl (inr star)) p q (inl (inr star)) = inv p is-retraction-aut-point-Fin-two-ℕ' e (inl (inr star)) (inl (inr star)) p q (inr star) = - ex-falso (Eq-Fin-eq 2 (is-injective-map-equiv e (p ∙ inv q))) + ex-falso (Eq-Fin-eq 2 (is-injective-equiv e (p ∙ inv q))) is-retraction-aut-point-Fin-two-ℕ' e (inl (inr star)) (inr star) p q (inl (inr star)) = inv p is-retraction-aut-point-Fin-two-ℕ' e @@ -249,10 +249,10 @@ abstract (inr star) (inl (inr star)) p q (inr star) = inv q is-retraction-aut-point-Fin-two-ℕ' e (inr star) (inr star) p q (inl (inr star)) = - ex-falso (Eq-Fin-eq 2 (is-injective-map-equiv e (p ∙ inv q))) + ex-falso (Eq-Fin-eq 2 (is-injective-equiv e (p ∙ inv q))) is-retraction-aut-point-Fin-two-ℕ' e (inr star) (inr star) p q (inr star) = - ex-falso (Eq-Fin-eq 2 (is-injective-map-equiv e (p ∙ inv q))) + ex-falso (Eq-Fin-eq 2 (is-injective-equiv e (p ∙ inv q))) is-retraction-aut-point-Fin-two-ℕ : (aut-point-Fin-two-ℕ ∘ ev-zero-aut-Fin-two-ℕ) ~ id @@ -544,10 +544,10 @@ cases-is-involution-aut-Fin-two-ℕ e (inl (inr star)) (inr star) (inl (inr star)) p q = ap (map-equiv e) p ∙ q cases-is-involution-aut-Fin-two-ℕ e (inl (inr star)) (inr star) (inr star) p q = - ex-falso (neq-inr-inl (is-injective-map-equiv e (q ∙ inv p))) + ex-falso (neq-inr-inl (is-injective-equiv e (q ∙ inv p))) cases-is-involution-aut-Fin-two-ℕ e (inr star) (inl (inr star)) (inl (inr star)) p q = - ex-falso (neq-inr-inl (is-injective-map-equiv e (p ∙ inv q))) + ex-falso (neq-inr-inl (is-injective-equiv e (p ∙ inv q))) cases-is-involution-aut-Fin-two-ℕ e (inr star) (inl (inr star)) (inr star) p q = ap (map-equiv e) p ∙ q cases-is-involution-aut-Fin-two-ℕ e (inr star) (inr star) z p q = @@ -656,7 +656,7 @@ module _ ( empty-Prop) ( λ f → neq-inr-inl - ( is-injective-map-equiv f + ( is-injective-equiv f ( htpy-eq-equiv (htpy-eq-equiv p' f) (zero-Fin 1)))) is-not-identity-swap-2-Element-Type : swap-2-Element-Type X ≠ id-equiv @@ -719,7 +719,7 @@ module _ f h y (inl (inr star)) (inl (inr star)) k3 p q r = tr ( λ z → map-equiv (swap-2-Element-Type X) z = z) - ( is-injective-map-equiv h (p ∙ inv q)) + ( is-injective-equiv h (p ∙ inv q)) ( P) f h y (inl (inr star)) (inr star) (inl (inr star)) p q r = ex-falso @@ -727,23 +727,23 @@ module _ ( inv p ∙ (ap (map-equiv h) (inv P) ∙ ( ap ( map-equiv (h ∘e (swap-2-Element-Type X))) - ( is-injective-map-equiv h (p ∙ inv r)) ∙ + ( is-injective-equiv h (p ∙ inv r)) ∙ ( ( ap ( map-equiv h) ( is-involution-aut-2-element-type X ( swap-2-Element-Type X) y)) ∙ ( q)))))) f h y (inl (inr star)) (inr star) (inr star) p q r = - ( is-injective-map-equiv h (r ∙ inv q)) + ( is-injective-equiv h (r ∙ inv q)) f h y (inr star) (inl (inr star)) (inl (inr star)) p q r = - ( is-injective-map-equiv h (r ∙ inv q)) + ( is-injective-equiv h (r ∙ inv q)) f h y (inr star) (inl (inr star)) (inr star) p q r = ex-falso ( neq-inr-inl ( inv p ∙ (ap (map-equiv h) (inv P) ∙ ( ap ( map-equiv (h ∘e (swap-2-Element-Type X))) - ( is-injective-map-equiv h (p ∙ inv r)) ∙ + ( is-injective-equiv h (p ∙ inv r)) ∙ ( ( ap ( map-equiv h) ( is-involution-aut-2-element-type X @@ -753,7 +753,7 @@ module _ f h y (inr star) (inr star) k3 p q r = tr ( λ z → map-equiv (swap-2-Element-Type X) z = z) - ( is-injective-map-equiv h (p ∙ inv q)) + ( is-injective-equiv h (p ∙ inv q)) ( P) ``` diff --git a/src/univalent-combinatorics/counting.lagda.md b/src/univalent-combinatorics/counting.lagda.md index 0ec67c276a..aec4b66b23 100644 --- a/src/univalent-combinatorics/counting.lagda.md +++ b/src/univalent-combinatorics/counting.lagda.md @@ -173,7 +173,7 @@ abstract is-one-number-of-elements-count-is-contr (pair (succ-ℕ (succ-ℕ k)) e) H = ex-falso ( Eq-Fin-eq (succ-ℕ (succ-ℕ k)) - ( is-injective-map-equiv e + ( is-injective-equiv e ( eq-is-contr' H ( map-equiv e (zero-Fin (succ-ℕ k))) ( map-equiv e (neg-one-Fin (succ-ℕ k)))))) diff --git a/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md b/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md index c4c8b668f2..9209a1d39a 100644 --- a/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md +++ b/src/univalent-combinatorics/orientations-complete-undirected-graph.lagda.md @@ -629,7 +629,7 @@ module _ ( λ h → pr1 Y ∘ (map-equiv h)) ( inv (left-inverse-law-equiv e))) ( eq-is-prop is-prop-type-trunc-Prop))) ∙ - ( ( is-injective-map-equiv e (pr1 (pair-eq-Σ p))) ∙ + ( ( is-injective-equiv e (pr1 (pair-eq-Σ p))) ∙ ( ap ( λ Y' → pr1 (d' Y')) ( eq-pair-Σ @@ -817,7 +817,7 @@ module _ ( two-distinct-elements-leq-2-Fin ( number-of-elements-count eX) ( ineq))) - ( is-injective-map-equiv (equiv-count eX) p) + ( is-injective-equiv (equiv-count eX) p) canonical-2-Element-Decidable-Subtype-count : 2-Element-Decidable-Subtype l X diff --git a/src/univalent-combinatorics/set-quotients-of-index-two.lagda.md b/src/univalent-combinatorics/set-quotients-of-index-two.lagda.md index ca51a81b33..afd05cac1d 100644 --- a/src/univalent-combinatorics/set-quotients-of-index-two.lagda.md +++ b/src/univalent-combinatorics/set-quotients-of-index-two.lagda.md @@ -59,7 +59,7 @@ module _ map-reflecting-map-equivalence-relation R f (h y) cases-coherence-square-maps-eq-one-value-emb-is-set-quotient H' y ( inl (inr _)) (inl (inr _)) k'' p q r = - ( is-injective-map-equiv eA (q ∙ inv p)) ∙ + ( is-injective-equiv eA (q ∙ inv p)) ∙ ( P ∙ reflects-map-reflecting-map-equivalence-relation R f ( pr1 H @@ -69,7 +69,7 @@ module _ ( H' ( map-reflecting-map-equivalence-relation R f x) ( map-reflecting-map-equivalence-relation R f y)) - ( is-injective-map-equiv eA (p ∙ inv q)))))) + ( is-injective-equiv eA (p ∙ inv q)))))) cases-coherence-square-maps-eq-one-value-emb-is-set-quotient H' y ( inl (inr _)) (inr _) (inl (inr _)) p q r = ex-falso @@ -81,14 +81,14 @@ module _ ( pr2 H (map-equiv ( is-effective-is-set-quotient R QR f Uf (h x) (h y)) - ( inv P ∙ is-injective-map-equiv eA (p ∙ inv r)))))) ∙ + ( inv P ∙ is-injective-equiv eA (p ∙ inv r)))))) ∙ ( q)))) cases-coherence-square-maps-eq-one-value-emb-is-set-quotient H' y ( inl (inr _)) (inr _) (inr _) p q r = - is-injective-map-equiv eA (q ∙ inv r) + is-injective-equiv eA (q ∙ inv r) cases-coherence-square-maps-eq-one-value-emb-is-set-quotient H' y ( inr _) (inl (inr _)) (inl (inr _)) p q r = - is-injective-map-equiv eA (q ∙ inv r) + is-injective-equiv eA (q ∙ inv r) cases-coherence-square-maps-eq-one-value-emb-is-set-quotient H' y ( inr _) (inl (inr _)) (inr _) p q r = ex-falso @@ -100,11 +100,11 @@ module _ ( pr2 H (map-equiv ( is-effective-is-set-quotient R QR f Uf (h x) (h y)) - ( inv P ∙ is-injective-map-equiv eA (p ∙ inv r)))))) ∙ + ( inv P ∙ is-injective-equiv eA (p ∙ inv r)))))) ∙ ( q)))) cases-coherence-square-maps-eq-one-value-emb-is-set-quotient H' y ( inr _) (inr _) k'' p q r = - ( is-injective-map-equiv eA (q ∙ inv p)) ∙ + ( is-injective-equiv eA (q ∙ inv p)) ∙ ( P ∙ reflects-map-reflecting-map-equivalence-relation R f ( pr1 H @@ -114,7 +114,7 @@ module _ ( H' ( map-reflecting-map-equivalence-relation R f x) ( map-reflecting-map-equivalence-relation R f y)) - ( is-injective-map-equiv eA (p ∙ inv q)))))) + ( is-injective-equiv eA (p ∙ inv q)))))) coherence-square-maps-eq-one-value-emb-is-set-quotient : is-emb h' → diff --git a/tables/pullbacks.md b/tables/pullbacks.md index f5951ec94c..147476168c 100644 --- a/tables/pullbacks.md +++ b/tables/pullbacks.md @@ -1,8 +1,8 @@ | Concept | File | | ----------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------- | -| Cospans | [`foundation.cospans`](foundation.cospans.md) | -| Morphisms of cospans | [`foundation.morphisms-cospans`](foundation.morphisms-cospans.md) | -| Cones over cospans | [`foundation.cones-over-cospans`](foundation.cones-over-cospans.md) | +| Cospan diagrams | [`foundation.cospans`](foundation.cospan-diagrams.md) | +| Morphisms of cospan diagrams | [`foundation.morphisms-cospans`](foundation.morphisms-cospan-diagrams.md) | +| Cones over cospan diagrams | [`foundation.cones-over-cospan-diagrams`](foundation.cones-over-cospan-diagrams.md) | | The universal property of pullbacks (foundation-core) | [`foundation-core.universal-property-pullbacks`](foundation-core.universal-property-pullbacks.md) | | The universal property of pullbacks (foundation) | [`foundation.universal-property-pullbacks`](foundation.universal-property-pullbacks.md) | | The universal property of fiber products | [`foundation.universal-property-fiber-products`](foundation.universal-property-fiber-products.md) |