Library TypeTheory.ALV1.Transport_along_Equivs
TypeTheory.ALV1.Transport_Along_Equivs
Part of the TypeTheory library (Ahrens, Lumsdaine, Voevodsky, 2015–present).
This file provides two results:
Given a universe in preShv C relative to the Yoneda embedding Yo : C ⟶ preShv C ,
and a fully faithful and essentially surjective functor F : C ⟶ D,
and D is a univalent category, then
we obtain a universe relative to Yo : D ⟶ preShv D
Furthermore, given a weak equivalence F : C ⟶ D as above,
then we obtain an equivalence of
weak universes on Yo C and on Yo D.
Put differently, weak relative universes (and hence representable maps of presheaves)
are invariant under weak equivalences, whereas cwf structures
are not - even though they can be transported along weak equivalences
in the direction of the underlying functor if the target category is univalent.
The results of this file could (should, actually) be instantiated
in order to obtain the result of ALV1.RelUnivYonedaCompletion.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.CategoryTheory.precomp_ess_surj.
Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
Require Import TypeTheory.Auxiliary.Auxiliary.
Require Import TypeTheory.Auxiliary.UnicodeNotations.
Require Import TypeTheory.ALV1.RelativeUniverses.
Set Automatic Introduction.
< C ------------> preShv C | | /\ | F | | precomp with F^op v V | D ------------> preShv D>
Context {C D : category}
(F : functor C D)
(F_ff : fully_faithful F)
(F_es : essentially_surjective F).
Definition Fop_precomp : preShv D ⟶ preShv C.
Proof.
use (pre_composition_functor C^op D^op HSET _ _ (functor_opp F) ).
apply has_homsets_opp. apply homset_property.
Defined.
Definition ff_Fop_precomp : fully_faithful Fop_precomp.
Proof.
apply pre_composition_with_ess_surj_and_fully_faithful_is_fully_faithful.
+ apply opp_functor_essentially_surjective. apply F_es.
+ apply opp_functor_fully_faithful. apply F_ff.
Defined.
Definition es_Fop_precomp : essentially_surjective Fop_precomp.
Proof.
apply pre_composition_essentially_surjective.
+ apply opp_functor_essentially_surjective. apply F_es.
+ apply opp_functor_fully_faithful. apply F_ff.
Defined.
Definition equiv_Fcomp : adj_equivalence_of_precats Fop_precomp.
Proof.
apply rad_equivalence_of_precats.
- apply is_univalent_functor_category.
- apply ff_Fop_precomp.
- apply es_Fop_precomp.
Defined.
Definition has_homsets_preShv X : has_homsets (preShv X).
Proof.
apply functor_category_has_homsets.
Defined.
Definition epsinv : iso (C:=[_ , _ , has_homsets_preShv _ ])
(functor_identity (preShv C)) (ext ∙ Fop_precomp).
Proof.
set (XR':= (counit_iso_from_adj_equivalence_of_precats (has_homsets_preShv _ ) equiv_Fcomp)).
apply iso_inv_from_iso.
apply XR'.
Defined.
Definition etainv : iso (C:=[ _ , _ , (has_homsets_preShv _ )])
(Fop_precomp ∙ ext) (functor_identity (preShv D)).
Proof.
set (XR := (unit_iso_from_adj_equivalence_of_precats (has_homsets_preShv _ ) equiv_Fcomp)).
apply iso_inv_from_iso.
apply XR.
Defined.
Definition fi : iso (C:=[C, preShv D])
(functor_composite Yo ext)
(functor_composite F Yo).
Proof.
set (T:= @iso_from_fully_faithful_reflection _ _
(pre_composition_functor C^op _ HSET (has_homsets_opp (homset_property _) ) has_homsets_HSET
(functor_opp (F)))
).
set (XTT := ff_Fop_precomp).
specialize (T XTT).
set (XR := iso_from_iso_with_postcomp).
apply (XR _ _ _ (functor_category_has_homsets _ _ _ )
(functor_category_has_homsets _ _ _ ) _ _ _ XTT).
eapply iso_comp.
apply functor_assoc_iso.
eapply iso_comp.
eapply functor_precomp_iso.
apply counit_iso_from_adj_equivalence_of_precats.
eapply iso_comp.
apply functor_comp_id_iso.
exists (yoneda_functor_precomp_nat_trans _ _ _ _ _ ).
apply functor_iso_if_pointwise_iso.
intro c. apply is_iso_yoneda_functor_precomp.
apply F_ff.
Defined.
Lemma preserves_pullbacks_ext
: maps_pb_squares_to_pb_squares (preShv C) (preShv D) ext.
Proof.
intros ? ? ? ? ? ? ? ? ? ?.
apply isPullback_image_square.
apply functor_category_has_homsets.
apply right_adj_equiv_is_ff.
apply right_adj_equiv_is_ess_sur.
assumption.
Defined.
Definition Transfer_of_RelUnivYoneda (Dcat : is_univalent D) (X : @relative_universe C _ Yo)
: relative_universe
((yoneda D (homset_property D) : functor D (preShv D))
:
functor D (preShv D)).
Proof.
cbn.
use (transfer_of_rel_univ_with_ess_surj
Yo
X
Yo
F
ext
fi
(pr2 fi)
preserves_pullbacks_ext
F_es
Dcat
(yoneda_fully_faithful _ _ )
(right_adj_equiv_is_full _ _)
).
Defined.
Lemma is_univalent_preShv X : is_univalent (preShv X).
Proof.
apply is_univalent_functor_category.
Defined.
Definition Transfer_of_WeakRelUnivYoneda :
weak_relative_universe (yoneda C (homset_property C)) ≃
weak_relative_universe (yoneda D (homset_property D)).
Proof.
set (XR := @weq_weak_relative_universe_transfer
C
(preShv C)
(yoneda C (homset_property C))
D
(preShv D)
Yo
F
ext
fi
(pr2 fi)
preserves_pullbacks_ext
F_es
(right_adj_equiv_is_full _ _)
(full_from_ff _ F_ff)
(is_univalent_preShv _ )
(is_univalent_preShv _ )
Fop_precomp
).
use XR.
- apply epsinv.
- apply etainv.
- apply right_adj_equiv_is_ff.
Defined.
End fix_category.