From 4cb8ae9ea58fe1f6e3d32c839e297dd3de9d58ce Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Mon, 17 Jun 2024 14:31:01 +0200 Subject: [PATCH 1/4] start of work on a self-contained file proving a special case of yoneda --- mkdocs.yml | 1 + src/simplicial-hott/13-yoneda-geodesic.rzk.md | 312 ++++++++++++++++++ 2 files changed, 313 insertions(+) create mode 100644 src/simplicial-hott/13-yoneda-geodesic.rzk.md diff --git a/mkdocs.yml b/mkdocs.yml index e509920..7ed7314 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -34,6 +34,7 @@ nav: - The Yoneda Lemma: simplicial-hott/09-yoneda.rzk.md - ∞-categories (Rezk Types): simplicial-hott/10-rezk-types.rzk.md - Cocartesian Families: simplicial-hott/12-cocartesian.rzk.md + - A self contained proof of the Yoneda lemma: simplicial-hott/13-yoneda-geodesic.rzk.md markdown_extensions: - admonition diff --git a/src/simplicial-hott/13-yoneda-geodesic.rzk.md b/src/simplicial-hott/13-yoneda-geodesic.rzk.md new file mode 100644 index 0000000..146c07f --- /dev/null +++ b/src/simplicial-hott/13-yoneda-geodesic.rzk.md @@ -0,0 +1,312 @@ +# A self contained proof of the Yoneda lemma + +This file, which is independent of the rest of the repository, contains a self- +contained proof of the Yoneda lemma in the special case where both functors +are contravariantly representable. This is intended for expository purposes. + +Terms are annotated "*" when they are redefinitions (or specializations of +redefinitions) of results with the same name in the broader repository. + +This is a literate `rzk` file: + +```rzk +#lang rzk-1 +``` + +## Prerequisites + +Some of the definitions in this file rely on function extensionality: + +```rzk +#assume funext : FunExt +``` + +## Natural transformations involving a representable functor + +Fix a pre-∞-category $A$ and terms $a b : A$. The Yoneda lemma characterizes +natural transformations between the type families contravariantly represented +by these terms. + +Ordinarily, such a natural transformation would involve a family of maps + +`#!rzk ϕ : (z : A) → hom A z a → hom A z b` + +together with a proof of naturality of these components, but by +naturality-covariant-fiberwise-transformation naturality is automatic. + +```rzk +#def naturality-contravariant-fiberwise-representable-transformation* + ( A : U) + ( is-pre-∞-category-A : is-pre-∞-category A) + ( a b x y : A) + ( f : hom A y a) + ( g : hom A x y) + ( ϕ : (z : A) → hom A z a → hom A z b) + : ( contravariant-transport A x y g + ( \ z → hom A z b) + ( is-contravariant-representable-is-pre-∞-category A is-pre-∞-category-A b) + ( ϕ y f)) + = ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a g f)) + := + naturality-contravariant-fiberwise-transformation A x y g + ( \ z → hom A z a) (\ z → hom A z b) + ( is-contravariant-representable-is-pre-∞-category A is-pre-∞-category-A a) + ( is-contravariant-representable-is-pre-∞-category A is-pre-∞-category-A b) + ( ϕ) + ( f) +``` + +For any pre-∞-category $A$ terms $a b : A$, the contravariant Yoneda lemma +provides an equivalence between the type `#!rzk (z : A) → hom A z a → hom A z b` +of natural transformations and the type `#!rzk hom A a b`. + +One of the maps in this equivalence is evaluation at the identity. The inverse +map makes use of the contravariant transport operation. + +The following map, `#!rzk contra-evid` evaluates a natural transformation out of +a representable functor at the identity arrow. + +```rzk +#def contra-evid* + ( A : U) + ( a b : A) + : ( ( z : A) → hom A z a → hom A z b) → hom A a b + := \ ϕ → ϕ a (id-hom A a) +``` + +The inverse map only exists for pre-∞-categories. + +```rzk +#def contra-yon* + ( A : U) + ( is-pre-∞-category-A : is-pre-∞-category A) + ( a b : A) + : hom A a b → ((z : A) → hom A z a → hom A z b) + := + \ v z f → + contravariant-transport A z a f + ( \ z → hom A z b) + ( is-contravariant-representable-is-pre-∞-category A is-pre-∞-category-A b) + ( v) +``` + +It remains to show that the Yoneda maps are inverses. One retraction is +straightforward: + +```rzk +#def contra-evid-yon* + ( A : U) + ( is-pre-∞-category-A : is-pre-∞-category A) + ( a b : A) + ( v : hom A a b) + : contra-evid* A a b (contra-yon* A is-pre-∞-category-A a b v) = v + := + id-arr-contravariant-transport A a + ( \ z → hom A z b) + ( is-contravariant-representable-is-pre-∞-category A is-pre-∞-category-A b) + ( v) +``` + +The other composite carries $ϕ$ to an a priori distinct natural transformation. +We first show that these are pointwise equal at all `#!rzk x : A` and +`#!rzk f : hom A x a` in two steps. + +```rzk +#section contra-yon-evid + +#variable A : U +#variable is-pre-∞-category-A : is-pre-∞-category A +#variables a b : A +``` + +The composite `#!rzk contra-yon-evid` of `#!rzk ϕ` equals `#!rzk ϕ` at all +`#!rzk x : A` and `#!rzk f : hom A x a`. + +```rzk +#def contra-yon-evid-twice-pointwise* + ( ϕ : (z : A) → hom A z a → hom A z b) + ( x : A) + ( f : hom A x a) + : ( ( contra-yon* A is-pre-∞-category-A a b) + ( ( contra-evid* A a b) ϕ)) x f = ϕ x f + := + concat + ( hom A x b) + ( ( ( contra-yon* A is-pre-∞-category-A a b) + ( ( contra-evid* A a b) ϕ)) x f) + ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x a a f (id-hom A a))) + ( ϕ x f) + ( naturality-contravariant-fiberwise-representable-transformation* + A is-pre-∞-category-A a b x a (id-hom A a) f ϕ) + ( ap + ( hom A x a) + ( hom A x b) + ( comp-is-pre-∞-category A is-pre-∞-category-A x a a f (id-hom A a)) + ( f) + ( ϕ x) + ( comp-id-is-pre-∞-category A is-pre-∞-category-A x a f)) +``` + +By `#!rzk funext`, these are equals as functions of `#!rzk f` pointwise in +`#!rzk x`. + +```rzk +#def contra-yon-evid-once-pointwise* uses (funext) + ( ϕ : (z : A) → hom A z a → hom A z b) + ( x : A) + : ( ( contra-yon* A is-pre-∞-category-A a b) + ( ( contra-evid* A a b) ϕ)) x = ϕ x + := + eq-htpy funext + ( hom A x a) + ( \ f → hom A x b) + ( \ f → + ( ( contra-yon* A is-pre-∞-category-A a b) + ( ( contra-evid* A a b) ϕ)) x f) + ( \ f → (ϕ x f)) + ( \ f → contra-yon-evid-twice-pointwise* ϕ x f) +``` + +By `#!rzk funext` again, these are equal as functions of `#!rzk x` and +`#!rzk f`. + +```rzk +#def contra-yon-evid* uses (funext) + ( ϕ : (z : A) → hom A z a → hom A z b) + : contra-yon* A is-pre-∞-category-A a b (contra-evid* A a b ϕ) = ϕ + := + eq-htpy funext + ( A) + ( \ x → (hom A x a → hom A x b)) + ( contra-yon* A is-pre-∞-category-A a b (contra-evid* A a b ϕ)) + ( ϕ) + ( contra-yon-evid-once-pointwise* ϕ) + +#end contra-yon-evid +``` + +The contravariant Yoneda lemma says that evaluation at the identity defines an +equivalence. + +```rzk +#def contra-yoneda-lemma* uses (funext) + ( A : U) + ( is-pre-∞-category-A : is-pre-∞-category A) + ( a b : A) + : is-equiv ((z : A) → hom A z a → hom A z b) (hom A a b) (contra-evid* A a b) + := + ( ( ( contra-yon* A is-pre-∞-category-A a b) + , ( contra-yon-evid* A is-pre-∞-category-A a b)) + , ( ( contra-yon* A is-pre-∞-category-A a b) + , ( contra-evid-yon* A is-pre-∞-category-A a b))) +``` + +## Contravariant Naturality + +The equivalence of the Yoneda lemma is natural in both $a : A$ and $b : A$. + +Naturality in $a$ follows from the fact that the maps `#!rzk evid` and +`#!rzk yon` are fiberwise equivalences between contravariant families over $A$, +though it requires some work, which has not yet been formalized, to prove that +the domain is contravariant. + +Naturality in $b$ is not automatic but can be proven easily: + +```rzk title="RS17, Lemma 9.2(i), dual" +#def is-natural-in-family-contra-evid* + ( A : U) + ( a b b' : A) + ( ψ : (z : A) → hom A z b → hom A z b') + ( φ : (z : A) → hom A z a → hom A z b) + : ( comp ((z : A) → hom A z a → hom A z b) (hom A a b) (hom A a b') + ( ψ a) (contra-evid* A a b)) φ + = ( comp ((z : A) → hom A z a → hom A z b) ((z : A) → hom A z a → hom A z b') + ( hom A a b') + ( contra-evid* A a b') (\ α z g → ψ z (α z g))) φ + := refl +``` + +```rzk title="RS17, Lemma 9.2(ii), dual" +#def is-natural-in-family-contra-yon-twice-pointwise* + ( A : U) + ( is-pre-∞-category-A : is-pre-∞-category A) + ( a b b' : A) + ( ψ : (z : A) → hom A z b → hom A z b') + ( u : hom A a b) + ( x : A) + ( f : hom A x a) + : ( comp (hom A a b) (hom A a b') ((z : A) → hom A z a → hom A z b') + ( contra-yon* A is-pre-∞-category-A a b') (ψ a)) u x f + = ( comp (hom A a b) + ( ( z : A) → hom A z a → hom A z b) + ( ( z : A) → hom A z a → hom A z b') + ( \ α z g → ψ z (α z g)) + ( contra-yon* A is-pre-∞-category-A a b)) u x f + := + naturality-contravariant-fiberwise-transformation + A x a f (\ z → hom A z b) (\ z → hom A z b') + ( is-contravariant-representable-is-pre-∞-category A is-pre-∞-category-A b) + ( is-contravariant-representable-is-pre-∞-category A is-pre-∞-category-A b') + ψ u + +#def is-natural-in-family-contra-yon-once-pointwise* uses (funext) + ( A : U) + ( is-pre-∞-category-A : is-pre-∞-category A) + ( a b b' : A) + ( ψ : (z : A) → hom A z b → hom A z b') + ( u : hom A a b) + ( x : A) + : ( comp (hom A a b) (hom A a b') ((z : A) → hom A z a → hom A z b') + ( contra-yon* A is-pre-∞-category-A a b') (ψ a)) u x + = ( comp (hom A a b) + ( ( z : A) → hom A z a → hom A z b) + ( ( z : A) → hom A z a → hom A z b') + ( \ α z g → ψ z (α z g)) + ( contra-yon* A is-pre-∞-category-A a b)) u x + := + eq-htpy funext + ( hom A x a) + ( \ f → hom A x b') + ( \ f → + ( comp (hom A a b) (hom A a b') ((z : A) → hom A z a → hom A z b') + ( contra-yon* A is-pre-∞-category-A a b') (ψ a)) u x f) + ( \ f → + ( comp (hom A a b) + ( ( z : A) → hom A z a → hom A z b) + ( ( z : A) → hom A z a → hom A z b') + ( \ α z g → ψ z (α z g)) + ( contra-yon* A is-pre-∞-category-A a b)) u x f) + ( \ f → + is-natural-in-family-contra-yon-twice-pointwise* + A is-pre-∞-category-A a b b' ψ u x f) + +#def is-natural-in-family-contra-yon* uses (funext) + ( A : U) + ( is-pre-∞-category-A : is-pre-∞-category A) + ( a b b' : A) + ( ψ : (z : A) → hom A z b → hom A z b') + ( u : hom A a b) + : ( comp (hom A a b) (hom A a b') ((z : A) → hom A z a → hom A z b') + ( contra-yon* A is-pre-∞-category-A a b') (ψ a)) u + = ( comp (hom A a b) + ( ( z : A) → hom A z a → hom A z b) + ( ( z : A) → hom A z a → hom A z b') + ( \ α z g → ψ z (α z g)) + ( contra-yon* A is-pre-∞-category-A a b)) u + := + eq-htpy funext + ( A) + ( \ x → hom A x a → hom A x b') + ( \ x → + ( comp (hom A a b) (hom A a b') ((z : A) → hom A z a → hom A z b') + ( contra-yon* A is-pre-∞-category-A a b') (ψ a)) u x) + ( \ x → + ( comp (hom A a b) + ( ( z : A) → hom A z a → hom A z b) + ( ( z : A) → hom A z a → hom A z b') + ( \ α z g → ψ z (α z g)) + ( contra-yon* A is-pre-∞-category-A a b)) u x) + ( \ x → + is-natural-in-family-contra-yon-once-pointwise* + A is-pre-∞-category-A a b b' ψ u x) +``` From fe275a6d2cfde89f2e8c2bc86123ef5d740315aa Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Mon, 17 Jun 2024 14:46:12 +0200 Subject: [PATCH 2/4] factored out proof that contravariant reps are contravariant --- src/simplicial-hott/13-yoneda-geodesic.rzk.md | 181 ++++++++++++++++-- 1 file changed, 164 insertions(+), 17 deletions(-) diff --git a/src/simplicial-hott/13-yoneda-geodesic.rzk.md b/src/simplicial-hott/13-yoneda-geodesic.rzk.md index 146c07f..e71d689 100644 --- a/src/simplicial-hott/13-yoneda-geodesic.rzk.md +++ b/src/simplicial-hott/13-yoneda-geodesic.rzk.md @@ -54,6 +54,163 @@ naturality-covariant-fiberwise-transformation naturality is automatic. ( is-contravariant-representable-is-pre-∞-category A is-pre-∞-category-A b) ( ϕ) ( f) + +-- Same as the above but without the contravariant transport. +-- This unfolds a composition triangle to a square with an identity component +#def id-codomain-square + ( A : U) + ( is-pre-∞-category-A : is-pre-∞-category A) + ( x y a : A) + ( f : hom A x y) + ( v : hom A y a) + : ( t : Δ¹) → hom A (f t) a + := \ t s → + recOR + ( s ≤ t ↦ + ( witness-comp-is-pre-∞-category A is-pre-∞-category-A x y a f v) + ( t , s) + , t ≤ s ↦ + ( comp-id-witness A x a + ( comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) (s , t)) + +-- We apply the transformation phi to the square just constructed. +#def transformation-id-codomain-square + ( A : U) + ( is-pre-∞-category-A : is-pre-∞-category A) + ( a b x y : A) + ( f : hom A x y) + ( v : hom A y a) + ( ϕ : (z : A) → hom A z a → hom A z b) + : ( t : Δ¹) → hom A (f t) b + := \ t → ϕ (f t) (\ s → id-codomain-square A is-pre-∞-category-A x y a f v t s) + +-- This extracts the diagonal composite of the square. +#def diagonal-transformation-id-codomain-square + ( A : U) + ( is-pre-∞-category-A : is-pre-∞-category A) + ( a b x y : A) + ( f : hom A x y) + ( v : hom A y a) + ( ϕ : (z : A) → hom A z a → hom A z b) + : hom A x b + := + \ t → + transformation-id-codomain-square A is-pre-∞-category-A a b x y f v ϕ t t + +-- One half of transformation-id-codomain-square. +#def witness-comp-transformation-id-codomain-square + ( A : U) + ( is-pre-∞-category-A : is-pre-∞-category A) + ( a b x y : A) + ( f : hom A x y) + ( v : hom A y a) + ( ϕ : (z : A) → hom A z a → hom A z b) + : hom2 A x y b f (ϕ y v) + ( diagonal-transformation-id-codomain-square + A is-pre-∞-category-A a b x y f v ϕ) + := + \ (t , s) → + transformation-id-codomain-square A is-pre-∞-category-A a b x y f v ϕ t s + +-- The associated coherence. +#def coherence-witness-comp-transformation-id-codomain-square + ( A : U) + ( is-pre-∞-category-A : is-pre-∞-category A) + ( a b x y : A) + ( f : hom A x y) + ( v : hom A y a) + ( ϕ : (z : A) → hom A z a → hom A z b) + : ( comp-is-pre-∞-category A is-pre-∞-category-A x y b f (ϕ y v)) + = ( diagonal-transformation-id-codomain-square + A is-pre-∞-category-A a b x y f v ϕ) + := + uniqueness-comp-is-pre-∞-category A is-pre-∞-category-A x y b f (ϕ y v) + ( diagonal-transformation-id-codomain-square + A is-pre-∞-category-A a b x y f v ϕ) + ( witness-comp-transformation-id-codomain-square + A is-pre-∞-category-A a b x y f v ϕ) + +-- The other half of transformation-id-codomain-square. +#def witness-id-transformation-id-codomain-square + ( A : U) + ( is-pre-∞-category-A : is-pre-∞-category A) + ( a b x y : A) + ( f : hom A x y) + ( v : hom A y a) + ( ϕ : (z : A) → hom A z a → hom A z b) + : hom2 A x b b + ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) + ( id-hom A b) + ( diagonal-transformation-id-codomain-square + A is-pre-∞-category-A a b x y f v ϕ) + := + \ (t , s) → + transformation-id-codomain-square A is-pre-∞-category-A a b x y f v ϕ s t + +-- The associated coherence. +#def coherence-witness-id-transformation-id-codomain-square + ( A : U) + ( is-pre-∞-category-A : is-pre-∞-category A) + ( a b x y : A) + ( f : hom A x y) + ( v : hom A y a) + ( ϕ : (z : A) → hom A z a → hom A z b) + : ( comp-is-pre-∞-category A is-pre-∞-category-A x b b + ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) + ( id-hom A b)) + = ( diagonal-transformation-id-codomain-square + A is-pre-∞-category-A a b x y f v ϕ) + := + uniqueness-comp-is-pre-∞-category A is-pre-∞-category-A x b b + ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) + ( id-hom A b) + ( diagonal-transformation-id-codomain-square + A is-pre-∞-category-A a b x y f v ϕ) + ( witness-id-transformation-id-codomain-square + A is-pre-∞-category-A a b x y f v ϕ) + +#def simplified-coherence-witness-id-transformation-id-codomain-square + ( A : U) + ( is-pre-∞-category-A : is-pre-∞-category A) + ( a b x y : A) + ( f : hom A x y) + ( v : hom A y a) + ( ϕ : (z : A) → hom A z a → hom A z b) + : ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) + = ( diagonal-transformation-id-codomain-square + A is-pre-∞-category-A a b x y f v ϕ) + := + zag-zig-concat (hom A x b) + ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) + ( comp-is-pre-∞-category A is-pre-∞-category-A x b b + ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) + ( id-hom A b)) + ( diagonal-transformation-id-codomain-square + A is-pre-∞-category-A a b x y f v ϕ) + ( comp-id-is-pre-∞-category A is-pre-∞-category-A x b + ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v))) + ( coherence-witness-id-transformation-id-codomain-square + A is-pre-∞-category-A a b x y f v ϕ) + +#def naturality-contravariant-fiberwise-representable-transformation** + ( A : U) + ( is-pre-∞-category-A : is-pre-∞-category A) + ( a b x y : A) + ( f : hom A x y) + ( v : hom A y a) + ( ϕ : (z : A) → hom A z a → hom A z b) + : ( comp-is-pre-∞-category A is-pre-∞-category-A x y b f (ϕ y v)) + = ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) + := + zig-zag-concat (hom A x b) + ( comp-is-pre-∞-category A is-pre-∞-category-A x y b f (ϕ y v)) + ( diagonal-transformation-id-codomain-square + A is-pre-∞-category-A a b x y f v ϕ) + ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) + ( coherence-witness-comp-transformation-id-codomain-square + A is-pre-∞-category-A a b x y f v ϕ) + ( simplified-coherence-witness-id-transformation-id-codomain-square + A is-pre-∞-category-A a b x y f v ϕ) ``` For any pre-∞-category $A$ terms $a b : A$, the contravariant Yoneda lemma @@ -82,12 +239,7 @@ The inverse map only exists for pre-∞-categories. ( is-pre-∞-category-A : is-pre-∞-category A) ( a b : A) : hom A a b → ((z : A) → hom A z a → hom A z b) - := - \ v z f → - contravariant-transport A z a f - ( \ z → hom A z b) - ( is-contravariant-representable-is-pre-∞-category A is-pre-∞-category-A b) - ( v) + := \ v z f → comp-is-pre-∞-category A is-pre-∞-category-A z a b f v ``` It remains to show that the Yoneda maps are inverses. One retraction is @@ -101,10 +253,7 @@ straightforward: ( v : hom A a b) : contra-evid* A a b (contra-yon* A is-pre-∞-category-A a b v) = v := - id-arr-contravariant-transport A a - ( \ z → hom A z b) - ( is-contravariant-representable-is-pre-∞-category A is-pre-∞-category-A b) - ( v) + id-comp-is-pre-∞-category A is-pre-∞-category-A a b v ``` The other composite carries $ϕ$ to an a priori distinct natural transformation. @@ -136,8 +285,8 @@ The composite `#!rzk contra-yon-evid` of `#!rzk ϕ` equals `#!rzk ϕ` at all ( ( contra-evid* A a b) ϕ)) x f) ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x a a f (id-hom A a))) ( ϕ x f) - ( naturality-contravariant-fiberwise-representable-transformation* - A is-pre-∞-category-A a b x a (id-hom A a) f ϕ) + ( naturality-contravariant-fiberwise-representable-transformation** + A is-pre-∞-category-A a b x a f (id-hom A a) ϕ) ( ap ( hom A x a) ( hom A x b) @@ -243,11 +392,9 @@ Naturality in $b$ is not automatic but can be proven easily: ( \ α z g → ψ z (α z g)) ( contra-yon* A is-pre-∞-category-A a b)) u x f := - naturality-contravariant-fiberwise-transformation - A x a f (\ z → hom A z b) (\ z → hom A z b') - ( is-contravariant-representable-is-pre-∞-category A is-pre-∞-category-A b) - ( is-contravariant-representable-is-pre-∞-category A is-pre-∞-category-A b') - ψ u + naturality-contravariant-fiberwise-representable-transformation** + A is-pre-∞-category-A b b' x a f u ψ + #def is-natural-in-family-contra-yon-once-pointwise* uses (funext) ( A : U) From 97df4a6a00866aafcd315ef7e03f38b427fc1f56 Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Mon, 17 Jun 2024 17:57:05 +0200 Subject: [PATCH 3/4] finished proof of naturality --- src/simplicial-hott/13-yoneda-geodesic.rzk.md | 808 +++++++++++++----- 1 file changed, 579 insertions(+), 229 deletions(-) diff --git a/src/simplicial-hott/13-yoneda-geodesic.rzk.md b/src/simplicial-hott/13-yoneda-geodesic.rzk.md index e71d689..ebfe281 100644 --- a/src/simplicial-hott/13-yoneda-geodesic.rzk.md +++ b/src/simplicial-hott/13-yoneda-geodesic.rzk.md @@ -15,116 +15,343 @@ This is a literate `rzk` file: ## Prerequisites -Some of the definitions in this file rely on function extensionality: +Some of the definitions in this file rely on function extensionality and +extension extensionality: ```rzk #assume funext : FunExt +#assume extext : ExtExt ``` -## Natural transformations involving a representable functor +## Hom types -Fix a pre-∞-category $A$ and terms $a b : A$. The Yoneda lemma characterizes -natural transformations between the type families contravariantly represented -by these terms. +Extension types are used to define the type of arrows between fixed terms: -Ordinarily, such a natural transformation would involve a family of maps + + + x + y + + +```rzk title="RS17, Definition 5.1" +#def Hom + ( A : U) + ( x y : A) + : U + := + ( t : Δ¹) + → A [ t ≡ 0₂ ↦ x , -- the left endpoint is exactly x + t ≡ 1₂ ↦ y] -- the right endpoint is exactly y -`#!rzk ϕ : (z : A) → hom A z a → hom A z b` +``` -together with a proof of naturality of these components, but by -naturality-covariant-fiberwise-transformation naturality is automatic. +Extension types are also used to define the type of commutative triangles: + + + + + + + x + y + z + f + g + h + + +```rzk title="RS17, Definition 5.2" +#def Hom2 + ( A : U) + ( x y z : A) + ( f : Hom A x y) + ( g : Hom A y z) + ( h : Hom A x z) + : U + := + ( ( t₁ , t₂) : Δ²) + → A [ t₂ ≡ 0₂ ↦ f t₁ , -- the top edge is exactly `f`, + t₁ ≡ 1₂ ↦ g t₂ , -- the right edge is exactly `g`, and + t₂ ≡ t₁ ↦ h t₂] -- the diagonal is exactly `h` +``` + +## The Segal condition + +A type is **a pre-∞-category** if every composable pair of arrows has a unique composite. +Note this is a considerable simplification of the usual Segal condition, which +also requires homotopical uniqueness of higher-order composites. + +```rzk title="RS17, Definition 5.3" +#def Is-pre-∞-category + ( A : U) + : U + := + ( x : A) → (y : A) → (z : A) + → ( f : Hom A x y) → (g : Hom A y z) + → is-contr (Σ (h : Hom A x z) , (Hom2 A x y z f g h)) +``` + +Pre-∞-categories have a composition functor and witnesses to the composition +relation. Composition is written in diagrammatic order to match the order of +arguments in `#!rzk is-pre-∞-category`. ```rzk -#def naturality-contravariant-fiberwise-representable-transformation* +#def Comp-is-pre-∞-category ( A : U) - ( is-pre-∞-category-A : is-pre-∞-category A) - ( a b x y : A) - ( f : hom A y a) - ( g : hom A x y) - ( ϕ : (z : A) → hom A z a → hom A z b) - : ( contravariant-transport A x y g - ( \ z → hom A z b) - ( is-contravariant-representable-is-pre-∞-category A is-pre-∞-category-A b) - ( ϕ y f)) - = ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a g f)) + ( is-pre-∞-category-A : Is-pre-∞-category A) + ( x y z : A) + ( f : Hom A x y) + ( g : Hom A y z) + : Hom A x z + := first (first (is-pre-∞-category-A x y z f g)) + +#def Witness-comp-is-pre-∞-category + ( A : U) + ( is-pre-∞-category-A : Is-pre-∞-category A) + ( x y z : A) + ( f : Hom A x y) + ( g : Hom A y z) + : Hom2 A x y z f g (Comp-is-pre-∞-category A is-pre-∞-category-A x y z f g) + := second (first (is-pre-∞-category-A x y z f g)) +``` + +Composition in a pre-∞-category is unique in the following sense. If there is a +witness that an arrow $h$ is a composite of $f$ and $g$, then the specified +composite equals $h$. + + + + + + + x + y + z + f + g + h + α + = + + + + + x + y + z + f + g + comp-is-pre-∞-category + Witness-comp-is-pre-∞-category + + +```rzk +#def Uniqueness-comp-is-pre-∞-category + ( A : U) + ( is-pre-∞-category-A : Is-pre-∞-category A) + ( x y z : A) + ( f : Hom A x y) + ( g : Hom A y z) + ( h : Hom A x z) + ( alpha : Hom2 A x y z f g h) + : ( Comp-is-pre-∞-category A is-pre-∞-category-A x y z f g) = h := - naturality-contravariant-fiberwise-transformation A x y g - ( \ z → hom A z a) (\ z → hom A z b) - ( is-contravariant-representable-is-pre-∞-category A is-pre-∞-category-A a) - ( is-contravariant-representable-is-pre-∞-category A is-pre-∞-category-A b) - ( ϕ) + first-path-Σ + ( Hom A x z) + ( Hom2 A x y z f g) + ( Comp-is-pre-∞-category A is-pre-∞-category-A x y z f g + , Witness-comp-is-pre-∞-category A is-pre-∞-category-A x y z f g) + ( h , alpha) + ( homotopy-contraction + ( Σ ( k : Hom A x z) , (Hom2 A x y z f g k)) + ( is-pre-∞-category-A x y z f g) + ( h , alpha)) +``` + +## Identity + +All types have identity arrows and witnesses to the identity composition law. + + + + x + x + x + + +```rzk title="RS17, Definition 5.7" +#def Id-hom + ( A : U) + ( x : A) + : Hom A x x + := \ t → x +``` + +Witness for the right identity law: + + + + + + + x + y + y + f + y + f + f + + +```rzk title="RS17, Proposition 5.8a" +#def Comp-id-witness + ( A : U) + ( x y : A) + ( f : Hom A x y) + : Hom2 A x y y f (Id-hom A y) f + := \ (t , s) → f t +``` + +Witness for the left identity law: + + + + + + + x + x + y + x + f + f + f + + +```rzk title="RS17, Proposition 5.8b" +#def Id-comp-witness + ( A : U) + ( x y : A) + ( f : Hom A x y) + : Hom2 A x x y (Id-hom A x) f f + := \ (t , s) → f s +``` + +In a pre-∞-category, where composition is unique, it follows that composition with an identity arrow recovers the original arrow. Thus, an identity axiom was not needed in the definition of pre-∞-categorys. + +```rzk title="If A is a pre-∞-category then the right unit law holds" +#def Comp-id-is-pre-∞-category + ( A : U) + ( is-pre-∞-category-A : Is-pre-∞-category A) + ( x y : A) + ( f : Hom A x y) + : ( Comp-is-pre-∞-category A is-pre-∞-category-A x y y f (Id-hom A y)) + = f + := + Uniqueness-comp-is-pre-∞-category + ( A) + ( is-pre-∞-category-A) + ( x) (y) (y) ( f) + ( Id-hom A y) + ( f) + ( Comp-id-witness A x y f) +``` --- Same as the above but without the contravariant transport. --- This unfolds a composition triangle to a square with an identity component -#def id-codomain-square +```rzk title="If A is a pre-∞-category then the left unit law holds" +#def Id-comp-is-pre-∞-category ( A : U) - ( is-pre-∞-category-A : is-pre-∞-category A) - ( x y a : A) - ( f : hom A x y) - ( v : hom A y a) - : ( t : Δ¹) → hom A (f t) a - := \ t s → - recOR - ( s ≤ t ↦ - ( witness-comp-is-pre-∞-category A is-pre-∞-category-A x y a f v) - ( t , s) - , t ≤ s ↦ - ( comp-id-witness A x a - ( comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) (s , t)) - --- We apply the transformation phi to the square just constructed. -#def transformation-id-codomain-square + ( is-pre-∞-category-A : Is-pre-∞-category A) + ( x y : A) + ( f : Hom A x y) + : ( Comp-is-pre-∞-category A is-pre-∞-category-A x x y (Id-hom A x) f) + = f + := + Uniqueness-comp-is-pre-∞-category + ( A) + ( is-pre-∞-category-A) + ( x) (x) (y) + ( Id-hom A x) + ( f) + ( f) + ( Id-comp-witness A x y f) +``` + +## Natural transformations between representable functors + +Fix a pre-∞-category $A$ and terms $a b : A$. The Yoneda lemma characterizes natural transformations between the type families contravariantly represented by these terms. + +Ordinarily, such a natural transformation would involve a family of maps + +`#!rzk ϕ : (z : A) → Hom A z a → Hom A z b` + +together with a proof of naturality of these components, but by +naturality-covariant-fiberwise-transformation* naturality is automatic. + +```rzk +-- We apply a fiberwise transformation ϕ to a square of a particular form. +#def square-representable-transformation ( A : U) - ( is-pre-∞-category-A : is-pre-∞-category A) + ( is-pre-∞-category-A : Is-pre-∞-category A) ( a b x y : A) - ( f : hom A x y) - ( v : hom A y a) - ( ϕ : (z : A) → hom A z a → hom A z b) - : ( t : Δ¹) → hom A (f t) b - := \ t → ϕ (f t) (\ s → id-codomain-square A is-pre-∞-category-A x y a f v t s) + ( f : Hom A x y) + ( v : Hom A y a) + ( ϕ : (z : A) → Hom A z a → Hom A z b) + : ( t : Δ¹) → Hom A (f t) b + := + \ t → + ϕ + ( f t) + ( \ s → + recOR + ( s ≤ t ↦ + ( Witness-comp-is-pre-∞-category A is-pre-∞-category-A x y a f v) + ( t , s) + , t ≤ s ↦ + ( Comp-id-witness A x a + ( Comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) (s , t))) -- This extracts the diagonal composite of the square. #def diagonal-transformation-id-codomain-square ( A : U) - ( is-pre-∞-category-A : is-pre-∞-category A) + ( is-pre-∞-category-A : Is-pre-∞-category A) ( a b x y : A) - ( f : hom A x y) - ( v : hom A y a) - ( ϕ : (z : A) → hom A z a → hom A z b) - : hom A x b + ( f : Hom A x y) + ( v : Hom A y a) + ( ϕ : (z : A) → Hom A z a → Hom A z b) + : Hom A x b := \ t → - transformation-id-codomain-square A is-pre-∞-category-A a b x y f v ϕ t t + square-representable-transformation A is-pre-∞-category-A a b x y f v ϕ t t -- One half of transformation-id-codomain-square. #def witness-comp-transformation-id-codomain-square ( A : U) - ( is-pre-∞-category-A : is-pre-∞-category A) + ( is-pre-∞-category-A : Is-pre-∞-category A) ( a b x y : A) - ( f : hom A x y) - ( v : hom A y a) - ( ϕ : (z : A) → hom A z a → hom A z b) - : hom2 A x y b f (ϕ y v) + ( f : Hom A x y) + ( v : Hom A y a) + ( ϕ : (z : A) → Hom A z a → Hom A z b) + : Hom2 A x y b f (ϕ y v) ( diagonal-transformation-id-codomain-square A is-pre-∞-category-A a b x y f v ϕ) := \ (t , s) → - transformation-id-codomain-square A is-pre-∞-category-A a b x y f v ϕ t s + square-representable-transformation A is-pre-∞-category-A a b x y f v ϕ t s -- The associated coherence. #def coherence-witness-comp-transformation-id-codomain-square ( A : U) - ( is-pre-∞-category-A : is-pre-∞-category A) + ( is-pre-∞-category-A : Is-pre-∞-category A) ( a b x y : A) - ( f : hom A x y) - ( v : hom A y a) - ( ϕ : (z : A) → hom A z a → hom A z b) - : ( comp-is-pre-∞-category A is-pre-∞-category-A x y b f (ϕ y v)) + ( f : Hom A x y) + ( v : Hom A y a) + ( ϕ : (z : A) → Hom A z a → Hom A z b) + : ( Comp-is-pre-∞-category A is-pre-∞-category-A x y b f (ϕ y v)) = ( diagonal-transformation-id-codomain-square A is-pre-∞-category-A a b x y f v ϕ) := - uniqueness-comp-is-pre-∞-category A is-pre-∞-category-A x y b f (ϕ y v) + Uniqueness-comp-is-pre-∞-category A is-pre-∞-category-A x y b f (ϕ y v) ( diagonal-transformation-id-codomain-square A is-pre-∞-category-A a b x y f v ϕ) ( witness-comp-transformation-id-codomain-square @@ -133,37 +360,37 @@ naturality-covariant-fiberwise-transformation naturality is automatic. -- The other half of transformation-id-codomain-square. #def witness-id-transformation-id-codomain-square ( A : U) - ( is-pre-∞-category-A : is-pre-∞-category A) + ( is-pre-∞-category-A : Is-pre-∞-category A) ( a b x y : A) - ( f : hom A x y) - ( v : hom A y a) - ( ϕ : (z : A) → hom A z a → hom A z b) - : hom2 A x b b + ( f : Hom A x y) + ( v : Hom A y a) + ( ϕ : (z : A) → Hom A z a → Hom A z b) + : Hom2 A x b b ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) - ( id-hom A b) + ( Id-hom A b) ( diagonal-transformation-id-codomain-square A is-pre-∞-category-A a b x y f v ϕ) := \ (t , s) → - transformation-id-codomain-square A is-pre-∞-category-A a b x y f v ϕ s t + square-representable-transformation A is-pre-∞-category-A a b x y f v ϕ s t -- The associated coherence. #def coherence-witness-id-transformation-id-codomain-square ( A : U) - ( is-pre-∞-category-A : is-pre-∞-category A) + ( is-pre-∞-category-A : Is-pre-∞-category A) ( a b x y : A) - ( f : hom A x y) - ( v : hom A y a) - ( ϕ : (z : A) → hom A z a → hom A z b) - : ( comp-is-pre-∞-category A is-pre-∞-category-A x b b + ( f : Hom A x y) + ( v : Hom A y a) + ( ϕ : (z : A) → Hom A z a → Hom A z b) + : ( Comp-is-pre-∞-category A is-pre-∞-category-A x b b ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) - ( id-hom A b)) + ( Id-hom A b)) = ( diagonal-transformation-id-codomain-square A is-pre-∞-category-A a b x y f v ϕ) := - uniqueness-comp-is-pre-∞-category A is-pre-∞-category-A x b b - ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) - ( id-hom A b) + Uniqueness-comp-is-pre-∞-category A is-pre-∞-category-A x b b + ( ϕ x (Comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) + ( Id-hom A b) ( diagonal-transformation-id-codomain-square A is-pre-∞-category-A a b x y f v ϕ) ( witness-id-transformation-id-codomain-square @@ -171,42 +398,42 @@ naturality-covariant-fiberwise-transformation naturality is automatic. #def simplified-coherence-witness-id-transformation-id-codomain-square ( A : U) - ( is-pre-∞-category-A : is-pre-∞-category A) + ( is-pre-∞-category-A : Is-pre-∞-category A) ( a b x y : A) - ( f : hom A x y) - ( v : hom A y a) - ( ϕ : (z : A) → hom A z a → hom A z b) - : ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) + ( f : Hom A x y) + ( v : Hom A y a) + ( ϕ : (z : A) → Hom A z a → Hom A z b) + : ( ϕ x (Comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) = ( diagonal-transformation-id-codomain-square A is-pre-∞-category-A a b x y f v ϕ) := - zag-zig-concat (hom A x b) - ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) - ( comp-is-pre-∞-category A is-pre-∞-category-A x b b - ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) - ( id-hom A b)) + zag-zig-concat (Hom A x b) + ( ϕ x (Comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) + ( Comp-is-pre-∞-category A is-pre-∞-category-A x b b + ( ϕ x (Comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) + ( Id-hom A b)) ( diagonal-transformation-id-codomain-square A is-pre-∞-category-A a b x y f v ϕ) - ( comp-id-is-pre-∞-category A is-pre-∞-category-A x b + ( Comp-id-is-pre-∞-category A is-pre-∞-category-A x b ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v))) ( coherence-witness-id-transformation-id-codomain-square A is-pre-∞-category-A a b x y f v ϕ) -#def naturality-contravariant-fiberwise-representable-transformation** +#def Naturality-contravariant-fiberwise-representable-transformation ( A : U) - ( is-pre-∞-category-A : is-pre-∞-category A) + ( is-pre-∞-category-A : Is-pre-∞-category A) ( a b x y : A) - ( f : hom A x y) - ( v : hom A y a) - ( ϕ : (z : A) → hom A z a → hom A z b) - : ( comp-is-pre-∞-category A is-pre-∞-category-A x y b f (ϕ y v)) - = ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) + ( f : Hom A x y) + ( v : Hom A y a) + ( ϕ : (z : A) → Hom A z a → Hom A z b) + : ( Comp-is-pre-∞-category A is-pre-∞-category-A x y b f (ϕ y v)) + = ( ϕ x (Comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) := - zig-zag-concat (hom A x b) - ( comp-is-pre-∞-category A is-pre-∞-category-A x y b f (ϕ y v)) + zig-zag-concat (Hom A x b) + ( Comp-is-pre-∞-category A is-pre-∞-category-A x y b f (ϕ y v)) ( diagonal-transformation-id-codomain-square A is-pre-∞-category-A a b x y f v ϕ) - ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) + ( ϕ x (Comp-is-pre-∞-category A is-pre-∞-category-A x y a f v)) ( coherence-witness-comp-transformation-id-codomain-square A is-pre-∞-category-A a b x y f v ϕ) ( simplified-coherence-witness-id-transformation-id-codomain-square @@ -214,122 +441,123 @@ naturality-covariant-fiberwise-transformation naturality is automatic. ``` For any pre-∞-category $A$ terms $a b : A$, the contravariant Yoneda lemma -provides an equivalence between the type `#!rzk (z : A) → hom A z a → hom A z b` -of natural transformations and the type `#!rzk hom A a b`. +provides an equivalence between the type +`#!rzk (z : A) → Hom A z a → Hom A z b` of natural transformations and the type `#!rzk Hom A a b`. -One of the maps in this equivalence is evaluation at the identity. The inverse -map makes use of the contravariant transport operation. +One of the maps in this equivalence is evaluation at the identity. The +inverse map makes use of the contravariant transport operation. -The following map, `#!rzk contra-evid` evaluates a natural transformation out of -a representable functor at the identity arrow. +The following map, `#!rzk contra-evid` evaluates a natural transformation +out of a representable functor at the identity arrow. ```rzk -#def contra-evid* +#def Contra-evid ( A : U) ( a b : A) - : ( ( z : A) → hom A z a → hom A z b) → hom A a b - := \ ϕ → ϕ a (id-hom A a) + : ( ( z : A) → Hom A z a → Hom A z b) → Hom A a b + := \ ϕ → ϕ a (Id-hom A a) ``` The inverse map only exists for pre-∞-categories. ```rzk -#def contra-yon* +#def Contra-yon ( A : U) - ( is-pre-∞-category-A : is-pre-∞-category A) + ( is-pre-∞-category-A : Is-pre-∞-category A) ( a b : A) - : hom A a b → ((z : A) → hom A z a → hom A z b) - := \ v z f → comp-is-pre-∞-category A is-pre-∞-category-A z a b f v + : Hom A a b → ((z : A) → Hom A z a → Hom A z b) + := \ v z f → Comp-is-pre-∞-category A is-pre-∞-category-A z a b f v ``` It remains to show that the Yoneda maps are inverses. One retraction is straightforward: ```rzk -#def contra-evid-yon* +#def Contra-evid-yon ( A : U) - ( is-pre-∞-category-A : is-pre-∞-category A) + ( is-pre-∞-category-A : Is-pre-∞-category A) ( a b : A) - ( v : hom A a b) - : contra-evid* A a b (contra-yon* A is-pre-∞-category-A a b v) = v + ( v : Hom A a b) + : Contra-evid A a b (Contra-yon A is-pre-∞-category-A a b v) = v := - id-comp-is-pre-∞-category A is-pre-∞-category-A a b v + Id-comp-is-pre-∞-category A is-pre-∞-category-A a b v ``` -The other composite carries $ϕ$ to an a priori distinct natural transformation. -We first show that these are pointwise equal at all `#!rzk x : A` and -`#!rzk f : hom A x a` in two steps. +The other composite carries $ϕ$ to an a priori distinct natural +transformation. We first show that these are pointwise equal at all +`#!rzk x : A` and `#!rzk f : Hom A x a` in two steps. ```rzk #section contra-yon-evid #variable A : U -#variable is-pre-∞-category-A : is-pre-∞-category A +#variable is-pre-∞-category-A : Is-pre-∞-category A #variables a b : A ``` -The composite `#!rzk contra-yon-evid` of `#!rzk ϕ` equals `#!rzk ϕ` at all -`#!rzk x : A` and `#!rzk f : hom A x a`. +The composite `#!rzk Contra-yon-evid` of `#!rzk ϕ` equals `#!rzk ϕ` at all +`#!rzk x : A` and `#!rzk f : Hom A x a`. ```rzk -#def contra-yon-evid-twice-pointwise* - ( ϕ : (z : A) → hom A z a → hom A z b) +#def Contra-yon-evid-twice-pointwise + ( ϕ : (z : A) → Hom A z a → Hom A z b) ( x : A) - ( f : hom A x a) - : ( ( contra-yon* A is-pre-∞-category-A a b) - ( ( contra-evid* A a b) ϕ)) x f = ϕ x f + ( f : Hom A x a) + : ( ( Contra-yon A is-pre-∞-category-A a b) + ( ( Contra-evid A a b) ϕ)) x f = ϕ x f := concat - ( hom A x b) - ( ( ( contra-yon* A is-pre-∞-category-A a b) - ( ( contra-evid* A a b) ϕ)) x f) - ( ϕ x (comp-is-pre-∞-category A is-pre-∞-category-A x a a f (id-hom A a))) + ( Hom A x b) + ( ( ( Contra-yon A is-pre-∞-category-A a b) + ( ( Contra-evid A a b) ϕ)) x f) + ( ϕ x (Comp-is-pre-∞-category A is-pre-∞-category-A x a a f (Id-hom A a))) ( ϕ x f) - ( naturality-contravariant-fiberwise-representable-transformation** - A is-pre-∞-category-A a b x a f (id-hom A a) ϕ) + ( Naturality-contravariant-fiberwise-representable-transformation + A is-pre-∞-category-A a b x a f (Id-hom A a) ϕ) ( ap - ( hom A x a) - ( hom A x b) - ( comp-is-pre-∞-category A is-pre-∞-category-A x a a f (id-hom A a)) + ( Hom A x a) + ( Hom A x b) + ( Comp-is-pre-∞-category A is-pre-∞-category-A x a a + f (Id-hom A a)) ( f) ( ϕ x) - ( comp-id-is-pre-∞-category A is-pre-∞-category-A x a f)) + ( Comp-id-is-pre-∞-category A is-pre-∞-category-A x a f)) ``` By `#!rzk funext`, these are equals as functions of `#!rzk f` pointwise in `#!rzk x`. ```rzk -#def contra-yon-evid-once-pointwise* uses (funext) - ( ϕ : (z : A) → hom A z a → hom A z b) +#def Contra-yon-evid-once-pointwise uses (funext) + ( ϕ : (z : A) → Hom A z a → Hom A z b) ( x : A) - : ( ( contra-yon* A is-pre-∞-category-A a b) - ( ( contra-evid* A a b) ϕ)) x = ϕ x + : ( ( Contra-yon A is-pre-∞-category-A a b) + ( ( Contra-evid A a b) ϕ)) x = ϕ x := eq-htpy funext - ( hom A x a) - ( \ f → hom A x b) + ( Hom A x a) + ( \ f → Hom A x b) ( \ f → - ( ( contra-yon* A is-pre-∞-category-A a b) - ( ( contra-evid* A a b) ϕ)) x f) + ( ( Contra-yon A is-pre-∞-category-A a b) + ( ( Contra-evid A a b) ϕ)) x f) ( \ f → (ϕ x f)) - ( \ f → contra-yon-evid-twice-pointwise* ϕ x f) + ( \ f → Contra-yon-evid-twice-pointwise ϕ x f) ``` By `#!rzk funext` again, these are equal as functions of `#!rzk x` and `#!rzk f`. ```rzk -#def contra-yon-evid* uses (funext) - ( ϕ : (z : A) → hom A z a → hom A z b) - : contra-yon* A is-pre-∞-category-A a b (contra-evid* A a b ϕ) = ϕ +#def Contra-yon-evid uses (funext) + ( ϕ : (z : A) → Hom A z a → Hom A z b) + : Contra-yon A is-pre-∞-category-A a b (Contra-evid A a b ϕ) = ϕ := eq-htpy funext ( A) - ( \ x → (hom A x a → hom A x b)) - ( contra-yon* A is-pre-∞-category-A a b (contra-evid* A a b ϕ)) + ( \ x → (Hom A x a → Hom A x b)) + ( Contra-yon A is-pre-∞-category-A a b (Contra-evid A a b ϕ)) ( ϕ) - ( contra-yon-evid-once-pointwise* ϕ) + ( Contra-yon-evid-once-pointwise ϕ) #end contra-yon-evid ``` @@ -338,122 +566,244 @@ The contravariant Yoneda lemma says that evaluation at the identity defines an equivalence. ```rzk -#def contra-yoneda-lemma* uses (funext) +#def Contra-yoneda-lemma uses (funext) ( A : U) - ( is-pre-∞-category-A : is-pre-∞-category A) + ( is-pre-∞-category-A : Is-pre-∞-category A) ( a b : A) - : is-equiv ((z : A) → hom A z a → hom A z b) (hom A a b) (contra-evid* A a b) + : is-equiv ((z : A) → Hom A z a → Hom A z b) (Hom A a b) (Contra-evid A a b) := - ( ( ( contra-yon* A is-pre-∞-category-A a b) - , ( contra-yon-evid* A is-pre-∞-category-A a b)) - , ( ( contra-yon* A is-pre-∞-category-A a b) - , ( contra-evid-yon* A is-pre-∞-category-A a b))) + ( ( ( Contra-yon A is-pre-∞-category-A a b) + , ( Contra-yon-evid A is-pre-∞-category-A a b)) + , ( ( Contra-yon A is-pre-∞-category-A a b) + , ( Contra-evid-yon A is-pre-∞-category-A a b))) ``` ## Contravariant Naturality The equivalence of the Yoneda lemma is natural in both $a : A$ and $b : A$. -Naturality in $a$ follows from the fact that the maps `#!rzk evid` and -`#!rzk yon` are fiberwise equivalences between contravariant families over $A$, -though it requires some work, which has not yet been formalized, to prove that -the domain is contravariant. - Naturality in $b$ is not automatic but can be proven easily: ```rzk title="RS17, Lemma 9.2(i), dual" -#def is-natural-in-family-contra-evid* +#def Is-natural-in-family-contra-evid ( A : U) ( a b b' : A) - ( ψ : (z : A) → hom A z b → hom A z b') - ( φ : (z : A) → hom A z a → hom A z b) - : ( comp ((z : A) → hom A z a → hom A z b) (hom A a b) (hom A a b') - ( ψ a) (contra-evid* A a b)) φ - = ( comp ((z : A) → hom A z a → hom A z b) ((z : A) → hom A z a → hom A z b') - ( hom A a b') - ( contra-evid* A a b') (\ α z g → ψ z (α z g))) φ + ( ψ : (z : A) → Hom A z b → Hom A z b') + ( φ : (z : A) → Hom A z a → Hom A z b) + : ( comp ((z : A) → Hom A z a → Hom A z b) (Hom A a b) (Hom A a b') + ( ψ a) (Contra-evid A a b)) φ + = ( comp ((z : A) → Hom A z a → Hom A z b) ((z : A) → Hom A z a → Hom A z b') + ( Hom A a b') + ( Contra-evid A a b') (\ α z g → ψ z (α z g))) φ := refl ``` ```rzk title="RS17, Lemma 9.2(ii), dual" -#def is-natural-in-family-contra-yon-twice-pointwise* +#def Is-natural-in-family-contra-yon-twice-pointwise ( A : U) - ( is-pre-∞-category-A : is-pre-∞-category A) + ( is-pre-∞-category-A : Is-pre-∞-category A) ( a b b' : A) - ( ψ : (z : A) → hom A z b → hom A z b') - ( u : hom A a b) + ( ψ : (z : A) → Hom A z b → Hom A z b') + ( u : Hom A a b) ( x : A) - ( f : hom A x a) - : ( comp (hom A a b) (hom A a b') ((z : A) → hom A z a → hom A z b') - ( contra-yon* A is-pre-∞-category-A a b') (ψ a)) u x f - = ( comp (hom A a b) - ( ( z : A) → hom A z a → hom A z b) - ( ( z : A) → hom A z a → hom A z b') + ( f : Hom A x a) + : ( comp (Hom A a b) (Hom A a b') ((z : A) → Hom A z a → Hom A z b') + ( Contra-yon A is-pre-∞-category-A a b') (ψ a)) u x f + = ( comp (Hom A a b) + ( ( z : A) → Hom A z a → Hom A z b) + ( ( z : A) → Hom A z a → Hom A z b') ( \ α z g → ψ z (α z g)) - ( contra-yon* A is-pre-∞-category-A a b)) u x f + ( Contra-yon A is-pre-∞-category-A a b)) u x f := - naturality-contravariant-fiberwise-representable-transformation** + Naturality-contravariant-fiberwise-representable-transformation A is-pre-∞-category-A b b' x a f u ψ - -#def is-natural-in-family-contra-yon-once-pointwise* uses (funext) +#def Is-natural-in-family-contra-yon-once-pointwise uses (funext) ( A : U) - ( is-pre-∞-category-A : is-pre-∞-category A) + ( is-pre-∞-category-A : Is-pre-∞-category A) ( a b b' : A) - ( ψ : (z : A) → hom A z b → hom A z b') - ( u : hom A a b) + ( ψ : (z : A) → Hom A z b → Hom A z b') + ( u : Hom A a b) ( x : A) - : ( comp (hom A a b) (hom A a b') ((z : A) → hom A z a → hom A z b') - ( contra-yon* A is-pre-∞-category-A a b') (ψ a)) u x - = ( comp (hom A a b) - ( ( z : A) → hom A z a → hom A z b) - ( ( z : A) → hom A z a → hom A z b') + : ( comp (Hom A a b) (Hom A a b') ((z : A) → Hom A z a → Hom A z b') + ( Contra-yon A is-pre-∞-category-A a b') (ψ a)) u x + = ( comp (Hom A a b) + ( ( z : A) → Hom A z a → Hom A z b) + ( ( z : A) → Hom A z a → Hom A z b') ( \ α z g → ψ z (α z g)) - ( contra-yon* A is-pre-∞-category-A a b)) u x + ( Contra-yon A is-pre-∞-category-A a b)) u x := eq-htpy funext - ( hom A x a) - ( \ f → hom A x b') + ( Hom A x a) + ( \ f → Hom A x b') ( \ f → - ( comp (hom A a b) (hom A a b') ((z : A) → hom A z a → hom A z b') - ( contra-yon* A is-pre-∞-category-A a b') (ψ a)) u x f) + ( comp (Hom A a b) (Hom A a b') ((z : A) → Hom A z a → Hom A z b') + ( Contra-yon A is-pre-∞-category-A a b') (ψ a)) u x f) ( \ f → - ( comp (hom A a b) - ( ( z : A) → hom A z a → hom A z b) - ( ( z : A) → hom A z a → hom A z b') + ( comp (Hom A a b) + ( ( z : A) → Hom A z a → Hom A z b) + ( ( z : A) → Hom A z a → Hom A z b') ( \ α z g → ψ z (α z g)) - ( contra-yon* A is-pre-∞-category-A a b)) u x f) + ( Contra-yon A is-pre-∞-category-A a b)) u x f) ( \ f → - is-natural-in-family-contra-yon-twice-pointwise* + Is-natural-in-family-contra-yon-twice-pointwise A is-pre-∞-category-A a b b' ψ u x f) -#def is-natural-in-family-contra-yon* uses (funext) +#def Is-natural-in-family-contra-yon uses (funext) ( A : U) - ( is-pre-∞-category-A : is-pre-∞-category A) + ( is-pre-∞-category-A : Is-pre-∞-category A) ( a b b' : A) - ( ψ : (z : A) → hom A z b → hom A z b') - ( u : hom A a b) - : ( comp (hom A a b) (hom A a b') ((z : A) → hom A z a → hom A z b') - ( contra-yon* A is-pre-∞-category-A a b') (ψ a)) u - = ( comp (hom A a b) - ( ( z : A) → hom A z a → hom A z b) - ( ( z : A) → hom A z a → hom A z b') + ( ψ : (z : A) → Hom A z b → Hom A z b') + ( u : Hom A a b) + : ( comp (Hom A a b) (Hom A a b') ((z : A) → Hom A z a → Hom A z b') + ( Contra-yon A is-pre-∞-category-A a b') (ψ a)) u + = ( comp (Hom A a b) + ( ( z : A) → Hom A z a → Hom A z b) + ( ( z : A) → Hom A z a → Hom A z b') ( \ α z g → ψ z (α z g)) - ( contra-yon* A is-pre-∞-category-A a b)) u + ( Contra-yon A is-pre-∞-category-A a b)) u := eq-htpy funext ( A) - ( \ x → hom A x a → hom A x b') + ( \ x → Hom A x a → Hom A x b') ( \ x → - ( comp (hom A a b) (hom A a b') ((z : A) → hom A z a → hom A z b') - ( contra-yon* A is-pre-∞-category-A a b') (ψ a)) u x) + ( comp (Hom A a b) (Hom A a b') ((z : A) → Hom A z a → Hom A z b') + ( Contra-yon A is-pre-∞-category-A a b') (ψ a)) u x) ( \ x → - ( comp (hom A a b) - ( ( z : A) → hom A z a → hom A z b) - ( ( z : A) → hom A z a → hom A z b') + ( comp (Hom A a b) + ( ( z : A) → Hom A z a → Hom A z b) + ( ( z : A) → Hom A z a → Hom A z b') ( \ α z g → ψ z (α z g)) - ( contra-yon* A is-pre-∞-category-A a b)) u x) + ( Contra-yon A is-pre-∞-category-A a b)) u x) ( \ x → - is-natural-in-family-contra-yon-once-pointwise* + Is-natural-in-family-contra-yon-once-pointwise A is-pre-∞-category-A a b b' ψ u x) ``` + +Naturality in $a$ follows formally, but also can be proven directly. The proof +requires associativity and thus extension extensionality. + +```rzk title="RS17, Lemma 9.2(i), dual" +#def Is-natural-in-object-contra-evid + ( A : U) + ( is-pre-∞-category-A : Is-pre-∞-category A) + ( a' a b : A) + ( k : Hom A a' a) + ( φ : (z : A) → Hom A z a → Hom A z b) + : ( comp ((z : A) → Hom A z a → Hom A z b) (Hom A a b) (Hom A a' b) + ( \ f → Comp-is-pre-∞-category A is-pre-∞-category-A a' a b k f) + ( Contra-evid A a b)) φ + = ( comp ((z : A) → Hom A z a → Hom A z b) ((z : A) → Hom A z a' → Hom A z b) + ( Hom A a' b) + ( Contra-evid A a' b) + ( \ α z g → + α z (Comp-is-pre-∞-category A is-pre-∞-category-A z a' a g k))) φ + := + concat (Hom A a' b) + ( Comp-is-pre-∞-category A is-pre-∞-category-A a' a b k (φ a (Id-hom A a))) + ( φ a' (Comp-is-pre-∞-category A is-pre-∞-category-A a' a a k (Id-hom A a))) + ( φ a' (Comp-is-pre-∞-category A is-pre-∞-category-A a' a' a (Id-hom A a') k)) + ( Naturality-contravariant-fiberwise-representable-transformation + A is-pre-∞-category-A a b a' a k (Id-hom A a) φ) + ( ap (hom A a' a) (hom A a' b) + ( Comp-is-pre-∞-category A is-pre-∞-category-A a' a a k (Id-hom A a)) + ( Comp-is-pre-∞-category A is-pre-∞-category-A a' a' a (Id-hom A a') k) + ( \ h → φ a' h) + ( concat (hom A a' a) + ( Comp-is-pre-∞-category A is-pre-∞-category-A a' a a k (Id-hom A a)) + ( k) + ( Comp-is-pre-∞-category A is-pre-∞-category-A a' a' a (Id-hom A a') k) + ( Comp-id-is-pre-∞-category A is-pre-∞-category-A a' a k) + ( rev (hom A a' a) + ( Comp-is-pre-∞-category A is-pre-∞-category-A a' a' a (Id-hom A a') k) + ( k) + ( Id-comp-is-pre-∞-category A is-pre-∞-category-A a' a k)))) +``` + +```rzk +#def Is-natural-in-obj-contra-yon-twice-pointwise uses (extext) + ( A : U) + ( is-pre-∞-category-A : Is-pre-∞-category A) + ( a' a b : A) + ( k : Hom A a' a) + ( u : Hom A a b) + ( x : A) + ( g : Hom A x a') + : ( comp (Hom A a b) + ( ( z : A) → Hom A z a → Hom A z b) + ( ( z : A) → Hom A z a' → Hom A z b) + ( \ α z g → α z (Comp-is-pre-∞-category A is-pre-∞-category-A z a' a g k)) + ( Contra-yon A is-pre-∞-category-A a b)) u x g + = ( comp (Hom A a b) (Hom A a' b) ((z : A) → Hom A z a' → Hom A z b) + ( Contra-yon A is-pre-∞-category-A a' b) + ( \ f → Comp-is-pre-∞-category A is-pre-∞-category-A a' a b k f)) u x g + := associative-is-pre-∞-category extext A is-pre-∞-category-A x a' a b g k u + +#def Is-natural-in-obj-contra-yon-once-pointwise uses (funext extext) + ( A : U) + ( is-pre-∞-category-A : Is-pre-∞-category A) + ( a' a b : A) + ( k : Hom A a' a) + ( u : Hom A a b) + ( x : A) + : ( comp (Hom A a b) + ( ( z : A) → Hom A z a → Hom A z b) + ( ( z : A) → Hom A z a' → Hom A z b) + ( \ α z g → α z (Comp-is-pre-∞-category A is-pre-∞-category-A z a' a g k)) + ( Contra-yon A is-pre-∞-category-A a b)) u x + = ( comp (Hom A a b) (Hom A a' b) ((z : A) → Hom A z a' → Hom A z b) + ( Contra-yon A is-pre-∞-category-A a' b) + ( \ f → Comp-is-pre-∞-category A is-pre-∞-category-A a' a b k f)) u x + := + eq-htpy funext + ( Hom A x a') + ( \ g → Hom A x b) + ( \ g → + ( comp (Hom A a b) + ( ( z : A) → Hom A z a → Hom A z b) + ( ( z : A) → Hom A z a' → Hom A z b) + ( \ α z g → + α z (Comp-is-pre-∞-category A is-pre-∞-category-A z a' a g k)) + ( Contra-yon A is-pre-∞-category-A a b)) u x g) + ( \ g → + ( comp (Hom A a b) (Hom A a' b) ((z : A) → Hom A z a' → Hom A z b) + ( Contra-yon A is-pre-∞-category-A a' b) + ( \ f → Comp-is-pre-∞-category A is-pre-∞-category-A a' a b k f)) + u x g) + ( \ g → + Is-natural-in-obj-contra-yon-twice-pointwise + A is-pre-∞-category-A a' a b k u x g) + +#def Is-natural-in-obj-contra-yon uses (funext extext) + ( A : U) + ( is-pre-∞-category-A : Is-pre-∞-category A) + ( a' a b : A) + ( k : Hom A a' a) + ( u : Hom A a b) + : ( comp (Hom A a b) + ( ( z : A) → Hom A z a → Hom A z b) + ( ( z : A) → Hom A z a' → Hom A z b) + ( \ α z g → α z (Comp-is-pre-∞-category A is-pre-∞-category-A z a' a g k)) + ( Contra-yon A is-pre-∞-category-A a b)) u + = ( comp (Hom A a b) (Hom A a' b) ((z : A) → Hom A z a' → Hom A z b) + ( Contra-yon A is-pre-∞-category-A a' b) + ( \ f → Comp-is-pre-∞-category A is-pre-∞-category-A a' a b k f)) u + := + eq-htpy funext + ( A) + ( \ x → Hom A x a' → Hom A x b) + ( \ x → + ( comp (Hom A a b) + ( ( z : A) → Hom A z a → Hom A z b) + ( ( z : A) → Hom A z a' → Hom A z b) + ( \ α z g → + α z (Comp-is-pre-∞-category A is-pre-∞-category-A z a' a g k)) + ( Contra-yon A is-pre-∞-category-A a b)) u x) + ( \ x → + ( comp (Hom A a b) (Hom A a' b) ((z : A) → Hom A z a' → Hom A z b) + ( Contra-yon A is-pre-∞-category-A a' b) + ( \ f → Comp-is-pre-∞-category A is-pre-∞-category-A a' a b k f)) u x) + ( \ x → + Is-natural-in-obj-contra-yon-once-pointwise + A is-pre-∞-category-A a' a b k u x) +``` From 88b61837635927b40a936ba91a30281747a183ea Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Tue, 25 Jun 2024 18:53:12 +0200 Subject: [PATCH 4/4] line edits --- .vscode/settings.json | 2 +- lean/_target/deps/mathlib | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index 81f2497..48797b5 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -15,7 +15,7 @@ "editor.inlineSuggest.enabled": true, "editor.acceptSuggestionOnEnter": "off", "editor.snippetSuggestions": "top", - "editor.wordBasedSuggestions": false, + "editor.wordBasedSuggestions": "off", "javascript.suggest.names": false, // Autoformatting and file type specific settings diff --git a/lean/_target/deps/mathlib b/lean/_target/deps/mathlib index 246f6f7..442a83d 160000 --- a/lean/_target/deps/mathlib +++ b/lean/_target/deps/mathlib @@ -1 +1 @@ -Subproject commit 246f6f7989ff86bd07e1b014846f11304f33cf9e +Subproject commit 442a83d738cb208d3600056c489be16900ba701d