module Cat.Univalent.Rezk.Universal where
private variable o β : Level A B C CβΊ : Precategory o β private module _ {o β} {C : Precategory o β} where open Cat.Reasoning C using (_β _) open _β _ public -- Using β/Β·Β· over equational reasoning saves ~5k conversion checks
Universal property of the Rezk completionπ
With the Rezk completion, we defined, for any precategory , a univalent category , together with a weak equivalence functor . We also stated, but did not in that module prove, the universal property of the Rezk completion: The functor is the universal map from to categories. This module actually proves it, but be warned: the proof is very technical, and is mostly a calculation.
In generic terms, universality of the Rezk completion follows from univalent categories being the class of local objects for the weak equivalences1: A category is univalent precisely if any weak equivalence induces2 a proper equivalence of categories .
The high-level overview of the proof is as follows:
For any eso , and for any , all precategories, the functor is faithful. This is the least technical part of the proof, so we do it first.
If is additionally full, then is fully faithful.
If is a weak equivalence, and is univalent, then is essentially surjective. By the principle of unique choice, it is an equivalence, and thus3 an isomorphism.
Faithfulnessπ
The argument here is almost elementary: Weβre given a witness that , so all we have to do is manipulate the expression to something which has a subexpression. Since is eso, given , we can find and an iso , from which we can calculate:
esoβpre-faithful : (H : Functor A B) {F G : Functor B C} β is-eso H β (Ξ³ Ξ΄ : F => G) β (β b β Ξ³ .Ξ· (H .Fβ b) β‘ Ξ΄ .Ξ· (H .Fβ b)) β Ξ³ β‘ Ξ΄ esoβpre-faithful {A = A} {B = B} {C = C} H {F} {G} h-eso Ξ³ Ξ΄ p = Nat-path Ξ» b β β₯-β₯-proj {ap = C.Hom-set _ _ _ _} do (bβ² , m) β h-eso b β₯_β₯.inc $ Ξ³ .Ξ· b β‘β¨ C.intror (F-map-iso F m .invl) β©β‘ Ξ³ .Ξ· b C.β F.β (m .to) C.β F.β (m .from) β‘β¨ C.extendl (Ξ³ .is-natural _ _ _) β©β‘ G.β (m .to) C.β Ξ³ .Ξ· _ C.β F.β (m .from) β‘β¨ apβ C._β_ refl (apβ C._β_ (p bβ²) refl) β©β‘ G.β (m .to) C.β Ξ΄ .Ξ· _ C.β F.β (m .from) β‘β¨ C.extendl (sym (Ξ΄ .is-natural _ _ _)) β©β‘ Ξ΄ .Ξ· b C.β F.β (m .to) C.β F.β (m .from) β‘β¨ C.elimr (F-map-iso F m .invl) β©β‘ Ξ΄ .Ξ· b β where module C = Cat.Reasoning C module F = Functor F module G = Functor G
The above is, unfortunately, the simplest result in this module. The next two proofs are both quite technical: thatβs because weβre given some mere4 data, from the assumption that is a weak equivalence, so to use it as proper data, we need to show that whatever we want lives in a contractible space, after which we are free to project only the data we are interested in, and forget about the coherences.
It will turn out, however, that the coherence data necessary to make these types contractible is exactly the coherence data we need to show that we are indeed building functors, natural transformations, etc. So, not only do we need it to use unique choice, we also need it to show weβre doing category theory.
Full-faithfulnessπ
Let , , and be as before, except now assume that is full (in addition to eso).
eso-fullβpre-ff : (H : Functor A B) β is-eso H β is-full H β is-fully-faithful {C = Cat[ B , C ]} (precompose H) eso-fullβpre-ff {A = A} {B = B} {C = C} H H-eso H-full = res where
We will show that, for every natural transformation , and each , there is a contractible type of βcomponent dataβ over . These data consist of morphisms , each equipped with a witness that acts naturally when faced with isomorphisms .
module A = Cat.Reasoning A module B = Cat.Reasoning B module C = Cat.Reasoning C module H = FR H module _ (F G : Functor B C) (Ξ³ : F Fβ H => G Fβ H) where module F = FR F module FH = FR (F Fβ H) module G = FR G module GH = FR (G Fβ H) module Ξ³ = _=>_ Ξ³
In more detail, if weβre given an essential fibre of over , we can use to βmatch upβ our component with the components of the natural transformation : since , weβve claimed to have a , and someone has just handed us a , then it darn well better be the case that is
T : B.Ob β Type _ T b = Ξ£ (C.Hom (F.β b) (G.β b)) Ξ» g β (a : A.Ob) (f : H.β a B.β b) β Ξ³.Ξ· a β‘ G.β (f .from) C.β g C.β F.β (f .to)
Weβll first show that components exist at all. Assume that we have some and an essential fibre of over it5. In this situation, guided by the compatibility condition (and isomorphisms being just the best), we can actually define the component to be βwhatever satisfies compatibility at ,β and a short calculation establishes that defining
g = G.β h.to C.β Ξ³.Ξ· aβ C.β F.β h.from
is indeed a possible choice. We present the formalisation below, but do not comment on the calculation, leaving it to the curious reader to load this file in Agda and poke around the proof.
lemma : (a : A.Ob) (f : H.β a B.β b) β Ξ³.Ξ· a β‘ G.β (f .from) C.β g C.β F.β (f .to) lemma a f = β₯-β₯-proj {ap = C.Hom-set _ _ _ _} do (k , p) β H-full (h.from B.β B.to f) (kβ»ΒΉ , q) β H-full (B.from f B.β h.to) β₯_β₯.inc $ C.intror (F.annihilate (apβ B._β_ q p Β·Β· B.cancel-inner h.invl Β·Β· f .invr)) Β·Β· C.extendl (Ξ³.is-natural _ _ _) Β·Β· apβ (Ξ» e eβ² β G.β e C.β Ξ³.Ξ· aβ C.β F.β eβ²) q p Β·Β· apβ (Ξ» e eβ² β e C.β Ξ³.Ξ· aβ C.β eβ²) (G.F-β _ _) (F.F-β _ _) Β·Β· C.pullr (ap (G.β h.to C.β_) (C.pulll refl) β C.pulll refl)
Anyway, because of how weβve phrased the coherence condition, if , both satisfy it, then we have equal to both and .6 Since isomorphisms are both monic and epic, we can cancel and from these equations to conclude . Since the coherence condition is a proposition, the type of component data over is a proposition.
T-prop : β b β is-prop (T b) T-prop b (g , coh) (gβ² , cohβ²) = Ξ£-prop-path (Ξ» x β Ξ -is-hlevelΒ² 1 Ξ» _ _ β C.Hom-set _ _ _ _) $ β₯-β₯-proj {ap = C.Hom-set _ _ _ _} do (aβ , h) β H-eso b pure $ C.isoβepic (F-map-iso F h) _ _ (C.isoβmonic (F-map-iso G (h B.Isoβ»ΒΉ)) _ _ (sym (coh aβ h) β cohβ² aβ h))
Given any , being eso means that we merely have an essential fibre of over . But since the type of components over is a proposition, if weβre going to use it to construct a component over , then we are granted the honour of actually getting hold of an pair.
mkTβ² : β b β β₯ Essential-fibre H b β₯ β β₯ T b β₯ mkTβ² b he = do (aβ , h) β he β₯_β₯.inc (Mk.g b aβ h , Mk.lemma b aβ h) mkT : β b β T b mkT b = β₯-β₯-proj {ap = T-prop b} (mkTβ² b (H-eso b))
Another calculation shows that, since is full, given any pair of essential fibres over and over , with a mediating map , we can choose a map satisfying , and since both the components at and βcome from β (which is natural), we get a naturality result for the transformation weβre defining, too.
That computation is a bit weirder, so itβs hidden in this <details>
tag.
module _ {b bβ²} (f : B.Hom b bβ²) (a aβ² : A.Ob) (h : H.β a B.β b) (hβ² : H.β aβ² B.β bβ²) where private module hβ² = B._β _ hβ² module h = B._β _ h naturality : _ naturality = β₯-β₯-proj {ap = C.Hom-set _ _ _ _} do (k , p) β H-full (hβ².from B.β f B.β h.to) pure $ C.pullr (C.pullr (F.weave (sym (B.pushl p β apβ B._β_ refl (B.cancelr h.invl))))) Β·Β· apβ C._β_ refl (C.extendl (Ξ³.is-natural _ _ _)) Β·Β· C.extendl (G.weave (B.lswizzle p hβ².invl))
Because of this naturality result, all the components weβve chosen piece together into a natural transformation. And since we defined parametrically over the choice of essential fibre, if weβre looking at some , then we can choose the identity isomorphism, from which it falls out that . Since we had already established that is faithful, and now weβve shown it is full, it is fully faithful.
Ξ΄ : F => G Ξ΄ .Ξ· b = mkT b .fst Ξ΄ .is-natural b bβ² f = β₯-β₯-elimβ {P = Ξ» Ξ± Ξ² β β₯-β₯-proj {ap = T-prop bβ²} (mkTβ² bβ² Ξ±) .fst C.β F.β f β‘ G.β f C.β β₯-β₯-proj {ap = T-prop b} (mkTβ² b Ξ²) .fst} (Ξ» _ _ β C.Hom-set _ _ _ _) (Ξ» (aβ² , hβ²) (a , h) β naturality f a aβ² h hβ²) (H-eso bβ²) (H-eso b) full : is-full (precompose H) full {x = x} {y = y} Ξ³ = pure (Ξ΄ _ _ Ξ³ , Nat-path p) where p : β b β Ξ΄ _ _ Ξ³ .Ξ· (H.β b) β‘ Ξ³ .Ξ· b p b = subst (Ξ» e β β₯-β₯-proj {ap = T-prop _ _ Ξ³ (H.β b)} (mkTβ² _ _ Ξ³ (H.β b) e) .fst β‘ Ξ³ .Ξ· b) (squash (inc (b , B.id-iso)) (H-eso (H.β b))) (C.eliml (y .F-id) β C.elimr (x .F-id)) res : is-fully-faithful (precompose H) res = full+faithfulβff (precompose H) full Ξ» {F} {G} {Ξ³} {Ξ΄} p β esoβpre-faithful H H-eso Ξ³ Ξ΄ Ξ» b β p Ξ·β b
Essential surjectivityπ
The rest of the proof proceeds in this same way: Define a type which characterises, up to a compatible space of choices, first the action on morphisms of a functor which inverts , and in terms of this type, the action on morphisms. Itβs mostly the same trick as above, but a lot wilder. We do not comment on it too extensively: the curious reader, again, can load this file in Agda and play around.
module _ {ao aβ bo bβ co cβ} {A : Precategory ao aβ} {B : Precategory bo bβ} {C : Precategory co cβ} (H : Functor A B) (H-eso : is-eso H) (H-ff : is-fully-faithful H) (c-cat : is-category C) where private module A = Cat.Reasoning A module B = Cat.Reasoning B module C = Cat.Reasoning C module H = FfR H H-ff
The type of object-candidates Obs is indexed by a , and any object candidate must come with a family of isomorphisms giving, for every way of expressing as coming from , a way of coming from . To show this type is a proposition, we additionally require a naturality condition for these isomorphisms.
private module _ (F : Functor A C) where private module F = FR F Obs : B.Ob β Type _ Obs b = Ξ£ C.Ob Ξ» c β Ξ£ ((a : A.Ob) (h : H.β a B.β b) β F.β a C.β c) Ξ» k β ((a , h) (aβ² , hβ²) : Essential-fibre H b) (f : A.Hom a aβ²) β hβ² .to B.β H.β f β‘ h .to β k aβ² hβ² .to C.β F.β f β‘ k a h .to
Note that we can derive an object candidate over from a fibre of over . Moreover, this choice is a center of contraction, so we can once more apply unique choice and the assumption that is eso to conclude that every has an object candidate over it.
objβ² : β {b} β Essential-fibre H b β Obs b objβ² (aβ , hβ) .fst = F.β aβ objβ² (aβ , hβ) .snd .fst a h = F-map-iso F (H.iso.from (h B.βIso (hβ B.Isoβ»ΒΉ))) objβ² (aβ , hβ) .snd .snd (a , h) (aβ² , hβ²) f p = F.collapse (H.ipushr p) Obs-is-prop : β {b} (f : Essential-fibre H b) (c : Obs b) β objβ² f β‘ c Obs-is-prop (aβ , hβ) (cβ² , kβ² , Ξ²) = Ξ£-pathp (Univalent.isoβpath c-cat cβ cβ²) $ Ξ£-prop-pathp (Ξ» i x β Ξ -is-hlevelΒ³ 1 Ξ» _ _ _ β Ξ -is-hlevel 1 Ξ» _ β C.Hom-set _ _ _ _) $ funextP Ξ» a β funextP Ξ» h β C.β -pathp _ _ $ Univalent.Hom-pathp-reflr-iso c-cat {q = cβ cβ²} ( C.pullr (F.eliml (H.from-id (hβ .invr))) β Ξ² _ _ _ (H.Ξ΅-lswizzle (hβ .invl))) where ckΞ± = objβ² (aβ , hβ) c = ckΞ± .fst k = ckΞ± .snd .fst Ξ± = ckΞ± .snd .snd cβ cβ² = (k aβ hβ C.Isoβ»ΒΉ) C.βIso kβ² aβ hβ
summon : β {b} β β₯ Essential-fibre H b β₯ β is-contr (Obs b) summon f = β₯-β₯-proj {ap = is-contr-is-prop} do f β f pure $ contr (objβ² f) (Obs-is-prop f) Gβ : B.Ob β C.Ob Gβ b = summon {b = b} (H-eso b) .centre .fst k : β {b} a (h : H.β a B.β b) β F.β a C.β Gβ b k {b = b} a h = summon {b = b} (H-eso b) .centre .snd .fst a h kcomm : β {b} ((a , h) (aβ² , hβ²) : Essential-fibre H b) (f : A.Hom a aβ²) β hβ² .to B.β H.β f β‘ h .to β k aβ² hβ² .to C.β F.β f β‘ k a h .to kcomm {b} f1 f2 f w = summon {b = b} (H-eso b) .centre .snd .snd f1 f2 f w
We will write Gβ for the canonical choice of object candidate, and k for the associated family of isomorphisms. The type of morphism candidates over consists of maps which are compatible with the reindexing isomorphisms for any essential fibre over , over , and map satisfying .
compat : β {b bβ²} (f : B.Hom b bβ²) β C.Hom (Gβ b) (Gβ bβ²) β Type _ compat {b} {bβ²} f g = β a (h : H.β a B.β b) aβ² (hβ² : H.β aβ² B.β bβ²) (l : A.Hom a aβ²) β hβ² .to B.β H.β l β‘ f B.β h .to β k aβ² hβ² .to C.β F.β l β‘ g C.β k a h .to Homs : β {b bβ²} (f : B.Hom b bβ²) β Type _ Homs {b = b} {bβ²} f = Ξ£ (C.Hom (Gβ b) (Gβ bβ²)) (compat f)
compat-prop : β {b bβ²} (f : B.Hom b bβ²) {g : C.Hom (Gβ b) (Gβ bβ²)} β is-prop (compat f g) compat-prop f = Ξ -is-hlevelΒ³ 1 Ξ» _ _ _ β Ξ -is-hlevelΒ³ 1 Ξ» _ _ _ β C.Hom-set _ _ _ _
It will again turn out that any initial choice of fibre over and gives a morphism candidate over , and the compatibility data is exactly what we need to show the type of morphism candidates is a proposition.
This proof really isnβt commented. Iβm sorry.
module _ {b bβ²} (f : B.Hom b bβ²) aβ (hβ : H.β aβ B.β b) aββ² (hββ² : H.β aββ² B.β bβ²) where lβ : A.Hom aβ aββ² lβ = H.from (hββ² .from B.β f B.β hβ .to) p : hββ² .to B.β H.β lβ β‘ (f B.β hβ .to) p = H.Ξ΅-lswizzle (hββ² .invl) gβ : C.Hom (Gβ b) (Gβ bβ²) gβ = k aββ² hββ² .to C.β F.β lβ C.β k aβ hβ .from module _ a (h : H.β a B.β b) aβ² (hβ² : H.β aβ² B.β bβ²) (l : A.Hom a aβ²) (w : hβ² .to B.β H.β l β‘ f B.β h .to) where m : aβ A.β a m = H.iso.from (hβ B.βIso (h B.Isoβ»ΒΉ)) mβ² : aββ² A.β aβ² mβ² = H.iso.from (hββ² B.βIso (hβ² B.Isoβ»ΒΉ)) Ξ± : k aβ hβ .from β‘ F.β (m .from) C.β k a h .from Ξ± = C.inverse-unique _ _ {f = k aβ hβ} {g = F-map-iso F m C.βIso k a h} $ sym (kcomm _ _ _ (H.Ξ΅-lswizzle (h .invl))) Ξ³ : H.β (mβ² .to) B.β H.β lβ β‘ H.β l B.β H.β (m .to) Ξ³ = B.pushl (H.Ξ΅ _) Β·Β· apβ B._β_ refl (p β B.pushl (B.insertr (h .invl) β apβ B._β_ (sym w) refl)) Β·Β· B.deletel (hβ² .invr) β apβ B._β_ refl (sym (H.Ξ΅ _)) Ξ³β² : lβ A.β m .from β‘ mβ² .from A.β l Ξ³β² = A.isoβmonic mβ² _ _ $ A.extendl (H.injective (H.swap Ξ³)) Β·Β· A.elimr (m .invl) Β·Β· A.insertl (mβ² .invl) Ξ΄ : gβ C.β k a h .to β‘ k aβ² hβ² .to C.β F.β l Ξ΄ = C.pullr ( C.pullr refl Β·Β· apβ C._β_ refl (C.pushl Ξ±) Β·Β· C.pulll refl β C.elimr (k a h .invr)) Β·Β· apβ C._β_ refl (F.weave Ξ³β²) Β·Β· C.pulll (C.pushl (sym (kcomm _ _ _ (H.Ξ΅-lswizzle (hβ² .invl)))) β C.elimr (F.annihilate (mβ² .invl))) Homs-pt : Homs f Homs-pt = gβ , Ξ» a h aβ² hβ² l w β sym (Ξ΄ a h aβ² hβ² l w) Homs-propβ² : (hβ² : Homs f) β hβ² .fst β‘ gβ Homs-propβ² (gβ , w) = C.isoβepic (k aβ hβ) _ _ (sym (Ξ΄ aβ hβ aββ² hββ² lβ p β w aβ hβ aββ² hββ² lβ p)) Homs-contrβ² : β {b bβ²} (f : B.Hom b bβ²) β β₯ is-contr (Homs f) β₯ Homs-contrβ² {b = b} {bβ²} f = do (aβ , h) β H-eso b (aββ² , hβ²) β H-eso bβ² inc (contr (Homs-pt f aβ h aββ² hβ²) Ξ» hβ² β Ξ£-prop-path (Ξ» _ β compat-prop f) (sym (Homs-propβ² f _ _ _ _ hβ²))) Homs-contr : β {b bβ²} (f : B.Hom b bβ²) β is-contr (Homs f) Homs-contr f = β₯-β₯-proj (Homs-contrβ² f) Gβ : β {b bβ²} β B.Hom b bβ² β C.Hom (Gβ b) (Gβ bβ²) Gβ f = Homs-contr f .centre .fst
Using the compatibility condition, and choices of , we can show that the assignment of morphism candidates does assemble into a functor.
module Gβ {x y z} (f : B.Hom y z) (g : B.Hom x y) {ax ay az} (hx : H.β ax B.β x) (hy : H.β ay B.β y) (hz : H.β az B.β z) where af : A.Hom ay az af = H.from (hz .from B.β f B.β hy .to) ag : A.Hom ax ay ag = H.from (hy .from B.β g B.β hx .to) hβ² : H.β (af A.β ag) β‘ hz .from B.β f B.β g B.β hx .to hβ² = H.Ξ΅-expand refl β B.pullr (B.cancel-inner (hy .invl)) commutes : Gβ (f B.β g) β‘ Gβ f C.β Gβ g commutes = C.isoβepic (k ax hx) _ _ $ sym (Homs-contr (f B.β g) .centre .snd ax hx az hz (af A.β ag) (apβ B._β_ refl hβ² Β·Β· B.cancell (hz .invl) Β·Β· B.pulll refl)) β sym ( C.pullr (sym (Homs-contr g .centre .snd ax hx ay hy ag (H.Ξ΅-lswizzle (hy .invl)))) β C.pulll (sym (Homs-contr f .centre .snd ay hy az hz af (H.Ξ΅-lswizzle (hz .invl)))) β F.pullr refl)
In this manner, the assignment of object candidates and morphism candidates fits together into a functor . After finishing this, we have to show that . But the compatibility data which we have used to uniquely characterise β¦ uniquely characterises , after all, and it does so as composing with to give .
G : Functor B C G .Fβ b = Gβ b G .Fβ f = Gβ f G .F-id = ap fst $ Homs-contr B.id .paths $ C.id , Ξ» a h aβ² hβ² l w β sym (C.idl _ β sym (kcomm (a , h) (aβ² , hβ²) l (w β B.idl _)))
Note that we proved7 that is functorial given choices of essential fibres of all three objects involved in the composition. Since weβre showing an equality in a set β a proposition β these choices donβt matter, so we can use essential surjectivity of .
G .F-β {x} {y} {z} f g = β₯-β₯-proj do (ax , hx) β H-eso x (ay , hy) β H-eso y (az , hz) β H-eso z inc (Gβ.commutes f g hx hy hz)
To use the unique charactersation of as βthe functor satisfying β, observe: for any , the object can be made into an object candidate over , and since the type of object candidates is a proposition, our candidate is identical to the value of . Thatβs half of established right off the bat!
module _ (x : A.Ob) where hf-obs : Obs (H.β x) hf-obs .fst = F.Fβ x hf-obs .snd .fst a h = F-map-iso F (H.iso.from h) hf-obs .snd .snd (a , h) (aβ² , hβ²) f Ξ± = F.collapse (H.invβl Ξ±) abstract objp : Gβ (H.β x) β‘ F.β x objp = ap fst $ summon {H.β x} (H-eso _) .paths hf-obs
kp : (a : A.Ob) (h : H.β a B.β H.β x) β PathP (Ξ» i β F.β a C.β objp i) (k a h) (hf-obs .snd .fst a h) kp a h = ap (Ξ» e β e .snd .fst a h) (summon {H.β x} (H-eso (H.β x)) .paths hf-obs)
Over that identification, we can show that, for any in , the value is also a candidate for the morphism , so these are also identical. This proof is a bit hairier, because only has the right type if we adjust it by the proof that : we have to transport , and then as punishment for our hubris, invoke a lot of technical lemmas about the characterisation of PathP in the morphism spaces of (pre)categories.
module _ {x y} (f : A.Hom x y) where homβ² : Homs (H.β f) homβ² .fst = transport (Ξ» i β C.Hom (objp x (~ i)) (objp y (~ i))) (F.β f) homβ² .snd a h aβ² hβ² l w = sym $ C.pushl (Hom-transport C (sym (objp x)) (sym (objp y)) (F.β f)) Β·Β· apβ C._β_ refl ( C.pullr (from-pathp-from C (objp x) (Ξ» i β kp x a h i .to)) β F.weave (H.Ξ΅-twist (sym w))) Β·Β· C.pulll (from-pathp-to C (sym (objp y)) Ξ» i β kp y aβ² hβ² (~ i) .to) homp : transport (Ξ» i β C.Hom (objp x (~ i)) (objp y (~ i))) (F.β f) β‘ Homs-contr (H.β f) .centre .fst homp = ap fst $ sym $ Homs-contr (H.β f) .paths homβ² correct : G Fβ H β‘ F correct = Functor-path objp Ξ» {x} {y} f β symP {A = Ξ» i β C.Hom (objp x (~ i)) (objp y (~ i))} $ to-pathp (homp f)
Since weβve shown that , so in particular , weβve now put together proofs that is fully faithful and, since the construction above works for any , essentially surjective. Even better, since weβve actually constructed a functor , weβve shown that is split essentially surjective! Since is univalent whenever is, the splitting would be automatic, but this is a nice strengthening.
weak-equivβpre-equiv : is-equivalence {C = Cat[ B , C ]} (precompose H) weak-equivβpre-equiv = ff+split-esoβis-equivalence {F = precompose H} (eso-fullβpre-ff H H-eso Ξ» g β inc (H.from g , H.Ξ΅ g)) Ξ» F β G F , pathβiso (correct F)
And since a functor is an equivalence of categories iff. it is an isomorphism of categories, we also have that the rule sending to its is an equivalence of types.
weak-equivβpre-iso : is-precat-iso {C = Cat[ B , C ]} (precompose H) weak-equivβpre-iso = is-equivalenceβis-precat-iso (precompose H) weak-equivβpre-equiv (Functor-is-category c-cat) (Functor-is-category c-cat)
Restating the result that acts on objects as an equivalence of types, we have the following result: If is a weak equivalence (a fully faithful and essentially surjective functor), then for any category and functor , there is a contractible space(!) of extensions which factor through .
weak-equivβreflection : (F : Functor C CβΊ) β is-eso F β is-fully-faithful F β {D : Precategory o β} β is-category D β (G : Functor C D) β is-contr (Ξ£ (Functor CβΊ D) Ξ» H β H Fβ F β‘ G) weak-equivβreflection F F-eso F-ff D-cat G = weak-equivβpre-iso F F-eso F-ff D-cat .is-precat-iso.has-is-iso .is-eqv G
Note that this is only half of the point of the Rezk completion: we would also like for to be univalent, but that is not necessary for to think that precomposition with is an isomorphism.
a weak equivalence is a fully faithful, essentially surjective functorβ©οΈ
since both its domain and codomain are univalentβ©οΈ
truncatedβ©οΈ
Donβt worry about actually getting your hands on an .β©οΈ
Iβve implicitly used that is eso to cough up an over , since weβre proving a propositionβ©οΈ
in the second
<details>
tag aboveβ©οΈ