./._Ahrens-Coq000777 000765 000024 00000000260 12404034062 013723 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/000777 000765 000024 00000000000 12404034062 013425 5ustar00nicolastaff000000 000000 Ahrens-Coq/._auxiliary_lemmas_HoTT.v000777 000765 000024 00000000260 12262322302 020274 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/auxiliary_lemmas_HoTT.v000777 000765 000024 00000015735 12262322302 020074 0ustar00nicolastaff000000 000000 Require Import Foundations.Generalities.uu0. Require Import Foundations.hlevel1.hProp. Require Import Foundations.hlevel2.hSet. Require Import RezkCompletion.pathnotations. Import RezkCompletion.pathnotations.PathNotations. Definition propproperty ( X : hProp ) := pr2 X . (** * Paths in total spaces are equivalent to pairs of paths *) (** some of the lemmas are proved for similar fibrations twice: once we consider fibrations over a type in universe [UU], once we consider fibrations over the universe [UU] itself *) Lemma total2_paths {A : UU} {B : A -> UU} {s s' : total2 (fun x => B x)} (p : pr1 s == pr1 s') (q : transportf (fun x => B x) p (pr2 s) == pr2 s') : s == s'. Proof. destruct s as [a b]; destruct s' as [a' b']. simpl in p; destruct p. simpl in q; destruct q. apply idpath. Defined. Lemma total2_paths_hProp (A : UU) (B : A -> UU) (is : forall a, isaprop (B a)) (s s' : total2 (fun x => B x)) : pr1 s == pr1 s' -> s == s'. Proof. intro h. apply (total2_paths h). apply proofirrelevance. apply is. Defined. Lemma total2_paths_UU {B : UU -> UU} {s s' : total2 (fun x => B x)} (p : pr1 s == pr1 s') (q : transportf (fun x => B x) p (pr2 s) == pr2 s') : s == s'. Proof. destruct s as [a b]; destruct s' as [a' b']. simpl in p; destruct p. simpl in q; destruct q. apply idpath. Defined. Lemma total2_paths2 {A : UU} {B : A -> UU} {a1 : A} {b1 : B a1} {a2 : A} {b2 : B a2} (p : a1 == a2) (q : transportf (fun x => B x) p b1 == b2) : tpair (fun x => B x) a1 b1 == tpair (fun x => B x) a2 b2. Proof. set (H := @total2_paths _ _ (tpair (fun x => B x) a1 b1)(tpair (fun x => B x) a2 b2)). simpl in H. apply (H p q). Defined. Lemma total2_paths2_UU {B : UU -> UU} {A A': UU} {b : B A} {b' : B A'} (p : A == A') (q : transportf (fun x => B x) p b == b') : tpair (fun x => B x) A b == tpair (fun x => B x) A' b'. Proof. set (H := @total2_paths _ _ (tpair (fun x => B x) A b)(tpair (fun x => B x) A' b')). simpl in H. apply (H p q). Defined. Lemma base_paths {A : UU}{B : A -> UU}(a b : total2 B) : a == b -> pr1 a == pr1 b. Proof. apply maponpaths. Defined. Lemma base_paths_UU {B : UU -> UU}(a b : total2 B) : a == b -> pr1 a == pr1 b. Proof. intro H. apply (maponpaths (@pr1 _ _) H). Defined. Definition fiber_path {A : UU} {B : A -> UU} {u v : total2 (fun x => B x)} (p : u == v) : transportf (fun x => B x) (base_paths _ _ p) (pr2 u) == pr2 v. Proof. destruct p. apply idpath. Defined. Definition fiber_path_UU {B : UU -> UU} {u v : total2 (fun x => B x)} (p : u == v) : transportf (fun x => B x) (base_paths_UU _ _ p) (pr2 u) == pr2 v. Proof. destruct p. apply idpath. Defined. Lemma total_path_reconstruction {A : UU} {B : A -> UU} {x y : total2 (fun x => B x)} (p : x == y) : total2_paths _ (fiber_path p) == p. Proof. induction p. destruct x. apply idpath. Defined. Lemma total_path_reconstruction_UU {B : UU -> UU} {x y : total2 (fun x => B x)} (p : x == y) : total2_paths_UU _ (fiber_path_UU p) == p. Proof. induction p. destruct x. apply idpath. Defined. Lemma base_total_path {A : UU} {B : A -> UU} {x y : total2 (fun x => B x)} {p : pr1 x == pr1 y} (q : transportf _ p (pr2 x) == pr2 y) : (base_paths _ _ (total2_paths _ q)) == p. Proof. destruct x as [x H]. destruct y as [y K]. simpl in p. induction p. simpl in q. induction q. apply idpath. Defined. Lemma base_total_path_UU {B : UU -> UU} {x y : total2 (fun x => B x)} {p : pr1 x == pr1 y} (q : transportf _ p (pr2 x) == pr2 y) : (base_paths_UU _ _ (total2_paths_UU _ q)) == p. Proof. destruct x as [x H]. destruct y as [y K]. simpl in p. induction p. simpl in q. induction q. apply idpath. Defined. Lemma fiber_total_path {A : UU} (B : A -> UU) (x y : total2 (fun x => B x)) (p : pr1 x == pr1 y) (q : transportf _ p (pr2 x) == pr2 y) : transportf (fun p' : pr1 x == pr1 y => transportf _ p' (pr2 x) == pr2 y) (base_total_path q) (fiber_path (total2_paths _ q)) == q. Proof. destruct x as [x H]. destruct y as [y K]. simpl in p. induction p. simpl in q. induction q. apply idpath. Defined. Lemma fiber_total_path_UU (B : UU -> UU) (x y : total2 (fun x => B x)) (p : pr1 x == pr1 y) (q : transportf _ p (pr2 x) == pr2 y) : transportf (fun p' : pr1 x == pr1 y => transportf _ p' (pr2 x) == pr2 y) (base_total_path_UU q) (fiber_path_UU (total2_paths_UU _ q)) == q. Proof. destruct x as [x H]. destruct y as [y K]. simpl in p. induction p. simpl in q. induction q. apply idpath. Defined. Theorem total_paths_equiv {A : UU} (B : A -> UU) (x y : total2 (fun x => B x)) : weq (x == y) (total2 (fun p : pr1 x == pr1 y => transportf _ p (pr2 x) == pr2 y )). Proof. exists ( fun r : x == y => tpair (fun p : pr1 x == pr1 y => transportf _ p (pr2 x) == pr2 y) (base_paths _ _ r) (fiber_path r)). apply (gradth _ (fun pq : total2 (fun p : pr1 x == pr1 y => transportf _ p (pr2 x) == pr2 y) => total2_paths (pr1 pq) (pr2 pq))). intro p. simpl. apply total_path_reconstruction. intros [p q]. simpl. set (H':= base_total_path q). apply ( total2_paths2 (B := fun p : pr1 x == pr1 y => transportf (fun x : A => B x) p (pr2 x) == pr2 y) H'). apply fiber_total_path. Defined. Theorem total_paths2_hProp_equiv {A : UU} (B : A -> hProp) (x y : total2 (fun x => B x)): weq (x == y) (pr1 x == pr1 y). Proof. set (t := total_paths_equiv B x y). simpl in *. set (t':= isweqpr1 (fun p : pr1 x == pr1 y => transportf (fun x : A => B x) p (pr2 x) == pr2 y)). simpl in *. assert (H : forall z : pr1 x == pr1 y, iscontr (transportf (fun x : A => B x) z (pr2 x) == pr2 y)). intro p. set (H := pr2 (B (pr1 y))). simpl in H. apply (H _ (pr2 y)). simpl in *. set (Ht := t' H). set (ht := tpair _ _ Ht). set (HHH := weqcomp t ht). exact HHH. Defined. Theorem equal_transport_along_weq (A B : UU) (f : weq A B) (a a' : A) : f a == f a' -> a == a'. Proof. intro H. apply (!homotinvweqweq f a @ maponpaths (invmap f) H @ homotinvweqweq f a'). Defined. Definition equal_equalities_between_pairs (A : UU)(B : A -> UU)(x y : total2 (fun x => B x)) (p q : x == y) : total_paths_equiv _ _ _ p == total_paths_equiv _ _ _ q -> p == q := equal_transport_along_weq _ _ _ _ _ . (** This helper lemma is an adaptation of an analogous lemma [isweqpr1] from Voevodsky's Foundations library. Here, we prove it for predicates on path spaces in [UU]. *) Lemma isweqpr1_UU (X X' : UU) ( B : (X == X') -> UU ) ( is1 : forall z , iscontr ( B z ) ) : isweq ( @pr1 _ B ) . Proof. intros. unfold isweq. intro y. set (isy:= is1 y). apply (iscontrweqf ( ezweqpr1 B y)) . assumption. Defined. Lemma pairofobuip (C C': hSet) (a b : C) (c d : C') (p q : dirprod (a == b) (c == d)) : p == q. Proof. assert (H : pr1 p == pr1 q). apply uip. exact (pr2 C). apply (total2_paths H). apply uip. exact (pr2 C'). Qed. Ahrens-Coq/._category_hset.v000777 000765 000024 00000000260 12262322302 016671 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/category_hset.v000777 000765 000024 00000012452 12262322302 016462 0ustar00nicolastaff000000 000000 (** ********************************************************** Benedikt Ahrens, Chris Kapulkin, Mike Shulman january 2013 ************************************************************) (** ********************************************************** Contents : Precategory HSET of hSets HSET is a category ************************************************************) Require Import Foundations.Generalities.uu0. Require Import Foundations.hlevel1.hProp. Require Import Foundations.hlevel2.hSet. Require Import Foundations.Proof_of_Extensionality.funextfun. Require Import RezkCompletion.auxiliary_lemmas_HoTT. Require Import RezkCompletion.precategories. Require Import RezkCompletion.HLevel_n_is_of_hlevel_Sn. Require Import RezkCompletion.pathnotations. Import RezkCompletion.pathnotations.PathNotations. Local Notation "a --> b" := (precategory_morphisms a b)(at level 50). (** * Precategory of hSets *) Lemma isaset_set_fun_space (A B : hSet) : isaset (A -> B). Proof. change isaset with (isofhlevel 2). apply impred. apply (fun _ => (pr2 B)). Qed. Definition hset_fun_space (A B : hSet) : hSet := hSetpair _ (isaset_set_fun_space A B). Definition hset_precategory_ob_mor : precategory_ob_mor := tpair (fun ob : UU => ob -> ob -> hSet) hSet (fun A B : hSet => hset_fun_space A B). Definition hset_precategory_data : precategory_data := precategory_data_pair hset_precategory_ob_mor (fun (A:hSet) (x : A) => x) (fun (A B C : hSet) (f : A -> B) (g : B -> C) (x : A) => g (f x)). Lemma is_precategory_hset_precategory_data : is_precategory hset_precategory_data. Proof. repeat split; simpl. intros a b f. apply funextfunax; intros; apply idpath. intros; apply funextfunax; intros; apply idpath. Qed. Definition hset_precategory : precategory := tpair _ _ is_precategory_hset_precategory_data. Notation HSET := hset_precategory. (* Canonical Structure hset_precategory. :-) *) (** * The precategory of hSets is a category. *) (** ** Equivalence between isomorphisms and weak equivalences of two hsets. *) (** Given an iso, we construct a weak equivalence. This is basically unpacking and packing again. *) Lemma hset_iso_is_equiv (A B : ob HSET) (f : iso A B) : isweq (pr1 f). Proof. destruct f as [f fax]; simpl in *. apply (gradth _ (pr1 fax)). destruct fax as [g [eta eps]]; simpl in *. unfold compose, identity in *; simpl in *. intro x. apply (toforallpaths _ _ _ eta). destruct fax as [g [eta eps]]; simpl in *. unfold compose, identity in *; simpl in *. intro x. apply (toforallpaths _ _ _ eps). Defined. Lemma hset_iso_equiv (A B : ob HSET) : iso A B -> weq (pr1 A) (pr1 B). Proof. intro f. exists (pr1 f). apply hset_iso_is_equiv. Defined. (** Given a weak equivalence, we construct an iso. Again mostly unwrapping and packing. *) Lemma hset_equiv_is_iso (A B : hSet) (f : weq (pr1 A) (pr1 B)) : is_isomorphism (C:=HSET) (pr1 f). Proof. exists (invmap f). split; simpl. apply funextfunax; intro x; simpl in *. unfold compose, identity; simpl. apply homotinvweqweq. apply funextfunax; intro x; simpl in *. unfold compose, identity; simpl. apply homotweqinvweq. Defined. Lemma hset_equiv_iso (A B : ob HSET) : weq (pr1 A) (pr1 B) -> iso A B. Proof. intro f. simpl in *. exists (pr1 f). apply hset_equiv_is_iso. Defined. (** Both maps defined above are weak equivalences. *) Lemma hset_iso_equiv_is_equiv (A B : ob HSET) : isweq (hset_iso_equiv A B). Proof. apply (gradth _ (hset_equiv_iso A B)). intro; apply eq_iso; reflexivity. intro; apply total2_paths_hProp. intro; apply isapropisweq. reflexivity. Qed. Definition hset_iso_equiv_weq (A B : ob HSET) : weq (iso A B) (weq (pr1 A) (pr1 B)). Proof. exists (hset_iso_equiv A B). apply hset_iso_equiv_is_equiv. Defined. Lemma hset_equiv_iso_is_equiv (A B : ob HSET) : isweq (hset_equiv_iso A B). Proof. apply (gradth _ (hset_iso_equiv A B)). intro f. apply total2_paths_hProp. apply isapropisweq. reflexivity. intro; apply eq_iso. reflexivity. Qed. Definition hset_equiv_iso_weq (A B : ob HSET) : weq (weq (pr1 A) (pr1 B))(iso A B). Proof. exists (hset_equiv_iso A B). apply hset_equiv_iso_is_equiv. Defined. (** ** HSET is a category. *) Definition univalenceweq (X X' : UU) : weq (X == X') (weq X X') := tpair _ _ (univalenceaxiom X X'). Definition hset_id_iso_weq (A B : ob HSET) : weq (A == B) (iso A B) := weqcomp (UA_for_HLevels 2 A B) (hset_equiv_iso_weq A B). (** The map [precat_paths_to_iso] for which we need to show [isweq] is actually equal to the carrier of the weak equivalence we constructed above. We use this fact to show that that [precat_paths_to_iso] is an equivalence. *) Lemma hset_id_iso_weq_is (A B : ob HSET): @idtoiso _ A B == pr1 (hset_id_iso_weq A B). Proof. apply funextfunax. intro p; elim p. apply eq_iso; simpl. apply funextfun; intro x; destruct A. apply idpath. Defined. Lemma is_weq_precat_paths_to_iso_hset (A B : ob HSET): isweq (@idtoiso _ A B). Proof. rewrite hset_id_iso_weq_is. apply (pr2 (hset_id_iso_weq A B)). Defined. Lemma is_category_HSET : is_category HSET. Proof. unfold is_category. apply is_weq_precat_paths_to_iso_hset. Defined. Ahrens-Coq/._equivalences.v000777 000765 000024 00000000260 12262322302 016515 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/equivalences.v000777 000765 000024 00000032003 12262322302 016300 0ustar00nicolastaff000000 000000 (** ********************************************************** Benedikt Ahrens, Chris Kapulkin, Mike Shulman january 2013 ************************************************************) (** ********************************************************** Contents : Definition of adjunction Definition of equivalence of precategories Equivalence of categories yields weak equivalence of object types A fully faithful and ess. surjective functor induces equivalence of precategories, if the source is a category. ************************************************************) Require Import Foundations.Generalities.uu0. Require Import Foundations.hlevel1.hProp. Require Import Foundations.hlevel2.hSet. Require Import RezkCompletion.pathnotations. Import RezkCompletion.pathnotations.PathNotations. Require Import RezkCompletion.auxiliary_lemmas_HoTT. Require Import RezkCompletion.precategories. Require Import RezkCompletion.functors_transformations. Ltac pathvia b := (apply (@pathscomp0 _ _ b _ )). Local Notation "a --> b" := (precategory_morphisms a b)(at level 50). (*Local Notation "'hom' C" := (precategory_morphisms (C := C)) (at level 2).*) Local Notation "f ;; g" := (compose f g)(at level 50). Notation "[ C , D ]" := (functor_precategory C D). Local Notation "# F" := (functor_on_morphisms F)(at level 3). Definition functor_composite (A B C : precategory) (F : ob [A, B]) (G : ob [B , C]) : ob [A , C] := functor_composite _ _ _ F G. Notation "G 'O' F" := (functor_composite _ _ _ F G) (at level 25). (** * Adjunction *) Definition form_adjunction (A B : precategory) (F : ob [A, B]) (G : ob [B, A]) (eta : nat_trans (functor_identity A) (pr1 (G O F))) (eps : nat_trans (pr1 (F O G)) (functor_identity B)) : UU := dirprod (forall a : ob A, # (pr1 F) (pr1 eta a) ;; pr1 eps (pr1 F a) == identity (pr1 F a)) (forall b : ob B, pr1 eta (pr1 G b) ;; # (pr1 G) (pr1 eps b) == identity (pr1 G b)). Definition are_adjoints (A B : precategory) (F : ob [A, B]) (G : ob [B, A]) : UU := total2 (fun etaeps : dirprod (nat_trans (functor_identity A) (pr1 (G O F))) (nat_trans (pr1 (F O G)) (functor_identity B)) => form_adjunction A B F G (pr1 etaeps) (pr2 etaeps)). Definition is_left_adjoint (A B : precategory) (F : ob [A, B]) : UU := total2 (fun G : ob [B, A] => are_adjoints A B F G). Definition right_adjoint (A B : precategory) (F : ob [A, B]) (H : is_left_adjoint _ _ F) : ob [B, A] := pr1 H. Definition eta_from_left_adjoint (A B : precategory) (F : ob [A, B]) (H : is_left_adjoint _ _ F) : nat_trans (functor_identity A) (pr1 (pr1 H O F)) := pr1 (pr1 (pr2 H)). Definition eps_from_left_adjoint (A B : precategory) (F : ob [A, B]) (H : is_left_adjoint _ _ F) : nat_trans (pr1 (F O pr1 H)) (functor_identity B) := pr2 (pr1 (pr2 H)). Definition triangle_id_left_ad (A B : precategory) (F : ob [A, B]) (H : is_left_adjoint _ _ F) : forall (a : ob A), #(pr1 F) (pr1 (pr1 (pr1 (pr2 H))) a);; pr1 (pr2 (pr1 (pr2 H))) ((pr1 F) a) == identity ((pr1 F) a) := pr1 (pr2 (pr2 H)). Definition triangle_id_right_ad (A B : precategory) (F : ob [A, B]) (H : is_left_adjoint _ _ F) : forall b : ob B, pr1 (pr1 (pr1 (pr2 H))) ((pr1 (pr1 H)) b);; #(pr1 (pr1 H)) (pr1 (pr2 (pr1 (pr2 H))) b) == identity ((pr1 (pr1 H)) b) := pr2 (pr2 (pr2 H)). (** * Equivalence of (pre)categories *) Definition equivalence_of_precats (A B : precategory)(F : ob [A, B]) : UU := total2 (fun H : is_left_adjoint _ _ F => dirprod (forall a, is_isomorphism (eta_from_left_adjoint A B F H a)) (forall b, is_isomorphism (eps_from_left_adjoint A B F H b)) ). Definition eta_iso_from_equivalence_of_precats (A B : precategory) (F : ob [A, B]) (HF : equivalence_of_precats _ _ F) : iso (C:=[A, A]) (functor_identity A) (right_adjoint _ _ _ (pr1 HF) O F). Proof. exists (eta_from_left_adjoint _ _ _ (pr1 HF)). apply functor_iso_if_pointwise_iso. apply (pr1 (pr2 HF)). Defined. Definition eps_iso_from_equivalence_of_precats (A B : precategory) (F : ob [A, B]) (HF : equivalence_of_precats _ _ F) : iso (C:=[B, B]) (F O right_adjoint _ _ _ (pr1 HF)) (functor_identity B). Proof. exists (eps_from_left_adjoint _ _ _ (pr1 HF)). apply functor_iso_if_pointwise_iso. apply (pr2 (pr2 HF)). Defined. (** * Equivalence of categories yields equivalence of object types *) (** Fundamentally needed that both source and target are categories *) Lemma equiv_of_cats_is_weq_of_objects (A B : precategory) (HA : is_category A) (HB : is_category B) (F : ob [A, B]) (HF : equivalence_of_precats A B F) : isweq (pr1 (pr1 F)). Proof. set (G := right_adjoint _ _ _ (pr1 HF)). set (et := eta_iso_from_equivalence_of_precats _ _ _ HF). set (ep := eps_iso_from_equivalence_of_precats _ _ _ HF). set (AAcat := is_category_functor_category A _ HA). set (BBcat := is_category_functor_category B _ HB). set (Et := isotoid _ AAcat et). set (Ep := isotoid _ BBcat ep). apply (gradth _ (fun b => pr1 (right_adjoint A B F (pr1 HF)) b)). intro a. set (ou := toforallpaths _ _ _ (base_paths _ _ (base_paths _ _ Et)) a). simpl in ou. apply (! ou). intro y. set (ou := toforallpaths _ _ _ (base_paths _ _ (base_paths _ _ Ep)) y). apply ou. Defined. Definition weq_on_objects_from_equiv_of_cats (A B : precategory) (HA : is_category A) (HB : is_category B) (F : ob [A, B]) (HF : equivalence_of_precats A B F) : weq (ob A) (ob B). Proof. exists (pr1 (pr1 F)). apply equiv_of_cats_is_weq_of_objects; assumption. Defined. (** If the source precategory is a category, then being split essentially surjective is a proposition *) Lemma isaprop_sigma_iso (A B : precategory) (HA : is_category A) (F : ob [A, B]) (HF : fully_faithful F) : forall b : ob B, isaprop (total2 (fun a : ob A => iso (pr1 F a) b)). Proof. intro b. apply invproofirrelevance. intros x x'. destruct x as [a f]. destruct x' as [a' f']. set (fminusf := iso_comp f (iso_inv_from_iso f')). set (g := iso_from_fully_faithful_reflection HF _ _ fminusf). apply (total2_paths2 (B:=fun a' => iso ((pr1 F) a') b) (isotoid _ HA g)). pathvia (iso_comp (iso_inv_from_iso (functor_on_iso _ _ F _ _ (idtoiso (isotoid _ HA g)))) f). generalize (isotoid _ HA g). intro p0; destruct p0. rewrite <- functor_on_iso_inv. rewrite iso_inv_of_iso_id. apply eq_iso. simpl; rewrite functor_id. rewrite id_left. apply idpath. rewrite idtoiso_isotoid. unfold g; clear g. unfold fminusf; clear fminusf. assert (HFg : functor_on_iso A B F a a' (iso_from_fully_faithful_reflection HF a a' (iso_comp f (iso_inv_from_iso f'))) == iso_comp f (iso_inv_from_iso f')). generalize (iso_comp f (iso_inv_from_iso f')). intro h. apply eq_iso; simpl. set (H3:= homotweqinvweq (weq_from_fully_faithful HF a a')). simpl in H3. unfold fully_faithful_inv_hom. unfold invweq; simpl. rewrite H3; apply idpath. rewrite HFg. rewrite iso_inv_of_iso_comp. apply eq_iso; simpl. repeat rewrite <- assoc. rewrite iso_after_iso_inv. rewrite id_right. set (H := iso_inv_iso_inv _ _ _ f'). set (h':= base_paths _ _ H). assumption. Qed. Lemma isaprop_pi_sigma_iso (A B : precategory) (HA : is_category A) (F : ob [A, B]) (HF : fully_faithful F) : isaprop (forall b : ob B, total2 (fun a : ob A => iso (pr1 F a) b)). Proof. apply impred. intro b. apply isaprop_sigma_iso; assumption. Qed. (** * From full faithfullness and ess surj to equivalence *) (** A fully faithful and ess. surjective functor induces an equivalence of precategories, if the source is a category. *) Section from_fully_faithful_and_ess_surj_to_equivalence. Variables A B : precategory. Hypothesis HA : is_category A. Variable F : ob [A, B]. Hypothesis HF : fully_faithful F. Hypothesis HS : essentially_surjective F. (** Definition of a functor which will later be the right adjoint. *) Definition rad_ob : ob B -> ob A. Proof. intro b. apply (pr1 (HS b (tpair (fun x => isaprop x) _ (isaprop_sigma_iso A B HA F HF b)) (fun x => x))). Defined. (** Definition of the epsilon transformation *) Definition rad_eps (b : ob B) : iso (pr1 F (rad_ob b)) b. Proof. apply (pr2 (HS b (tpair (fun x => isaprop x) _ (isaprop_sigma_iso A B HA F HF b)) (fun x => x))). Defined. (** The right adjoint on morphisms *) Definition rad_mor (b b' : ob B) (g : b --> b') : rad_ob b --> rad_ob b'. Proof. set (epsgebs' := rad_eps b ;; g ;; iso_inv_from_iso (rad_eps b')). set (Gg := fully_faithful_inv_hom HF (rad_ob b) _ epsgebs'). exact Gg. Defined. (** Definition of the eta transformation *) Definition rad_eta (a : ob A) : a --> rad_ob (pr1 F a). Proof. set (epsFa := inv_from_iso (rad_eps (pr1 F a))). exact (fully_faithful_inv_hom HF _ _ epsFa). Defined. (** Above data specifies a functor *) Definition rad_functor_data : functor_data B A. Proof. exists rad_ob. exact rad_mor. Defined. Lemma rad_is_functor : is_functor rad_functor_data. Proof. split; simpl. intro b. unfold rad_mor; simpl. rewrite id_right, iso_inv_after_iso, fully_faithful_inv_identity. apply idpath. intros a b c f g. unfold rad_mor; simpl. rewrite <- fully_faithful_inv_comp. apply maponpaths. repeat rewrite <- assoc. repeat apply maponpaths. rewrite assoc. rewrite iso_after_iso_inv, id_left. apply idpath. Qed. Definition rad : ob [B, A]. Proof. exists rad_functor_data. apply rad_is_functor. Defined. (** Epsilon is natural *) Lemma rad_eps_is_nat_trans : is_nat_trans (pr1 (F O rad)) (functor_identity B) (fun b => rad_eps b). Proof. unfold is_nat_trans. simpl. intros b b' g. unfold rad_mor; unfold fully_faithful_inv_hom. set (H3 := homotweqinvweq (weq_from_fully_faithful HF (pr1 rad b) (pr1 rad b'))). simpl in *. rewrite H3; clear H3. repeat rewrite <- assoc. rewrite iso_after_iso_inv, id_right. apply idpath. Qed. Definition rad_eps_trans : nat_trans _ _ := tpair _ _ rad_eps_is_nat_trans. (** Eta is natural *) Ltac inv_functor x y := let H:=fresh in set (H:= homotweqinvweq (weq_from_fully_faithful HF x y)); simpl in H; unfold fully_faithful_inv_hom; simpl; rewrite H; clear H. Lemma rad_eta_is_nat_trans : is_nat_trans (functor_identity A) (pr1 (rad O F)) (fun a => rad_eta a). Proof. unfold is_nat_trans. simpl. intros a a' f. unfold rad_mor. simpl. apply (equal_transport_along_weq _ _ (weq_from_fully_faithful HF a (rad_ob ((pr1 F) a')))). simpl; repeat rewrite functor_comp. unfold rad_eta. set (HHH := rad_eps_is_nat_trans (pr1 F a) (pr1 F a')). simpl in HHH; rewrite <- HHH; clear HHH. inv_functor a' (rad_ob ((pr1 F) a')). inv_functor a (rad_ob ((pr1 F) a)). inv_functor (rad_ob (pr1 F a)) (rad_ob ((pr1 F) a')). unfold rad_mor. simpl. repeat rewrite <- assoc. rewrite iso_inv_after_iso. rewrite id_right. inv_functor (rad_ob (pr1 F a)) (rad_ob ((pr1 F) a')). repeat rewrite assoc. rewrite iso_after_iso_inv. rewrite id_left. apply idpath. Qed. Definition rad_eta_trans : nat_trans _ _ := tpair _ _ rad_eta_is_nat_trans. (** The data [rad], [eta], [eps] forms an adjunction *) Lemma rad_form_adjunction : form_adjunction A B F rad rad_eta_trans rad_eps_trans. Proof. split; simpl. intro a. unfold rad_eta. inv_functor a (rad_ob (pr1 F a)). rewrite iso_after_iso_inv. apply idpath. intro b. apply (equal_transport_along_weq _ _ (weq_from_fully_faithful HF (rad_ob b) (rad_ob b))). simpl; rewrite functor_comp. unfold rad_eta. inv_functor (rad_ob b) (rad_ob (pr1 F (rad_ob b))). unfold rad_mor. inv_functor (rad_ob (pr1 F (rad_ob b))) (rad_ob b). repeat rewrite assoc. rewrite iso_after_iso_inv. rewrite <- assoc. rewrite iso_inv_after_iso. rewrite id_left. rewrite functor_id. apply idpath. Qed. Definition rad_are_adjoints : are_adjoints _ _ F rad. Proof. exists (dirprodpair rad_eta_trans rad_eps_trans). apply rad_form_adjunction. Defined. Definition rad_is_left_adjoint : is_left_adjoint _ _ F. Proof. exists rad. apply rad_are_adjoints. Defined. (** Get an equivalence of precategories: remains to show that [eta], [eps] are isos *) Lemma rad_equivalence_of_precats : equivalence_of_precats _ _ F. Proof. exists rad_is_left_adjoint. split; simpl. intro a. unfold rad_eta. set (H := fully_faithful_reflects_iso_proof _ _ _ HF a (rad_ob ((pr1 F) a))). simpl in *. set (H' := H (iso_inv_from_iso (rad_eps ((pr1 F) a)))). change ((fully_faithful_inv_hom HF a (rad_ob ((pr1 F) a)) (inv_from_iso (rad_eps ((pr1 F) a))))) with (fully_faithful_inv_hom HF a (rad_ob ((pr1 F) a)) (iso_inv_from_iso (rad_eps ((pr1 F) a)))). apply H'. intro b. apply (pr2 (rad_eps b)). Defined. End from_fully_faithful_and_ess_surj_to_equivalence. Ahrens-Coq/._functors_transformations.v000777 000765 000024 00000000260 12262322302 021205 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/functors_transformations.v000777 000765 000024 00000064771 12262322302 021011 0ustar00nicolastaff000000 000000 (** ********************************************************** Benedikt Ahrens, Chris Kapulkin, Mike Shulman january 2013 ************************************************************) (** ********************************************************** Contents : - Functors - preserve isos, inverses - fully faithful functors - preserve isos, inverses, composition backwards - essentially surjective - faithful - full - fully faithful is the same as full and faithful - Image of a functor, full subcat specified by a functor - Natural transformations - Equality is pointwise equality. - Functor (pre)category - Isomorphisms in functor category are pointwise isomorphisms - Isomorphic Functors are equal if target precategory is category [functor_eq_from_functor_iso] - Functor precategory is category if target precategory is [is_category_functor_category] ************************************************************) Require Import Foundations.Generalities.uu0. Require Import Foundations.hlevel1.hProp. Require Import Foundations.hlevel2.hSet. Require Import RezkCompletion.pathnotations. Import RezkCompletion.pathnotations.PathNotations. Require Import RezkCompletion.auxiliary_lemmas_HoTT. Require Import RezkCompletion.precategories. Local Notation "a --> b" := (precategory_morphisms a b)(at level 50). Local Notation "f ;; g" := (compose f g)(at level 50). Ltac pathvia b := (apply (@pathscomp0 _ _ b _ )). (** * Functors : Morphisms of precategories *) Definition functor_data (C C' : precategory_ob_mor) := total2 ( fun F : ob C -> ob C' => forall a b : ob C, a --> b -> F a --> F b). Definition functor_on_objects {C C' : precategory_ob_mor} (F : functor_data C C') : ob C -> ob C' := pr1 F. Coercion functor_on_objects : functor_data >-> Funclass. Definition functor_on_morphisms {C C' : precategory_ob_mor} (F : functor_data C C') { a b : ob C} : a --> b -> F a --> F b := pr2 F a b. Local Notation "# F" := (functor_on_morphisms F)(at level 3). Definition is_functor {C C' : precategory_data} (F : functor_data C C') := dirprod (forall a : ob C, #F (identity a) == identity (F a)) (forall a b c : ob C, forall f : a --> b, forall g : b --> c, #F (f ;; g) == #F f ;; #F g). Lemma isaprop_is_functor (C C' : precategory_data) (F : functor_data C C'): isaprop (is_functor F). Proof. apply isofhleveldirprod. apply impred; intro a. apply (pr2 (_ --> _)). repeat (apply impred; intro). apply (pr2 (_ --> _)). Qed. Definition functor (C C' : precategory_data) := total2 ( fun F : functor_data C C' => is_functor F). Lemma functor_eq (C C' : precategory_data) (F F': functor C C'): pr1 F == pr1 F' -> F == F'. Proof. intro H. apply (total2_paths H). apply proofirrelevance. apply isaprop_is_functor. Defined. Definition functor_data_from_functor (C C': precategory_data) (F : functor C C') : functor_data C C' := pr1 F. Coercion functor_data_from_functor : functor >-> functor_data. Definition functor_eq_eq_from_functor_ob_eq (C C' : precategory_data) (F G : functor C C') (p q : F == G) (H : base_paths _ _ (base_paths _ _ p) == base_paths _ _ (base_paths _ _ q)) : p == q. Proof. apply equal_equalities_between_pairs. simpl. assert (H' : base_paths _ _ p == base_paths _ _ q). apply equal_equalities_between_pairs. simpl. apply (@total2_paths2 _ (fun p : pr1 (pr1 F) == pr1 (pr1 G) => transportf (fun x : ob C -> ob C' => (fun x0 : ob C -> ob C' => forall a b : ob C, a --> b -> x0 a --> x0 b) x) p (pr2 (pr1 F)) == pr2 (pr1 G)) _ (fiber_path (base_paths F G p)) _ (fiber_path (base_paths F G q)) H). apply uip. change (isaset) with (isofhlevel 2). apply impred; intro a. apply impred; intro b. apply impred; intro f. apply (pr2 (_ --> _)). apply (@total2_paths2 (pr1 F == pr1 G) (fun x : pr1 F == pr1 G => transportf _ x (pr2 F) == pr2 G) (base_paths F G p) (fiber_path p) (base_paths F G q) (fiber_path q) H'). apply uip. apply isasetaprop. apply isaprop_is_functor. Defined. Definition functor_id (C C' : precategory_data)(F : functor C C'): forall a : ob C, #F (identity a) == identity (F a) := pr1 (pr2 F). Definition functor_comp (C C' : precategory_data) (F : functor C C'): forall a b c : ob C, forall f : a --> b, forall g : b --> c, #F (f ;; g) == #F f ;; #F g := pr2 (pr2 F). (** ** Functors preserve isomorphisms *) Lemma is_inverse_functor_image (C C' : precategory) (F : functor C C') (a b : C) (f : iso a b): is_inverse_in_precat (#F f) (#F (inv_from_iso f)). Proof. simpl; split; simpl. rewrite <- functor_comp. rewrite iso_inv_after_iso. apply functor_id. rewrite <- functor_comp. rewrite (iso_after_iso_inv _ _ _ f). apply functor_id. Qed. Lemma functor_on_iso_is_iso (C C' : precategory) (F : functor C C') (a b : ob C)(f : iso a b) : is_isomorphism (#F f). Proof. exists (#F (inv_from_iso f)). simpl; apply is_inverse_functor_image. Defined. Definition functor_on_iso (C C' : precategory) (F : functor C C') (a b : ob C)(f : iso a b) : iso (F a) (F b). Proof. exists (#F f). apply functor_on_iso_is_iso. Defined. Lemma functor_on_iso_inv (C C' : precategory) (F : functor C C') (a b : ob C) (f : iso a b) : functor_on_iso _ _ F _ _ (iso_inv_from_iso f) == iso_inv_from_iso (functor_on_iso _ _ F _ _ f). Proof. apply eq_iso. simpl. apply idpath. Defined. (** ** Functors preserve inverses *) Lemma functor_on_inv_from_iso (C C' : precategory) (F : functor C C') (a b : ob C)(f : iso a b) : #F (inv_from_iso f) == inv_from_iso (functor_on_iso _ _ F _ _ f) . Proof. apply idpath. Qed. (** ** Fully faithful functors *) Definition fully_faithful {C D : precategory} (F : functor C D) := forall a b : ob C, isweq (functor_on_morphisms F (a:=a) (b:=b)). Lemma isaprop_fully_faithful (C D : precategory) (F : functor C D) : isaprop (fully_faithful F). Proof. apply impred; intro a. apply impred; intro b. apply isapropisweq. Qed. Definition weq_from_fully_faithful {C D : precategory}{F : functor C D} (FF : fully_faithful F) (a b : ob C) : weq (a --> b) (F a --> F b). Proof. exists (functor_on_morphisms F (a:=a) (b:=b)). exact (FF a b). Defined. Definition fully_faithful_inv_hom {C D : precategory}{F : functor C D} (FF : fully_faithful F) (a b : ob C) : F a --> F b -> a --> b := invweq (weq_from_fully_faithful FF a b). Local Notation "FF ^-1" := (fully_faithful_inv_hom FF _ _ ) (at level 20). Lemma fully_faithful_inv_identity (C D : precategory) (F : functor C D) (FF : fully_faithful F) (a : ob C) : FF^-1 (identity (F a)) == identity _. Proof. apply (equal_transport_along_weq _ _ (weq_from_fully_faithful FF a a)). unfold fully_faithful_inv_hom. set (HFaa:=homotweqinvweq (weq_from_fully_faithful FF a a)(identity _ )). simpl in *. rewrite HFaa. rewrite functor_id; apply idpath. Qed. Lemma fully_faithful_inv_comp (C D : precategory) (F : functor C D) (FF : fully_faithful F) (a b c : ob C) (f : F a --> F b) (g : F b --> F c) : FF^-1 (f ;; g) == FF^-1 f ;; FF^-1 g. Proof. apply (equal_transport_along_weq _ _ (weq_from_fully_faithful FF a c)). set (HFFac := homotweqinvweq (weq_from_fully_faithful FF a c) (f ;; g)). unfold fully_faithful_inv_hom. simpl in *. rewrite HFFac; clear HFFac. rewrite functor_comp. set (HFFab := homotweqinvweq (weq_from_fully_faithful FF a b) f). set (HFFbc := homotweqinvweq (weq_from_fully_faithful FF b c) g). simpl in *. rewrite HFFab; clear HFFab. rewrite HFFbc; clear HFFbc. apply idpath. Qed. (** *** Fully faithful functors reflect isos *) Lemma inv_of_ff_inv_is_inv (C D : precategory) (F : functor C D) (FF : fully_faithful F) (a b : C) (f : iso (F a) (F b)) : is_inverse_in_precat ((FF ^-1) f) ((FF ^-1) (inv_from_iso f)). Proof. unfold fully_faithful_inv_hom; simpl. split. apply (equal_transport_along_weq _ _ (weq_from_fully_faithful FF a a)). set (HFFab := homotweqinvweq (weq_from_fully_faithful FF a b)). set (HFFba := homotweqinvweq (weq_from_fully_faithful FF b a)). simpl in *. rewrite functor_comp. rewrite HFFab; clear HFFab. rewrite HFFba; clear HFFba. rewrite functor_id. apply iso_inv_after_iso. apply (equal_transport_along_weq _ _ (weq_from_fully_faithful FF b b)). set (HFFab := homotweqinvweq (weq_from_fully_faithful FF a b)). set (HFFba := homotweqinvweq (weq_from_fully_faithful FF b a)). simpl in *. rewrite functor_comp. rewrite HFFab. rewrite HFFba. rewrite functor_id. apply iso_after_iso_inv. Qed. Lemma fully_faithful_reflects_iso_proof (C D : precategory)(F : functor C D) (FF : fully_faithful F) (a b : ob C) (f : iso (F a) (F b)) : is_isomorphism (FF^-1 f). Proof. exists (FF^-1 (inv_from_iso f)). simpl; apply inv_of_ff_inv_is_inv. Defined. Definition iso_from_fully_faithful_reflection {C D : precategory}{F : functor C D} (HF : fully_faithful F) (a b : ob C) (f : iso (F a) (F b)) : iso a b. Proof. exists (fully_faithful_inv_hom HF a b f). apply fully_faithful_reflects_iso_proof. Defined. Lemma functor_on_iso_iso_from_fully_faithful_reflection (C D : precategory) (F : functor C D) (HF : fully_faithful F) (a b : ob C) (f : iso (F a) (F b)) : functor_on_iso _ _ F a b (iso_from_fully_faithful_reflection HF a b f) == f. Proof. apply eq_iso. simpl; apply (homotweqinvweq (weq_from_fully_faithful HF a b)). Qed. (** ** Essentially surjective functors *) Definition essentially_surjective {C D : precategory} (F : functor C D) := forall b, ishinh (total2 (fun a => iso (F a) b)). (** ** Faithful functors *) Definition faithful {C D : precategory} (F : functor C D) := forall a b : ob C, forall f g : a --> b, #F f == #F g -> f == g. Lemma isaprop_faithful (C D : precategory) (F : functor C D) : isaprop (faithful F). Proof. repeat (apply impred; intro). apply (pr2 (_ --> _)). Qed. (** ** Full functors *) Definition full {C D : precategory} (F : functor C D) := forall a b (g : F a --> F b), ishinh (total2 (fun f : a --> b => #F f == g)). (** ** Fully faithful is the same as full and faithful *) Definition full_and_faithful {C D : precategory} (F : functor C D) := dirprod (full F) (faithful F). Lemma fully_faithful_implies_full_and_faithful (C D : precategory) (F : functor C D) : fully_faithful F -> full_and_faithful F. Proof. intro H. split; simpl. unfold full. intros a b f. apply hinhpr. exists (fully_faithful_inv_hom H _ _ f). set (HFFaa := homotweqinvweq (weq_from_fully_faithful H a b)). simpl in HFFaa. apply HFFaa. unfold faithful. intros a b f g Heq. apply (equal_transport_along_weq _ _ (weq_from_fully_faithful H a b)). simpl. assumption. Qed. Lemma full_and_faithful_implies_fully_faithful (C D : precategory) (F : functor C D) : full_and_faithful F -> fully_faithful F. Proof. intros [Hfull Hfaith]. intros a b g. unfold full in Hfull. set (Hfull_f := Hfull a b g). assert (H : isaprop (iscontr (hfiber #F g))). apply isapropiscontr. apply (Hfull_f (hProppair (iscontr (hfiber #F g)) H)). simpl. intro X. exists X. unfold hfiber. intro t. unfold faithful in Hfaith. assert (HX : pr1 t == pr1 X). apply Hfaith. rewrite (pr2 t). set (H':= pr2 X). simpl in H'. rewrite H'. apply idpath. simpl in *. apply (total2_paths HX). apply proofirrelevance. apply (pr2 (F a --> F b)). Qed. Lemma isaprop_full_and_faithful (C D : precategory) (F : functor C D) : isaprop (full_and_faithful F). Proof. apply isofhleveldirprod. repeat (apply impred; intro). simpl. repeat (apply impred; intro). apply isapropishinh. apply isaprop_faithful. Qed. Definition weq_fully_faithful_full_and_faithful (C D : precategory) (F : functor C D) : weq (fully_faithful F) (full_and_faithful F) := weqimplimpl (fully_faithful_implies_full_and_faithful _ _ F) (full_and_faithful_implies_fully_faithful _ _ F) (isaprop_fully_faithful _ _ F) (isaprop_full_and_faithful _ _ F). (** ** Image on objects of a functor *) (** is used later to define the full image subcategory of a category [D] defined by a functor [F : C -> D] *) Definition is_in_img_functor {C D : precategory} (F : functor C D) (d : ob D) := ishinh ( total2 (fun c : ob C => iso (F c) d)). Definition sub_img_functor {C D : precategory}(F : functor C D) : hsubtypes (ob D) := fun d : ob D => is_in_img_functor F d. (** ** Composition of Functors, Identity Functors *) (** *** Composition *) Lemma functor_composite_ob_mor {C C' C'' : precategory} (F : functor C C') (F' : functor C' C'') : is_functor (tpair (fun F : ob C -> ob C'' => forall a b : ob C, a --> b -> F a --> F b) (fun a => F' (F a)) (fun (a b : ob C) f => #F' (#F f))). Proof. split; simpl. intro a. repeat rewrite functor_id. apply idpath. intros. repeat rewrite functor_comp. apply idpath. Qed. Definition functor_composite (C C' C'' : precategory) (F : functor C C') (F' : functor C' C'') : functor C C'' := tpair _ _ (functor_composite_ob_mor F F'). (** *** Identity functor *) Lemma functor_identity_ob_mor (C : precategory) : is_functor (tpair (fun F : ob C -> ob C => forall a b : ob C, a --> b -> F a --> F b) (fun a => a) (fun (a b : ob C) f => f)). Proof. split; simpl. intros; apply idpath. intros; apply idpath. Qed. Definition functor_identity (C : precategory) : functor C C. Proof. exists (tpair (fun F : ob C -> ob C => forall a b : ob C, a --> b -> F a --> F b) (fun a => a) (fun (a b : ob C) f => f)). apply (functor_identity_ob_mor C). Defined. (** * Natural transformations *) (** ** Definition of natural transformations *) Definition is_nat_trans {C C' : precategory_data} (F F' : functor_data C C') (t : forall x : ob C, F x --> F' x) := forall (x x' : ob C)(f : x --> x'), #F f ;; t x' == t x ;; #F' f. Lemma isaprop_is_nat_trans (C C' : precategory_data) (F F' : functor_data C C') (t : forall x : ob C, F x --> F' x): isaprop (is_nat_trans F F' t). Proof. repeat (apply impred; intro). apply (pr2 (_ --> _)). Qed. Definition nat_trans {C C' : precategory_data} (F F' : functor_data C C') := total2 ( fun t : forall x : ob C, F x --> F' x => is_nat_trans F F' t). Lemma isaset_nat_trans {C C' : precategory_data} (F F' : functor_data C C') : isaset (nat_trans F F'). Proof. change isaset with (isofhlevel 2). apply isofhleveltotal2. apply impred. intro t. apply (pr2 (_ --> _)). intro x. apply isasetaprop. apply isaprop_is_nat_trans. Qed. Definition nat_trans_data (C C' : precategory_data) (F F' : functor_data C C')(a : nat_trans F F') : forall x : ob C, F x --> F' x := pr1 a. Coercion nat_trans_data : nat_trans >-> Funclass. Definition nat_trans_ax {C C' : precategory_data} (F F' : functor_data C C') (a : nat_trans F F') : forall (x x' : ob C)(f : x --> x'), #F f ;; a x' == a x ;; #F' f := pr2 a. (** Equality between two natural transformations *) Lemma nat_trans_eq {C C' : precategory_data} (F F' : functor_data C C')(a a' : nat_trans F F'): (forall x, a x == a' x) -> a == a'. Proof. intro H. assert (H' : pr1 a == pr1 a'). apply funextsec. assumption. apply (total2_paths H'). apply proofirrelevance. apply isaprop_is_nat_trans. Qed. Definition nat_trans_eq_pointwise (C C' : precategory_data) (F F' : functor_data C C') (a a' : nat_trans F F'): a == a' -> forall x, a x == a' x. Proof. intro h. apply toforallpaths. apply maponpaths. assumption. Qed. (** ** Functor category [[C, D]] *) Definition functor_precategory_ob_mor (C C' : precategory_data): precategory_ob_mor := precategory_ob_mor_pair (functor C C') (fun F F' : functor C C' => hSetpair (nat_trans F F') (isaset_nat_trans F F')). (** *** Identity natural transformation *) Lemma is_nat_trans_id {C C' : precategory} (F : functor_data C C') : is_nat_trans F F (fun c : ob C => identity (F c)). Proof. intros ? ? ? . rewrite id_left. rewrite id_right. apply idpath. Qed. Definition nat_trans_id {C C' : precategory} (F : functor_data C C') : nat_trans F F := tpair _ _ (is_nat_trans_id F). (** *** Composition of natural transformations *) Lemma is_nat_trans_comp {C C' : precategory} {F G H : functor_data C C'} (a : nat_trans F G) (b : nat_trans G H): is_nat_trans F H (fun x : ob C => a x ;; b x). Proof. intros ? ? ? . rewrite assoc. rewrite nat_trans_ax. rewrite <- assoc. rewrite nat_trans_ax. apply assoc. Qed. Definition nat_trans_comp {C C' : precategory} (F G H: functor_data C C') (a : nat_trans F G) (b : nat_trans G H): nat_trans F H := tpair _ _ (is_nat_trans_comp a b). (** *** The data of the functor precategory *) Definition functor_precategory_data (C C' : precategory): precategory_data. Proof. apply ( precategory_data_pair (functor_precategory_ob_mor C C')). intro a. simpl. apply (nat_trans_id (pr1 a)). intros a b c f g. apply (nat_trans_comp _ _ _ f g). Defined. (** *** Above data forms a precategory *) Lemma is_precategory_functor_precategory_data (C C' : precategory) : is_precategory (functor_precategory_data C C'). Proof. repeat split; simpl; intros. unfold identity. simpl. apply nat_trans_eq. intro x; simpl. apply id_left. apply nat_trans_eq. intro x; simpl. apply id_right. apply nat_trans_eq. intro x; simpl. apply assoc. Qed. Definition functor_precategory (C C' : precategory): precategory := tpair _ _ (is_precategory_functor_precategory_data C C'). Notation "[ C , D ]" := (functor_precategory C D). Lemma nat_trans_comp_pointwise (C C' : precategory) (F G H : ob [C, C']) (A : F --> G) (A' : G --> H) (B : F --> H) : A ;; A' == B -> forall a, pr1 A a ;; pr1 A' a == pr1 B a. Proof. intros H' a. pathvia (pr1 (A ;; A') a). apply idpath. destruct H'. apply idpath. Defined. (** Characterizing isomorphisms in the functor category *) Lemma is_nat_trans_inv_from_pointwise_inv (C D : precategory) (F G : ob [C,D]) (A : F --> G) (H : forall a : ob C, is_isomorphism (pr1 A a)) : is_nat_trans _ _ (fun a : ob C => inv_from_iso (tpair _ _ (H a))). Proof. unfold is_nat_trans. intros x x' f. apply pathsinv0. apply iso_inv_on_right. rewrite assoc. apply iso_inv_on_left. set (HA:= pr2 A). simpl in *. unfold is_nat_trans in HA. rewrite HA. apply idpath. Qed. Definition nat_trans_inv_from_pointwise_inv (C D : precategory) (F G : ob [C,D]) (A : F --> G) (H : forall a : ob C, is_isomorphism (pr1 A a)) : G --> F := tpair _ _ (is_nat_trans_inv_from_pointwise_inv _ _ _ _ _ H). Lemma is_inverse_nat_trans_inv_from_pointwise_inv (C C' : precategory) (F G : [C, C']) (A : F --> G) (H : forall a : C, is_isomorphism (pr1 A a)) : is_inverse_in_precat A (nat_trans_inv_from_pointwise_inv C C' F G A H). Proof. simpl; split; simpl. apply nat_trans_eq. intro x; simpl. apply (pr2 (H _)). apply nat_trans_eq. intro x; simpl. apply (pr2 (pr2 (H _))). Qed. Lemma functor_iso_if_pointwise_iso (C C' : precategory) (F G : ob [C, C']) (A : F --> G) : (forall a : ob C, is_isomorphism (pr1 A a)) -> is_isomorphism A . Proof. intro H. exists (nat_trans_inv_from_pointwise_inv _ _ _ _ _ H). simpl; apply is_inverse_nat_trans_inv_from_pointwise_inv. Defined. Definition functor_iso_from_pointwise_iso (C C' : precategory) (F G : ob [C, C']) (A : F --> G) (H : forall a : ob C, is_isomorphism (pr1 A a)) : iso F G := tpair _ _ (functor_iso_if_pointwise_iso _ _ _ _ _ H). Lemma is_functor_iso_pointwise_if_iso (C C' : precategory) (F G : ob [C, C']) (A : F --> G) : is_isomorphism A -> forall a : ob C, is_isomorphism (pr1 A a). Proof. intros H a. simpl in *. set (R := pr1 H). simpl in *. exists (R a). unfold is_inverse_in_precat in *; simpl; split. set (H1' := nat_trans_eq_pointwise _ _ _ _ _ _ (pr1 (pr2 H))). simpl in H1'. apply H1'. apply (nat_trans_eq_pointwise _ _ _ _ _ _ (pr2 (pr2 H))). Defined. Definition functor_iso_pointwise_if_iso (C C' : precategory) (F G : ob [C, C']) (A : F --> G) (H : is_isomorphism A) : forall a : ob C, iso (pr1 F a) (pr1 G a) := fun a => tpair _ _ (is_functor_iso_pointwise_if_iso C C' F G A H a). Definition pr1_pr1_functor_eq_from_functor_iso (C D : precategory) (H : is_category D) (F G : ob [C , D]) : iso F G -> pr1 (pr1 F) == pr1 (pr1 G). Proof. intro A. apply funextsec. intro t. apply isotoid. assumption. apply (functor_iso_pointwise_if_iso _ _ _ _ A). apply (pr2 A). Defined. Lemma transport_of_functor_map_is_pointwise (C D : precategory) (F0 G0 : ob C -> ob D) (F1 : forall a b : ob C, a --> b -> F0 a --> F0 b) (gamma : F0 == G0 ) (a b : ob C) (f : a --> b) : transportf (fun x : ob C -> ob D => forall a0 b0 : ob C, a0 --> b0 -> x a0 --> x b0) gamma F1 a b f == transportf (fun TT : ob D => G0 a --> TT) (toforallpaths (fun _ : ob C => D) F0 G0 gamma b) (transportf (fun SS : ob D => SS --> F0 b) (toforallpaths (fun _ : ob C => D) F0 G0 gamma a) (F1 a b f)). Proof. induction gamma. apply idpath. Defined. Lemma toforallpaths_funextsec : forall (T : UU) (P : T -> UU) (f g : forall t : T, P t) (h : forall t : T, f t == g t), toforallpaths _ _ _ (funextsec _ _ _ h) == h. Proof. intros T P f g h. set (H':= homotweqinvweq (weqtoforallpaths _ f g)). simpl in H'. apply H'. Qed. Definition pr1_functor_eq_from_functor_iso (C D : precategory) (H : is_category D) (F G : ob [C , D]) : iso F G -> pr1 F == pr1 G. Proof. intro A. apply (total2_paths (pr1_pr1_functor_eq_from_functor_iso C D H F G A)). unfold pr1_pr1_functor_eq_from_functor_iso. apply funextsec; intro a. apply funextsec; intro b. apply funextsec; intro f. rewrite transport_of_functor_map_is_pointwise. rewrite toforallpaths_funextsec. pathvia ((inv_from_iso (idtoiso (isotoid D H (functor_iso_pointwise_if_iso C D F G A (pr2 A) a)));; pr2 (pr1 F) a b f);; idtoiso (isotoid D H (functor_iso_pointwise_if_iso C D F G A (pr2 A) b))). set (H':= double_transport_idtoiso D _ _ _ _ (isotoid D H (functor_iso_pointwise_if_iso C D F G A (pr2 A) a)) (isotoid D H (functor_iso_pointwise_if_iso C D F G A (pr2 A) b)) (pr2 (pr1 F) a b f)). unfold double_transport in H'. apply H'; clear H'. rewrite idtoiso_isotoid. rewrite idtoiso_isotoid. destruct A as [A Aiso]. simpl in *. pathvia (inv_from_iso (functor_iso_pointwise_if_iso C D F G A Aiso a) ;; (A a ;; #G f)). rewrite <- assoc. apply maponpaths. apply (nat_trans_ax _ _ A). rewrite assoc. unfold functor_iso_pointwise_if_iso. unfold inv_from_iso. simpl in *. destruct Aiso as [A' AH]. simpl in *. destruct AH as [A1 A2]. rewrite (nat_trans_comp_pointwise _ _ _ _ _ _ _ _ A2). simpl. rewrite id_left. apply idpath. Defined. Definition functor_eq_from_functor_iso {C D : precategory} (H : is_category D) (F G : ob [C , D]) (H' : iso F G) : F == G. Proof. apply (functor_eq _ _ F G). apply pr1_functor_eq_from_functor_iso; assumption. Defined. Lemma idtoiso_compute_pointwise (C D : precategory) (F G : ob [C, D]) (p : F == G) (a : ob C) : functor_iso_pointwise_if_iso C D F G (idtoiso p) (pr2 (idtoiso p)) a == idtoiso (toforallpaths (fun _ : ob C => D) (pr1 (pr1 F)) (pr1 (pr1 G)) (base_paths (pr1 F) (pr1 G) (base_paths F G p)) a). Proof. induction p. apply eq_iso. apply idpath. Qed. Lemma functor_eq_from_functor_iso_idtoiso (C D : precategory) (H : is_category D) (F G : ob [C, D]) (p : F == G) : functor_eq_from_functor_iso H F G (idtoiso p) == p. Proof. simpl; apply functor_eq_eq_from_functor_ob_eq. unfold functor_eq_from_functor_iso. unfold functor_eq. rewrite base_total_path. unfold pr1_functor_eq_from_functor_iso. rewrite base_total_path. unfold pr1_pr1_functor_eq_from_functor_iso. apply (equal_transport_along_weq _ _ (weqtoforallpaths _ _ _ )). simpl. rewrite toforallpaths_funextsec. apply funextsec; intro a. rewrite idtoiso_compute_pointwise. apply isotoid_idtoiso. Qed. Lemma idtoiso_functor_eq_from_functor_iso (C D : precategory) (H : is_category D) (F G : ob [C, D]) (gamma : iso F G) : idtoiso (functor_eq_from_functor_iso H F G gamma) == gamma. Proof. apply eq_iso. simpl; apply nat_trans_eq; intro a. assert (H':= idtoiso_compute_pointwise C D F G (functor_eq_from_functor_iso H F G gamma) a). simpl in *. pathvia (pr1 (idtoiso (toforallpaths (fun _ : ob C => D) (pr1 (pr1 F)) (pr1 (pr1 G)) (base_paths (pr1 F) (pr1 G) (base_paths F G (functor_eq_from_functor_iso H F G gamma))) a))). assert (H2 := maponpaths (@pr1 _ _ ) H'). simpl in H2. apply H2. unfold functor_eq_from_functor_iso. unfold functor_eq. rewrite base_total_path. unfold pr1_functor_eq_from_functor_iso. rewrite base_total_path. pathvia (pr1 (idtoiso (isotoid D H (functor_iso_pointwise_if_iso C D F G gamma (pr2 gamma) a)))). apply maponpaths. apply maponpaths. unfold pr1_pr1_functor_eq_from_functor_iso. rewrite toforallpaths_funextsec. apply idpath. rewrite idtoiso_isotoid. apply idpath. Qed. Lemma isweq_idtoiso_functorcat (C D : precategory) (H : is_category D) (F G : ob [C, D]) : isweq (@idtoiso _ F G). Proof. apply (gradth _ (functor_eq_from_functor_iso H F G)). apply functor_eq_from_functor_iso_idtoiso. apply idtoiso_functor_eq_from_functor_iso. Defined. Lemma is_category_functor_category (C D : precategory) (H : is_category D) : is_category [C, D]. Proof. intros F G. apply isweq_idtoiso_functorcat. apply H. Qed. Ahrens-Coq/._HLevel_n_is_of_hlevel_Sn.v000777 000765 000024 00000000260 12262322302 020703 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/HLevel_n_is_of_hlevel_Sn.v000777 000765 000024 00000014026 12262322302 020473 0ustar00nicolastaff000000 000000 (** * [HLevel(n)] is of hlevel n+1 *) (** Authors: Benedikt Ahrens, Chris Kapulkin Title: HLevel(n) is of hlevel n+1 Date: December 2012 *) (** In this file we prove the main result of this work: the type of types of hlevel n is itself of hlevel n+1. *) Require Import Foundations.hlevel1.hProp. Require Import Foundations.Proof_of_Extensionality.funextfun. Require Import RezkCompletion.auxiliary_lemmas_HoTT. (** As before, we use an infix notation for the path space. *) Require Import RezkCompletion.pathnotations. Import RezkCompletion.pathnotations.PathNotations. (** ** Weak equivalence between identity types in [HLevel] and [U] *) (** To show that HLevel(n) is of hlevel n + 1, we need to show that its path spaces are of hlevel n. First, we show that each of its path spaces equivalent to the path space of the underlying types. More generally, we prove this for any predicate [P : UU -> hProp] which we later instantiate with [P := isofhlevel n]. *) (** Overview of the proof: Identity of Sigmas <~> Sigma of Identities <~> Identities in [U] , where the first equivalence is called [weq1] and the second one is called [weq2]. *) Lemma weq1 (P : UU -> hProp) (X X' : UU) (pX : P X) (pX' : P X') : weq (tpair _ X pX == tpair (fun x => P x) X' pX') (total2 (fun w : X == X' => transportf (fun x => P x) w pX == pX')). Proof. apply total_paths_equiv. Defined. (** This helper lemma is needed to show that our fibration is indeed a predicate, so that we can instantiate the hProposition [P] with this fibration. *) Lemma ident_is_prop : forall (P : UU -> hProp) (X X' : UU) (pX : P X) (pX' : P X') (w : X == X'), isaprop (transportf (fun X => P X) w pX == pX'). Proof. intros P X X' pX pX' w. apply isapropifcontr. apply (pr2 (P X')). Defined. (** We construct the equivalence [weq2] as a projection from a total space, which, by the previous lemma, is a weak equivalence. *) Lemma weq2 (P : UU -> hProp) (X X' : UU) (pX : P X) (pX' : P X') : weq (total2 (fun w : X == X' => transportf (fun x => P x) w pX == pX')) (X == X'). Proof. exists (@pr1 (X == X') (fun w : X == X' => (transportf (fun x : UU => P x) w pX) == pX' )). set (H' := isweqpr1_UU X X' (fun w : X == X' => (transportf (fun X => P X) w pX == pX') )). simpl in H'. apply H'. intro z. apply (pr2 (P X')). Defined. (** Composing [weq1] and [weq2] yields the desired weak equivalence. *) Lemma Id_p_weq_Id (P : UU -> hProp) (X X' : UU) (pX : P X) (pX' : P X') : weq ((tpair _ X pX) == (tpair (fun x => P x) X' pX')) (X == X'). Proof. set (f := weq1 P X X' pX pX'). set (g := weq2 P X X' pX pX'). set (fg := weqcomp f g). exact fg. Defined. (** ** Hlevel of path spaces *) (** We show that if [X] and [X'] are of hlevel [n], then so is their identity type [X == X']. *) (** The proof works differently for [n == 0] and [n == S n'], so we treat these two cases in separate lemmas [isofhlevel0pathspace] and [isofhlevelSnpathspace] and put them together in the lemma [isofhlevelpathspace]. *) (** *** The case [n == 0] *) Lemma isofhlevel0weq (X Y : UU) : iscontr X -> iscontr Y -> weq X Y. Proof. intros pX pY. set (wX := wequnittocontr pX). set (wY := wequnittocontr pY). exact (weqcomp (invweq wX) wY). Defined. Lemma isofhlevel0pathspace (X Y : UU) : iscontr X -> iscontr Y -> iscontr (X == Y). Proof. intros pX pY. set (H := isofhlevelweqb 0 (tpair _ _ (univalenceaxiom X Y))). apply H. exists (isofhlevel0weq _ _ pX pY ). intro f. assert (H' : pr1 f == pr1 (isofhlevel0weq X Y pX pY)). apply funextfun. simpl. intro x. apply (pr2 pY). apply (total2_paths H'). apply proofirrelevance. apply isapropisweq. Defined. (** *** The case [n == S n'] *) Lemma isofhlevelSnpathspace : forall n : nat, forall X Y : UU, isofhlevel (S n) Y -> isofhlevel (S n) (X == Y). Proof. intros n X Y pY. set (H:=isofhlevelweqb (S n) (tpair _ _ (univalenceaxiom X Y))). apply H. assert (H' : isofhlevel (S n) (X -> Y)). apply impred. intro x. assumption. assert (H2 : isincl (@pr1 (X -> Y) (fun f => isweq f))). apply isofhlevelfpr1. intro f. apply isapropisweq. apply (isofhlevelsninclb _ _ H2). assumption. Defined. (** ** The lemma itself *) Lemma isofhlevelpathspace : forall n : nat, forall X Y : UU, isofhlevel n X -> isofhlevel n Y -> isofhlevel n (X == Y). Proof. intros n. case n. intros X Y pX pY. apply isofhlevel0pathspace; assumption. intros. apply isofhlevelSnpathspace; assumption. Defined. (** ** HLevel *) (** We define the type [HLevel n] of types of hlevel n. *) Definition HLevel n := total2 (fun X : UU => isofhlevel n X). (** * Main theorem: [HLevel n] is of hlevel [S n] *) Lemma hlevel_of_hlevels : forall n, isofhlevel (S n) (HLevel n). Proof. intro n. simpl. intros [X pX] [X' pX']. set (H := isofhlevelweqb n (Id_p_weq_Id (fun X => tpair (fun X => isaprop X) (isofhlevel n X) (isapropisofhlevel _ _)) X X' pX pX')). apply H. apply isofhlevelpathspace; assumption. Defined. (** ** Aside: Univalence for predicates and hlevels *) (** As a corollary from [Id_p_weq_Id], we obtain a version of the Univalence Axiom for predicates on the universe [U]. In particular, we can instantiate this predicate with [isofhlevel n]. *) Lemma UA_for_Predicates (P : UU -> hProp) (X X' : UU) (pX : P X) (pX' : P X') : weq ((tpair _ X pX) == (tpair (fun x => P x) X' pX')) (weq X X'). Proof. set (f := Id_p_weq_Id P X X' pX pX'). set (g := tpair _ _ (univalenceaxiom X X')). exact (weqcomp f g). Defined. Corollary UA_for_HLevels : forall (n : nat) (X X' : HLevel n), weq (X == X') (weq (pr1 X) (pr1 X')). Proof. intros n [X pX] [X' pX']. simpl. apply (UA_for_Predicates (fun X => tpair (fun X => isaprop X) (isofhlevel n X) (isapropisofhlevel _ _))). Defined. Ahrens-Coq/._Make000777 000765 000024 00000000260 12262322302 014442 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/Make000777 000765 000024 00000000435 12262322302 014231 0ustar00nicolastaff000000 000000 -o Make.makefile -R . RezkCompletion auxiliary_lemmas_HoTT.v category_hset.v equivalences.v functors_transformations.v HLevel_n_is_of_hlevel_Sn.v pathnotations.v precategories.v precomp_ess_surj.v precomp_fully_faithful.v rezk_completion.v sub_precategories.v whiskering.v yoneda.v Ahrens-Coq/._Make.makefile000777 000765 000024 00000000260 12262322302 016216 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/Make.makefile000777 000765 000024 00000013453 12262322302 016011 0ustar00nicolastaff000000 000000 ############################################################################# ## v # The Coq Proof Assistant ## ## "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) byte: $(MAKE) all "OPT:=-byte" opt: $(MAKE) all "OPT:=-opt" install: mkdir -p $(COQLIB)/user-contrib (for i in $(VOFILES); do \ install -d `dirname $(COQLIB)/user-contrib/RezkCompletion/$$i`; \ install $$i $(COQLIB)/user-contrib/RezkCompletion/$$i; \ done) clean: rm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~ rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d) - rm -rf html archclean: rm -f *.cmx *.o printenv: @echo CAMLC = $(CAMLC) @echo CAMLOPTC = $(CAMLOPTC) @echo CAMLP4LIB = $(CAMLP4LIB) Make.makefile: Make mv -f Make.makefile Make.makefile.bak $(COQBIN)coq_makefile -f Make -o Make.makefile -include $(VFILES:.v=.v.d) .SECONDARY: $(VFILES:.v=.v.d) # WARNING # # This Makefile has been automagically generated # Edit at your own risks ! # # END OF WARNING Ahrens-Coq/._Makefile000777 000765 000024 00000000260 12262322302 015302 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/Makefile000777 000765 000024 00000000561 12262322302 015071 0ustar00nicolastaff000000 000000 # -*- makefile-gmake -*- include Make.makefile COQDEFS := --language=none -r '/^[[:space:]]*\(Axiom\|Theorem\|Class\|Instance\|Let\|Ltac\|Definition\|Lemma\|Record\|Remark\|Structure\|Fixpoint\|Fact\|Corollary\|Let\|Inductive\|Coinductive\|Notation\|Proposition\)[[:space:]]+\([[:alnum:]_]+\)/\2/' TAGS : $(VFILES); etags $(COQDEFS) $^ clean:clean2 clean2:; rm -f TAGS Ahrens-Coq/._pathnotations.v000777 000765 000024 00000000260 12262322302 016724 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/pathnotations.v000777 000765 000024 00000000434 12262322302 016512 0ustar00nicolastaff000000 000000 Require Import Foundations.Generalities.uu0. Module Import PathNotations. Notation "a == b" := (paths a b) (at level 70, no associativity). Notation "! p " := (pathsinv0 p) (at level 50). Notation "p @ q" := (pathscomp0 p q) (at level 60, right associativity). End PathNotations. Ahrens-Coq/._precategories.v000777 000765 000024 00000000260 12262322302 016665 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/precategories.v000777 000765 000024 00000046147 12262322302 016466 0ustar00nicolastaff000000 000000 (** ********************************************************** Benedikt Ahrens, Chris Kapulkin, Mike Shulman january 2013 ************************************************************) (** ********************************************************** Contents : Definition of Precategories, Categories (aka saturated precategories) Setcategories Isomorphisms various lemmas: uniqueness of inverse, composition etc. stability under composition Categories have groupoid as objects ************************************************************) Require Import Foundations.Generalities.uu0. Require Import Foundations.hlevel1.hProp. Require Import Foundations.hlevel2.hSet. Require Import RezkCompletion.auxiliary_lemmas_HoTT. Require Import RezkCompletion.pathnotations. Import RezkCompletion.pathnotations.PathNotations. Ltac pathvia b := (apply (@pathscomp0 _ _ b _ )). (** * Definition of a precategory *) Definition precategory_ob_mor := total2 ( fun ob : UU => ob -> ob -> hSet). Definition precategory_ob_mor_pair (ob : UU)(mor : ob -> ob -> hSet) : precategory_ob_mor := tpair _ ob mor. Definition ob (C : precategory_ob_mor) : Type := @pr1 _ _ C. Coercion ob : precategory_ob_mor >-> Sortclass. Definition precategory_morphisms { C : precategory_ob_mor } : C -> C -> hSet := pr2 C. (** We introduce notation for morphisms *) (** in order for this notation not to pollute subsequent files, we define this notation locally *) Local Notation "a --> b" := (precategory_morphisms a b)(at level 50). (** ** [precategory_data] *) (** data of a precategory : - objects - morphisms - identity morphisms - composition *) Definition precategory_data := total2 ( fun C : precategory_ob_mor => dirprod (forall c : C, c --> c) (* identities *) (forall a b c : C, a --> b -> b --> c -> a --> c)). Definition precategory_data_pair (C : precategory_ob_mor) (id : forall c : C, c --> c) (comp: forall a b c : C, a --> b -> b --> c -> a --> c) : precategory_data := tpair _ C (dirprodpair id comp). Definition precategory_ob_mor_from_precategory_data (C : precategory_data) : precategory_ob_mor := pr1 C. Coercion precategory_ob_mor_from_precategory_data : precategory_data >-> precategory_ob_mor. Definition identity { C : precategory_data } : forall c : C, c --> c := pr1 (pr2 C). Definition compose { C : precategory_data } { a b c : C } : a --> b -> b --> c -> a --> c := pr2 (pr2 C) a b c. Local Notation "f ;; g" := (compose f g)(at level 50). (** ** Axioms of a precategory *) (** - identity is left and right neutral for composition - composition is associative *) Definition is_precategory (C : precategory_data) := dirprod (dirprod (forall (a b : C) (f : a --> b), identity a ;; f == f) (forall (a b : C) (f : a --> b), f ;; identity b == f)) (forall (a b c d : C) (f : a --> b)(g : b --> c) (h : c --> d), f ;; (g ;; h) == (f ;; g) ;; h). Definition precategory := total2 is_precategory. Definition precategory_data_from_precategory (C : precategory) : precategory_data := pr1 C. Coercion precategory_data_from_precategory : precategory >-> precategory_data. Definition id_left (C : precategory) : forall (a b : C) (f : a --> b), identity a ;; f == f := pr1 (pr1 (pr2 C)). Definition id_right (C : precategory) : forall (a b : C) (f : a --> b), f ;; identity b == f := pr2 (pr1 (pr2 C)). Definition assoc (C : precategory) : forall (a b c d : C) (f : a --> b)(g : b --> c) (h : c --> d), f ;; (g ;; h) == (f ;; g) ;; h := pr2 (pr2 C). (** Any equality on objects a and b induces a morphism from a to b *) Definition precategory_eq_morphism (C : precategory_data) (a b : C) (H : a == b) : a --> b. Proof. destruct H. exact (identity a). Defined. Definition precategory_eq_morphism_inv (C : precategory_data) (a b : C) (H : a == b) : b --> a. Proof. destruct H. exact (identity a). Defined. Lemma cancel_postcomposition (C : precategory_data) (a b c: C) (f f' : a --> b) (g : b --> c) : f == f' -> f ;; g == f' ;; g. Proof. intro H. destruct H. apply idpath. Defined. (** * Setcategories: Precategories whose objects form a set *) Definition setcategory := total2 ( fun C : precategory => isaset (ob C)). Definition precategory_from_setcategory (C : setcategory) : precategory := pr1 C. Coercion precategory_from_setcategory : setcategory >-> precategory. Definition setcategory_objects_set (C : setcategory) : hSet := hSetpair (ob C) (pr2 C). Lemma setcategory_eq_morphism_pi (C : setcategory) (a b : ob C) (H H': a == b) : precategory_eq_morphism C a b H == precategory_eq_morphism C a b H'. Proof. assert (h : H == H'). apply uip. apply (pr2 C). apply (maponpaths (precategory_eq_morphism C a b) h). Qed. (** * Isomorphisms in a precategory *) (** ** Definition of isomorphisms *) Definition is_inverse_in_precat {C : precategory} {a b : C} (f : a --> b) (g : b --> a) := dirprod (f ;; g == identity a) (g ;; f == identity b). Lemma isaprop_is_inverse_in_precat (C : precategory) (a b : ob C) (f : a --> b) (g : b --> a) : isaprop (is_inverse_in_precat f g). Proof. apply isapropdirprod. apply (pr2 (a --> a)). apply (pr2 (b --> b)). Qed. Lemma inverse_unique_precat (C : precategory) (a b : ob C) (f : a --> b) (g g': b --> a) (H : is_inverse_in_precat f g) (H' : is_inverse_in_precat f g') : g == g'. Proof. destruct H as [eta eps]. destruct H' as [eta' eps']. assert (H : g == identity b ;; g). rewrite id_left; apply idpath. apply (pathscomp0 H). rewrite <- eps'. rewrite <- assoc. rewrite eta. apply id_right. Qed. Definition is_isomorphism {C : precategory} {a b : ob C} (f : a --> b) := total2 (fun g => is_inverse_in_precat f g). Lemma isaprop_is_isomorphism {C : precategory} {a b : ob C} (f : a --> b) : isaprop (is_isomorphism f). Proof. apply invproofirrelevance. intros g g'. set (Hpr1 := inverse_unique_precat _ _ _ _ _ _ (pr2 g) (pr2 g')). apply (total2_paths Hpr1). destruct g as [g [eta eps]]. destruct g' as [g' [eta' eps']]. simpl in *. apply pairofobuip. Qed. Definition iso {C : precategory} (a b :ob C) := total2 (fun f : a --> b => is_isomorphism f). Lemma eq_iso (C : precategory)(a b : ob C) (f g : iso a b) : pr1 f == pr1 g -> f == g. Proof. intro H. apply (total2_paths H). apply proofirrelevance. apply isaprop_is_isomorphism. Defined. Definition morphism_from_iso (C : precategory)(a b : ob C) (f : iso a b) : a --> b := pr1 f. Coercion morphism_from_iso : iso >-> pr1hSet. Lemma isaset_iso {C : precategory} (a b :ob C) : isaset (iso a b). Proof. change isaset with (isofhlevel 2). apply isofhleveltotal2. apply (pr2 (a --> b)). intro f. apply isasetaprop. apply isaprop_is_isomorphism. Qed. Lemma identity_is_iso (C : precategory) (a : ob C) : is_isomorphism (identity a). Proof. exists (identity a). simpl; split; apply id_left. Defined. Definition identity_iso {C : precategory} (a : ob C) : iso a a := tpair _ _ (identity_is_iso C a). Definition inv_from_iso {C : precategory} {a b : ob C} (f : iso a b) : b --> a := pr1 (pr2 f). Lemma is_iso_inv_from_iso {C : precategory} (a b : ob C) (f : iso a b) : is_isomorphism (inv_from_iso f). Proof. exists (pr1 f). simpl; split; simpl. unfold inv_from_iso. apply (pr2 (pr2 (pr2 f))). apply (pr1 (pr2 (pr2 f))). Defined. Definition iso_inv_from_iso {C : precategory} {a b : ob C} (f : iso a b) : iso b a. Proof. exists (inv_from_iso f). apply is_iso_inv_from_iso. Defined. Definition iso_inv_after_iso (C : precategory) (a b : ob C) (f : iso a b) : f;; inv_from_iso f == identity _ := pr1 (pr2 (pr2 f)). Definition iso_after_iso_inv (C : precategory) (a b : ob C) (f : iso a b) : inv_from_iso f ;; f == identity _ := pr2 (pr2 (pr2 f)). Lemma iso_inv_on_right (C : precategory) (a b c: ob C) (f : iso a b) (g : b --> c) (h : a --> c) (H : h == f;;g) : inv_from_iso f ;; h == g. Proof. assert (H2 : inv_from_iso f;; h == inv_from_iso f;; (f ;; g)). apply maponpaths; assumption. rewrite assoc in H2. rewrite H2. rewrite iso_after_iso_inv. apply id_left. Qed. Lemma iso_inv_on_left (C : precategory) (a b c: ob C) (f : a --> b) (g : iso b c) (h : a --> c) (H : h == f;;g) : f == h ;; inv_from_iso g. Proof. assert (H2 : h ;; inv_from_iso g == (f;; g) ;; inv_from_iso g). rewrite H. apply idpath. rewrite <- assoc in H2. rewrite iso_inv_after_iso in H2. rewrite id_right in H2. apply pathsinv0. assumption. Qed. (** ** Properties of isomorphisms *) (** Stability under composition, inverses etc *) Lemma are_inverse_comp_of_inverses (C : precategory) (a b c : C) (f : iso a b) (g : iso b c) : is_inverse_in_precat (f;; g) (inv_from_iso g;; inv_from_iso f). Proof. simpl; split; simpl; unfold inv_from_iso; simpl. destruct f as [f [f' Hf]]. simpl in *. destruct g as [g [g' Hg]]; simpl in *. pathvia ((f ;; (g ;; g')) ;; f'). repeat rewrite assoc; apply idpath. rewrite (pr1 Hg). rewrite id_right. rewrite (pr1 Hf). apply idpath. destruct f as [f [f' Hf]]. simpl in *. destruct g as [g [g' Hg]]; simpl in *. pathvia ((g' ;; (f' ;; f)) ;; g). repeat rewrite assoc; apply idpath. rewrite (pr2 Hf). rewrite id_right. rewrite (pr2 Hg). apply idpath. Qed. Lemma is_iso_comp_of_isos {C : precategory} {a b c : ob C} (f : iso a b) (g : iso b c) : is_isomorphism (f ;; g). Proof. exists (inv_from_iso g ;; inv_from_iso f). simpl. apply are_inverse_comp_of_inverses. Defined. (* Qed. *) Definition iso_comp {C : precategory} {a b c : ob C} (f : iso a b) (g : iso b c) : iso a c. Proof. exists (f ;; g). apply is_iso_comp_of_isos. Defined. Lemma inv_iso_unique (C : precategory) (a b : ob C) (f : iso a b) (g : iso b a) : is_inverse_in_precat f g -> g == iso_inv_from_iso f. Proof. intro H. apply eq_iso. apply (inverse_unique_precat _ _ _ f). assumption. split. apply iso_inv_after_iso. set (h := iso_after_iso_inv _ _ _ f). unfold iso_inv_from_iso. simpl in *. apply h. Qed. Lemma iso_inv_of_iso_comp (C : precategory) (a b c : ob C) (f : iso a b) (g : iso b c) : iso_inv_from_iso (iso_comp f g) == iso_comp (iso_inv_from_iso g) (iso_inv_from_iso f). Proof. apply eq_iso. reflexivity. Qed. Lemma iso_inv_of_iso_id (C : precategory) (a : ob C) : iso_inv_from_iso (identity_iso a) == identity_iso a. Proof. apply eq_iso. apply idpath. Qed. Lemma iso_inv_iso_inv (C : precategory) (a b : ob C) (f : iso a b) : iso_inv_from_iso (iso_inv_from_iso f) == f. Proof. apply eq_iso. reflexivity. Defined. Lemma pre_comp_with_iso_is_inj (C : precategory) (a b c : ob C) (f : a --> b) (H : is_isomorphism f) (g h : b --> c) : f ;; g == f ;; h -> g == h. Proof. intro HH. pathvia (pr1 H ;; f ;; g). rewrite (pr2 (pr2 H)). rewrite id_left. apply idpath. pathvia ((pr1 H ;; f) ;; h). repeat rewrite <- assoc. apply maponpaths. assumption. rewrite (pr2 (pr2 H)). rewrite id_left. apply idpath. Qed. Lemma post_comp_with_iso_is_inj (C : precategory) (b c : ob C) (h : b --> c) (H : is_isomorphism h) (a : ob C) (f g : a --> b) : f ;; h == g ;; h -> f == g. Proof. intro HH. pathvia (f ;; (h ;; pr1 H)). rewrite (pr1 (pr2 H)). rewrite id_right. apply idpath. pathvia (g ;; (h ;; pr1 H)). repeat rewrite assoc. rewrite HH. apply idpath. rewrite (pr1 (pr2 H)). rewrite id_right. apply idpath. Qed. (** * Categories (aka saturated precategories) *) (** ** Definition of categories *) Definition idtoiso {C : precategory} {a b : ob C}: a == b -> iso a b. Proof. intro H. destruct H. exact (identity_iso a). Defined. (* use eta expanded version to force printing of object arguments *) Definition is_category (C : precategory) := forall (a b : ob C), isweq (fun p : a == b => idtoiso p). Lemma isaprop_is_category (C : precategory) : isaprop (is_category C). Proof. apply impred. intro a. apply impred. intro b. apply isapropisweq. Qed. Definition category := total2 (fun C : precategory => is_category C). Definition precat_from_cat (C : category) : precategory := pr1 C. Coercion precat_from_cat : category >-> precategory. Lemma category_has_groupoid_ob (C : category) : isofhlevel 3 (ob C). Proof. change (isofhlevel 3 C) with (forall a b : C, isofhlevel 2 (a == b)). intros a b. apply (isofhlevelweqb _ (tpair _ _ (pr2 C a b))). apply isaset_iso. Qed. (** ** Definition of [isotoid] *) Definition isotoid (C : precategory) (H : is_category C) {a b : ob C}: iso a b -> a == b := invmap (weqpair _ (H a b)). Lemma idtoiso_isotoid (C : precategory) (H : is_category C) (a b : ob C) (f : iso a b) : idtoiso (isotoid _ H f) == f. Proof. unfold isotoid. set (Hw := homotweqinvweq (weqpair idtoiso (H a b))). simpl in Hw. apply Hw. Qed. Lemma isotoid_idtoiso (C : precategory) (H : is_category C) (a b : ob C) (p : a == b) : isotoid _ H (idtoiso p) == p. Proof. unfold isotoid. set (Hw := homotinvweqweq (weqpair idtoiso (H a b))). simpl in Hw. apply Hw. Qed. (** ** Properties of [idtoiso] and [isotoid] *) Definition double_transport {C : precategory} {a a' b b' : ob C} (p : a == a') (q : b == b') (f : a --> b) : a' --> b' := transportf (fun c => a' --> c) q (transportf (fun c => c --> b) p f). Lemma idtoiso_postcompose (C : precategory) (a b b' : ob C) (p : b == b') (f : a --> b) : f ;; idtoiso p == transportf (fun b => a --> b) p f. Proof. destruct p. apply id_right. Qed. Lemma idtoiso_postcompose_iso (C : precategory) (a b b' : ob C) (p : b == b') (f : iso a b) : iso_comp f (idtoiso p) == transportf (fun b => iso a b) p f. Proof. destruct p. apply eq_iso. simpl. apply id_right. Qed. Lemma idtoiso_precompose (C : precategory) (a a' b : ob C) (p : a == a') (f : a --> b) : (idtoiso (!p)) ;; f == transportf (fun a => a --> b) p f. Proof. destruct p. apply id_left. Qed. Lemma idtoiso_precompose_iso (C : precategory) (a a' b : ob C) (p : a == a') (f : iso a b) : iso_comp (idtoiso (!p)) f == transportf (fun a => iso a b) p f. Proof. destruct p. apply eq_iso. simpl. apply id_left. Qed. Lemma double_transport_idtoiso (C : precategory) (a a' b b' : ob C) (p : a == a') (q : b == b') (f : a --> b) : double_transport p q f == inv_from_iso (idtoiso p) ;; f ;; idtoiso q. Proof. destruct p. destruct q. rewrite id_right. rewrite id_left. apply idpath. Qed. Lemma idtoiso_inv (C : precategory) (a a' : ob C) (p : a == a') : idtoiso (!p) == iso_inv_from_iso (idtoiso p). Proof. destruct p. apply idpath. Qed. Lemma idtoiso_concat (C : precategory) (a a' a'' : ob C) (p : a == a') (q : a' == a'') : idtoiso (p @ q) == iso_comp (idtoiso p) (idtoiso q). Proof. destruct p. destruct q. apply eq_iso. simpl; rewrite id_left. apply idpath. Qed. Lemma idtoiso_inj (C : precategory) (H : is_category C) (a a' : ob C) (p p' : a == a') : idtoiso p == idtoiso p' -> p == p'. Proof. apply invmaponpathsincl. apply isinclweq. apply H. Qed. Lemma isotoid_inj (C : precategory) (H : is_category C) (a a' : ob C) (f f' : iso a a') : isotoid _ H f == isotoid _ H f' -> f == f'. Proof. apply invmaponpathsincl. apply isinclweq. apply isweqinvmap. Qed. Lemma isotoid_comp (C : precategory) (H : is_category C) (a b c : ob C) (e : iso a b) (f : iso b c) : isotoid _ H (iso_comp e f) == isotoid _ H e @ isotoid _ H f. Proof. apply idtoiso_inj. assumption. rewrite idtoiso_concat. repeat rewrite idtoiso_isotoid. apply idpath. Qed. Lemma isotoid_identity_iso (C : precategory) (H : is_category C) (a : C) : isotoid _ H (identity_iso a) == idpath _ . Proof. apply idtoiso_inj; try assumption. rewrite idtoiso_isotoid; apply idpath. Qed. Lemma inv_isotoid (C : precategory) (H : is_category C) (a b : C) (f : iso a b) : ! isotoid _ H f == isotoid _ H (iso_inv_from_iso f). Proof. apply idtoiso_inj; try assumption. rewrite idtoiso_isotoid. rewrite idtoiso_inv. rewrite idtoiso_isotoid. apply idpath. Qed. Lemma transportf_isotoid (C : precategory) (H : is_category C) (a a' b : ob C) (p : iso a a') (f : a --> b) : transportf (fun a0 : C => a0 --> b) (isotoid C H p) f == inv_from_iso p ;; f. Proof. rewrite <- idtoiso_precompose. rewrite idtoiso_inv. rewrite idtoiso_isotoid. apply idpath. Qed. Lemma transportf_isotoid_dep (C : precategory) (a a' : C) (p : a == a') (f : forall c, a --> c) : transportf (fun x : C => forall c, x --> c) p f == fun c => idtoiso (!p) ;; f c. Proof. destruct p. simpl. apply funextsec. intro. rewrite id_left. apply idpath. Qed. Lemma transportf_isotoid_dep' (J C : precategory) (F : J -> C) (a a' : C) (p : a == a') (f : forall c, a --> F c) : transportf (fun x : C => forall c, x --> F c) p f == fun c => idtoiso (!p) ;; f c. Proof. destruct p. apply funextsec. intro. simpl. apply (! id_left _ _ _ _). Defined. (** ** Precategories in style of essentially algebraic cats *) (** Of course we later want SETS of objects, rather than types, but the construction can already be specified. *) Definition total_morphisms (C : precategory_ob_mor) := total2 ( fun ab : dirprod (ob C)(ob C) => precategory_morphisms (pr1 ab) (pr2 ab)). Lemma isaset_setcategory_total_morphisms (C : setcategory) : isaset (total_morphisms C). Proof. change isaset with (isofhlevel 2). apply isofhleveltotal2. apply isofhleveldirprod. exact (pr2 C). exact (pr2 C). exact (fun x => (pr2 (pr1 x --> pr2 x))). Qed. Definition setcategory_total_morphisms_set (C : setcategory) : hSet := hSetpair _ (isaset_setcategory_total_morphisms C). Definition precategory_source (C : precategory_ob_mor) : total_morphisms C -> ob C := fun abf => pr1 (pr1 abf). Definition precategory_target (C : precategory_ob_mor) : total_morphisms C -> ob C := fun abf => pr2 (pr1 abf). Definition precategory_total_id (C : precategory_data) : ob C -> total_morphisms C := fun c => tpair _ (dirprodpair c c) (identity c). Definition precategory_total_comp'' (C : precategory_data) : forall f g : total_morphisms C, precategory_target C f == precategory_source C g -> total_morphisms C. Proof. intros f g H. destruct f as [[a b] f]. simpl in *. destruct g as [[b' c] g]. simpl in *. unfold precategory_target in H; simpl in H. unfold precategory_source in H; simpl in H. simpl. exists (dirprodpair a c). simpl. exact ((f ;; precategory_eq_morphism C b b' H) ;; g). Defined. Definition precategory_total_comp (C : precategory_data) : forall f g : total_morphisms C, precategory_target C f == precategory_source C g -> total_morphisms C := fun f g H => tpair _ (dirprodpair (pr1 (pr1 f))(pr2 (pr1 g))) ((pr2 f ;; precategory_eq_morphism _ _ _ H) ;; pr2 g). Ahrens-Coq/._precomp_ess_surj.v000777 000765 000024 00000000260 12262322302 017413 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/precomp_ess_surj.v000777 000765 000024 00000067331 12262322302 017212 0ustar00nicolastaff000000 000000 (** ********************************************************** Benedikt Ahrens, Chris Kapulkin, Mike Shulman january 2013 ************************************************************) (** ********************************************************** Contents : Precomposition with a fully faithful and essentially surjective functor yields an essentially surjective functor ************************************************************) Require Import Foundations.Generalities.uu0. Require Import Foundations.hlevel1.hProp. Require Import Foundations.hlevel2.hSet. Require Import RezkCompletion.pathnotations. Import RezkCompletion.pathnotations.PathNotations. Require Import RezkCompletion.auxiliary_lemmas_HoTT. Require Import RezkCompletion.precategories. Require Import RezkCompletion.functors_transformations. Require Import RezkCompletion.whiskering. Ltac pathvia b := (apply (@pathscomp0 _ _ b _ )). Local Notation "a --> b" := (precategory_morphisms a b)(at level 50). (*Local Notation "'hom' C" := (precategory_morphisms (C := C)) (at level 2).*) Local Notation "f ;; g" := (compose f g)(at level 50). Notation "[ C , D ]" := (functor_precategory C D). Local Notation "# F" := (functor_on_morphisms F)(at level 3). Local Notation "FF ^-1" := (fully_faithful_inv_hom FF _ _ ) (at level 20). Local Notation "F '^-i'" := (iso_from_fully_faithful_reflection F _ _) (at level 20). Local Notation "G 'O' F" := (functor_compose _ _ _ F G) (at level 25). Ltac simp_rew lem := let H:=fresh in assert (H:= lem); simpl in *; rewrite H; clear H. Ltac simp_rerew lem := let H:=fresh in assert (H:= lem); simpl in *; rewrite <- H; clear H. Ltac inv_functor HF x y := let H:=fresh in set (H:= homotweqinvweq (weq_from_fully_faithful HF x y)); simpl in H; unfold fully_faithful_inv_hom; simpl; rewrite H; clear H. (** * Lengthy preparation for the main result of this file *) Section precomp_w_ess_surj_ff_is_ess_surj. (** ** Section variables *) Variables A B C : precategory. Hypothesis Ccat : is_category C. Variable H : functor A B. Hypothesis p : essentially_surjective H. Hypothesis fH : fully_faithful H. (** We prove that precomposition with a [H] yields an essentially surjective functor *) Section essentially_surjective. (** ** Specification of preimage [G] of a functor [F] *) (** Given a functor [F] from [A] to [C], we construct [G] such that [F == G O H] *) Variable F : functor A C. Section preimage. (** The type [X b] will be contractible, and [G] is defined as the first component of its center. *) Let X (b : B) := total2 ( fun ck : total2 (fun c : C => forall a : A, iso (H a) b -> iso (F a) c) => forall t t' : total2 (fun a : A => iso (H a) b), forall f : pr1 t --> pr1 t', (#H f ;; pr2 t' == pr2 t -> #F f ;; pr2 ck (pr1 t') (pr2 t') == pr2 ck (pr1 t) (pr2 t))). Definition kX {b : B} (t : X b) := (pr2 (pr1 t)). (** The following is the third component of the center of [X b] *) Lemma X_aux_type_center_of_contr_proof (b : B) (anot : A) (hnot : iso (H anot) b) : forall (t t' : total2 (fun a : A => iso (H a) b)) (f : pr1 t --> pr1 t'), #H f;; pr2 t' == pr2 t -> #F f;; #F (fH^-1 (pr2 t';; inv_from_iso hnot)) == #F (fH^-1 (pr2 t;; inv_from_iso hnot)). Proof. intros t t' f. destruct t as [a h]. destruct t' as [a' h']. simpl in *. intro star. rewrite <- (functor_comp _ _ F). apply maponpaths. apply (equal_transport_along_weq _ _ (weq_from_fully_faithful fH a anot)). simpl. rewrite functor_comp. inv_functor fH a' anot. rewrite assoc. inv_functor fH a anot. rewrite <- star. apply idpath. Qed. (** The center of [X b] *) Definition X_aux_type_center_of_contr (b : B) (anot : A)(hnot : iso (H anot) b) : X b. Proof. set (cnot := F anot). set (g := fun (a : A)(h : iso (H a) b) => (fH^-i (iso_comp h (iso_inv_from_iso hnot)))). set (knot := fun (a : A)(h : iso (H a) b) => functor_on_iso _ _ F _ _ (g a h)). simpl in *. exists (tpair _ (F anot) knot). simpl. apply X_aux_type_center_of_contr_proof. Defined. (** Any inhabitant of [X b] is equal to the center of [X b]. *) Lemma X_aux_type_contr_eq (b : B) (anot : A) (hnot : iso (H anot) b) : forall t : X b, t == X_aux_type_center_of_contr b anot hnot. Proof. intro t. simpl in X. assert (Hpr1 : pr1 (X_aux_type_center_of_contr b anot hnot) == pr1 t). set (w := isotoid _ Ccat ((pr2 (pr1 t)) anot hnot) : pr1 (pr1 (X_aux_type_center_of_contr b anot hnot)) == pr1 (pr1 t)). apply (total2_paths w). simpl. destruct t as [[c1 k1] q1]. simpl in *. apply funextsec; intro a. apply funextsec; intro h. set (gah := fH^-i (iso_comp h (iso_inv_from_iso hnot))). set (qhelp := q1 (tpair _ a h)(tpair _ anot hnot) gah). simpl in *. assert (feedtoqhelp : #H (fH^-1 (h;; inv_from_iso hnot));; hnot == h). inv_functor fH a anot. rewrite <- assoc. rewrite iso_after_iso_inv. apply id_right. assert (quack := qhelp feedtoqhelp). simpl in *. pathvia (iso_comp (functor_on_iso A C F a anot (fH^-i (iso_comp h (iso_inv_from_iso hnot)))) (idtoiso w) ). generalize w; intro w0. induction w0. simpl. apply eq_iso. simpl. rewrite id_right. apply idpath. apply eq_iso. simpl. unfold w. rewrite idtoiso_isotoid. apply quack. apply pathsinv0. apply (total2_paths Hpr1). apply proofirrelevance. repeat (apply impred; intro). apply (pr2 (_ --> _)). Qed. (** Putting everything together: [X b] is contractible. *) Definition iscontr_X : forall b : B, iscontr (X b). Proof. intro b. assert (HH : isaprop (iscontr (X b))). apply isapropiscontr. apply (p b (tpair (fun x => isaprop x) (iscontr (X b)) HH)). intro t. exists (X_aux_type_center_of_contr b (pr1 t) (pr2 t)). apply (X_aux_type_contr_eq b (pr1 t) (pr2 t)). Qed. (** The object part of [G], [Go b], is defined as the first component of the center of [X b]. *) (** *** [G] on objects *) Definition Go : B -> C := fun b : B => pr1 (pr1 (pr1 (iscontr_X b))). Let k (b : B) : forall a : A, iso (H a) b -> iso (F a) (Go b) := pr2 (pr1 (pr1 (iscontr_X b))). Let q (b : B) := pr2 (pr1 (iscontr_X b)). (** Given any inhabitant of [X b], its first component is equal to [Go b]. *) Definition Xphi (b : B) (t : X b) : pr1 (pr1 t) == Go b. Proof. set (p1 := pr2 (iscontr_X b) t). exact (base_paths _ _ (base_paths _ _ p1)). Defined. (** Given any inhabitant [t : X b], its second component is equal to [k b], modulo transport along [Xphi b t]. *) Definition Xkphi_transp (b : B) (t : X b) : forall a : A, forall h : iso (H a) b, transportf _ (Xphi b t) (kX t) a h == k b a h. Proof. unfold k. rewrite <- (fiber_path (base_paths _ _ (pr2 (iscontr_X b) t))). intros ? ?. apply maponpaths, idpath. Qed. (** Similarly to the lemma before, the second component of [t] is the same as [k b], modulo postcomposition with an isomorphism. *) Definition Xkphi_idtoiso (b : B) (t : X b) : forall a : A, forall h : iso (H a) b, k b a h ;; idtoiso (!Xphi b t) == kX t a h. Proof. intros a h. rewrite <- (Xkphi_transp _ t). generalize (Xphi b t). intro i; destruct i. apply id_right. Qed. (* Lemma k_transport (b : ob B) (*t : X b*) (c : ob C) (p : pr1 (pr1 t) == c) (a : ob A) (h : iso (pr1 H a) b): transportf (fun c' : ob C => forall a : ob A, iso (pr1 H a) b -> iso ((pr1 F) a) c') p (k) a h == (k b) b a h ;; idtoiso p . *) (** *** Preparation for [G] on morphisms *) (** [G f] will be defined as the first component of the center of contraction of [Y f]. *) Let Y {b b' : B} (f : b --> b') := total2 (fun g : Go b --> Go b' => forall a : A, forall h : iso (H a) b, forall a' : A, forall h' : iso (H a') b', forall l : a --> a', #H l ;; h' == h ;; f -> #F l ;; k b' a' h' == k b a h ;; g). Lemma Y_inhab_proof (b b' : B) (f : b --> b') (a0 : A) (h0 : iso (H a0) b) (a0' : A) (h0' : iso (H a0') b') : forall (a : A) (h : iso (H a) b) (a' : A) (h' : iso (H a') b') (l : a --> a'), #H l;; h' == h;; f -> #F l;; k b' a' h' == k b a h;; ((inv_from_iso (k b a0 h0);; #F (fH^-1 ((h0;; f);; inv_from_iso h0')));; k b' a0' h0'). Proof. intros a h a' h' l alpha. set (m := fH^-i (iso_comp h0 (iso_inv_from_iso h))). set (m' := fH^-i (iso_comp h0' (iso_inv_from_iso h'))). assert (sss : iso_comp (functor_on_iso _ _ F _ _ m) (k b a h) == k b a0 h0). apply eq_iso. apply (q b (tpair _ a0 h0) (tpair _ a h) m). simpl. inv_functor fH a0 a. rewrite <- assoc. rewrite iso_after_iso_inv. apply id_right. assert (ssss : iso_comp (functor_on_iso _ _ F _ _ m') (k b' a' h') == k b' a0' h0'). apply eq_iso. apply (q b' (tpair _ a0' h0') (tpair _ a' h') m'). simpl; inv_functor fH a0' a'. rewrite <- assoc. rewrite iso_after_iso_inv. apply id_right. set (hfh := h0 ;; f ;; inv_from_iso h0'). set (l0 := fH^-1 hfh). set (g0 := inv_from_iso (k b a0 h0) ;; #F l0 ;; k b' a0' h0'). assert (sssss : #H (l0 ;; m') == #H (m ;; l)). rewrite (functor_comp _ _ H). unfold m'. simpl. inv_functor fH a0' a'. unfold l0. inv_functor fH a0 a0'. unfold hfh. pathvia (h0 ;; f ;; (inv_from_iso h0' ;; h0') ;; inv_from_iso h'). repeat rewrite assoc; apply idpath. rewrite iso_after_iso_inv, id_right, (functor_comp _ _ H). inv_functor fH a0 a. repeat rewrite <- assoc. apply maponpaths, pathsinv0, iso_inv_on_right. rewrite assoc. apply iso_inv_on_left, pathsinv0, alpha. assert (star5 : inv_from_iso m ;; l0 == l ;; inv_from_iso m'). apply iso_inv_on_right. rewrite assoc. apply iso_inv_on_left, (equal_transport_along_weq _ _ (weq_from_fully_faithful fH a0 a' )), pathsinv0, sssss. clear sssss. unfold g0. assert (sss'' : k b a h ;; inv_from_iso (k b a0 h0) == inv_from_iso (functor_on_iso _ _ F _ _ m)). apply pathsinv0, iso_inv_on_left, pathsinv0. apply iso_inv_on_right. unfold m; simpl. apply pathsinv0, (base_paths _ _ sss). repeat rewrite assoc. rewrite sss''. clear sss'' sss. rewrite <- functor_on_inv_from_iso. rewrite <- (functor_comp _ _ F). rewrite star5; clear star5 . rewrite functor_comp, functor_on_inv_from_iso. assert (star4 : inv_from_iso (functor_on_iso A C F a0' a' m');; k b' a0' h0' == k b' a' h' ). apply iso_inv_on_right. apply pathsinv0, (base_paths _ _ ssss). rewrite <- assoc. rewrite star4. apply idpath. Qed. (** The center of [Y b b' f]. *) Definition Y_inhab (b b' : B) (f : b --> b') (a0 : A) (h0 : iso (H a0) b) (a0' : A) (h0' : iso (H a0') b') : Y b b' f. Proof. set (hfh := h0 ;; f ;; inv_from_iso h0'). set (l0 := fH^-1 hfh). set (g0 := inv_from_iso (k b a0 h0) ;; #F l0 ;; k b' a0' h0'). exists g0. apply Y_inhab_proof. Defined. (** Any inhabitant of [Y b b' f] is equal to the center. *) Lemma Y_contr_eq (b b' : B) (f : b --> b') (a0 : A) (h0 : iso (H a0) b) (a0' : A) (h0' : iso (H a0') b') : forall t : Y b b' f, t == Y_inhab b b' f a0 h0 a0' h0'. Proof. intro t. apply pathsinv0. assert (Hpr : pr1 (Y_inhab b b' f a0 h0 a0' h0') == pr1 t). destruct t as [g1 r1]; simpl in *. rewrite <- assoc. apply iso_inv_on_right. set (hfh := h0 ;; f ;; inv_from_iso h0'). set (l0 := fH^-1 hfh). apply (r1 a0 h0 a0' h0' l0). unfold l0. inv_functor fH a0 a0' . unfold hfh. repeat rewrite <- assoc. rewrite iso_after_iso_inv, id_right. apply idpath. apply (total2_paths Hpr). apply proofirrelevance. repeat (apply impred; intro). apply (pr2 (_ --> _)). Qed. (** The type [Y b b' f] is contractible. *) Definition Y_iscontr (b b' : B) (f : b --> b') : iscontr (Y b b' f). Proof. assert (HH : isaprop (iscontr (Y b b' f))). apply isapropiscontr. apply (p b (tpair (fun x => isaprop x) (iscontr (Y b b' f)) HH)). intros [a0 h0]. apply (p b' (tpair (fun x => isaprop x) (iscontr (Y b b' f)) HH)). intros [a0' h0']. exists (Y_inhab b b' f a0 h0 a0' h0'). apply Y_contr_eq. Qed. (** *** [G] on morphisms *) (** We now have the data necessary to define the functor [G]. *) Definition preimage_functor_data : functor_data B C. Proof. exists Go. intros b b' f. exact (pr1 (pr1 (Y_iscontr b b' f))). Defined. Notation "'G' f" := (pr1 (pr1 (Y_iscontr _ _ f))) (at level 3). (** The above data is indeed functorial. *) Lemma is_functor_preimage_functor_data : is_functor preimage_functor_data. Proof. split; simpl. intro b. assert (PR2 : forall (a : A) (h : iso (H a) b) (a' : A) (h' : iso (H a') b) (l : a --> a'), #H l;; h' == h;; identity b -> #F l;; k b a' h' == k b a h;; identity (Go b)). intros a h a' h' l LL. rewrite id_right. apply (q b (tpair _ a h) (tpair _ a' h') l). rewrite id_right in LL. apply LL. set (Gbrtilde := tpair _ (identity (Go b)) PR2 : Y b b (identity b)). set (H' := pr2 (Y_iscontr b b (identity b)) Gbrtilde). set (H'' := base_paths _ _ H'). simpl in H'. rewrite <- H'. apply idpath. (** composition *) intros b b' b'' f f'. assert (HHHH : isaprop (pr1 (pr1 (Y_iscontr b b'' (f;; f'))) == pr1 (pr1 (Y_iscontr b b' f));; pr1 (pr1 (Y_iscontr b' b'' f')))). apply (pr2 (Go b --> Go b'')). apply (p b (tpair (fun x => isaprop x) (pr1 (pr1 (Y_iscontr b b'' (f;; f'))) == pr1 (pr1 (Y_iscontr b b' f));; pr1 (pr1 (Y_iscontr b' b'' f'))) HHHH)). intros [a0 h0]; simpl. apply (p b' (tpair (fun x => isaprop x) (pr1 (pr1 (Y_iscontr b b'' (f;; f'))) == pr1 (pr1 (Y_iscontr b b' f));; pr1 (pr1 (Y_iscontr b' b'' f'))) HHHH)). intros [a0' h0']; simpl. apply (p b'' (tpair (fun x => isaprop x) (pr1 (pr1 (Y_iscontr b b'' (f;; f'))) == pr1 (pr1 (Y_iscontr b b' f));; pr1 (pr1 (Y_iscontr b' b'' f'))) HHHH)). intros [a0'' h0'']. simpl; clear HHHH. set (l0 := fH^-1 (h0 ;; f ;; inv_from_iso h0')). set (l0' := fH^-1 (h0' ;; f' ;; inv_from_iso h0'')). set (l0'' := fH^-1 (h0 ;; (f;; f') ;; inv_from_iso h0'')). assert (L : l0 ;; l0' == l0''). apply (equal_transport_along_weq _ _ (weq_from_fully_faithful fH a0 a0'')). simpl; rewrite functor_comp. unfold l0'. inv_functor fH a0' a0''. unfold l0. inv_functor fH a0 a0'. pathvia (h0 ;; f ;; (inv_from_iso h0' ;; h0') ;; f' ;; inv_from_iso h0''). repeat rewrite assoc; apply idpath. rewrite iso_after_iso_inv, id_right. unfold l0''. inv_functor fH a0 a0''. repeat rewrite assoc; apply idpath. assert (PR2 : forall (a : A) (h : iso (H a) b)(a' : A) (h' : iso (H a') b') (l : a --> a'), #H l;; h' == h;; f -> #F l;; k b' a' h' == k b a h;; ((inv_from_iso (k b a0 h0);; #F l0);; k b' a0' h0') ). intros a h a' h' l. intro alpha. set (m := fH^-i (iso_comp h0 (iso_inv_from_iso h))). set (m' := fH^-i (iso_comp h0' (iso_inv_from_iso h'))). assert (sss : iso_comp (functor_on_iso _ _ F _ _ m) (k b a h) == k b a0 h0). apply eq_iso; simpl. apply (q b (tpair _ a0 h0) (tpair _ a h) m). simpl. inv_functor fH a0 a. rewrite <- assoc. rewrite iso_after_iso_inv. apply id_right. assert (ssss : iso_comp (functor_on_iso _ _ F _ _ m') (k b' a' h') == k b' a0' h0'). apply eq_iso; simpl. apply (q b' (tpair _ a0' h0') (tpair _ a' h') m'); simpl. inv_functor fH a0' a'. rewrite <- assoc. rewrite iso_after_iso_inv. apply id_right. assert (sssss : #H (l0 ;; m') == #H (m ;; l)). rewrite (functor_comp _ _ H). unfold m'; simpl. inv_functor fH a0' a'. unfold l0. inv_functor fH a0 a0'. pathvia (h0 ;; f ;; (inv_from_iso h0' ;; h0') ;; inv_from_iso h'). repeat rewrite assoc; apply idpath. rewrite iso_after_iso_inv, id_right, (functor_comp _ _ H). inv_functor fH a0 a. repeat rewrite <- assoc. apply maponpaths. apply pathsinv0. apply iso_inv_on_right. rewrite assoc. apply iso_inv_on_left. apply pathsinv0. apply alpha. assert (star5 : inv_from_iso m ;; l0 == l ;; inv_from_iso m'). apply iso_inv_on_right. rewrite assoc. apply iso_inv_on_left. apply (equal_transport_along_weq _ _ (weq_from_fully_faithful fH a0 a' )). apply pathsinv0. apply sssss. clear sssss. set (sss':= base_paths _ _ sss); simpl in sss'. assert (sss'' : k b a h ;; inv_from_iso (k b a0 h0) == inv_from_iso (functor_on_iso _ _ F _ _ m)). apply pathsinv0. apply iso_inv_on_left. apply pathsinv0. apply iso_inv_on_right. unfold m; simpl. apply pathsinv0. apply sss'. repeat rewrite assoc. rewrite sss''. clear sss'' sss' sss. rewrite <- functor_on_inv_from_iso. rewrite <- (functor_comp _ _ F). rewrite star5, functor_comp, functor_on_inv_from_iso. clear star5. assert (star4 : inv_from_iso (functor_on_iso A C F a0' a' m');; k b' a0' h0' == k b' a' h' ). apply iso_inv_on_right. set (ssss' := base_paths _ _ ssss). apply pathsinv0. simpl in ssss'. simpl. apply ssss'; clear ssss'. rewrite <- assoc. rewrite star4. apply idpath. assert (HGf : G f == inv_from_iso (k b a0 h0) ;; #F l0 ;; k b' a0' h0'). set (Gbrtilde := tpair _ (inv_from_iso (k b a0 h0) ;; #F l0 ;; k b' a0' h0') PR2 : Y b b' f). set (H' := pr2 (Y_iscontr b b' f) Gbrtilde). set (H'' := base_paths _ _ H'). simpl in H'. rewrite <- H'. apply idpath. clear PR2. assert (PR2 : forall (a : A) (h : iso (H a) b') (a' : A) (h' : iso (H a') b'') (l : a --> a'), #H l;; h' == h;; f' -> #F l;; k b'' a' h' == k b' a h;; ((inv_from_iso (k b' a0' h0');; #F l0');; k b'' a0'' h0'')). intros a' h' a'' h'' l'. intro alpha. set (m := fH^-i (iso_comp h0' (iso_inv_from_iso h'))). set (m' := fH^-i (iso_comp h0'' (iso_inv_from_iso h''))). assert (sss : iso_comp (functor_on_iso _ _ F _ _ m) (k b' a' h') == k b' a0' h0'). apply eq_iso; simpl. apply (q b' (tpair _ a0' h0') (tpair _ a' h') m); simpl. inv_functor fH a0' a'. rewrite <- assoc. rewrite iso_after_iso_inv. apply id_right. assert (ssss : iso_comp (functor_on_iso _ _ F _ _ m') (k b'' a'' h'') == k b'' a0'' h0''). apply eq_iso; simpl. apply (q b'' (tpair _ a0'' h0'') (tpair _ a'' h'') m'); simpl. inv_functor fH a0'' a''. rewrite <- assoc. rewrite iso_after_iso_inv. apply id_right. assert (sssss : #H (l0' ;; m') == #H (m ;; l')). rewrite (functor_comp _ _ H). unfold m'. simpl. inv_functor fH a0'' a''. unfold l0'. inv_functor fH a0' a0''. pathvia (h0' ;; f' ;; (inv_from_iso h0'' ;; h0'') ;; inv_from_iso h''). repeat rewrite assoc; apply idpath. rewrite iso_after_iso_inv, id_right, (functor_comp _ _ H). inv_functor fH a0' a'. repeat rewrite <- assoc. apply maponpaths, pathsinv0, iso_inv_on_right. rewrite assoc. apply iso_inv_on_left, pathsinv0, alpha. assert (star5 : inv_from_iso m ;; l0' == l' ;; inv_from_iso m'). apply iso_inv_on_right. rewrite assoc. apply iso_inv_on_left, (equal_transport_along_weq _ _ (weq_from_fully_faithful fH a0' a'' )), pathsinv0, sssss. set (sss':= base_paths _ _ sss); simpl in sss'. assert (sss'' : k b' a' h' ;; inv_from_iso (k b' a0' h0') == inv_from_iso (functor_on_iso _ _ F _ _ m)). apply pathsinv0, iso_inv_on_left, pathsinv0, iso_inv_on_right. unfold m; simpl; apply pathsinv0, sss'. repeat rewrite assoc. rewrite sss''. clear sss'' sss' sss. rewrite <- functor_on_inv_from_iso. rewrite <- (functor_comp _ _ F). rewrite star5. clear star5 sssss. rewrite functor_comp, functor_on_inv_from_iso. assert (star4 : inv_from_iso (functor_on_iso A C F a0'' a'' m');; k b'' a0'' h0'' == k b'' a'' h'' ). apply iso_inv_on_right. set (ssss' := base_paths _ _ ssss). apply pathsinv0. simpl in *; apply ssss'. rewrite <- assoc. rewrite star4. apply idpath. assert (HGf' : G f' == inv_from_iso (k b' a0' h0') ;; #F l0' ;; k b'' a0'' h0''). set (Gbrtilde := tpair _ (inv_from_iso (k b' a0' h0') ;; #F l0' ;; k b'' a0'' h0'') PR2 : Y b' b'' f'). set (H' := pr2 (Y_iscontr b' b'' f') Gbrtilde). rewrite <-(base_paths _ _ H'). apply idpath. clear PR2. assert (PR2 : forall (a : A) (h : iso (H a) b) (a' : A) (h' : iso (H a') b'') (l : a --> a'), #H l;; h' == h;; (f;; f') -> #F l;; k b'' a' h' == k b a h;; ((inv_from_iso (k b a0 h0);; #F l0'');; k b'' a0'' h0'')). intros a h a'' h'' l. intro alpha. set (m := fH^-i (iso_comp h0 (iso_inv_from_iso h))). set (m' := fH^-i (iso_comp h0'' (iso_inv_from_iso h''))). assert (sss : iso_comp (functor_on_iso _ _ F _ _ m) (k b a h) == k b a0 h0). apply eq_iso. apply (q b (tpair _ a0 h0) (tpair _ a h) m); simpl. inv_functor fH a0 a. rewrite <- assoc. rewrite iso_after_iso_inv. apply id_right. assert (ssss : iso_comp (functor_on_iso _ _ F _ _ m') (k b'' a'' h'') == k b'' a0'' h0''). apply eq_iso. apply (q b'' (tpair _ a0'' h0'') (tpair _ a'' h'') m'). simpl; inv_functor fH a0'' a''. rewrite <- assoc. rewrite iso_after_iso_inv. apply id_right. assert (sssss : #H (l0'' ;; m') == #H (m ;; l)). rewrite (functor_comp _ _ H). unfold m'. simpl. inv_functor fH a0'' a''. unfold l0''. inv_functor fH a0 a0''. pathvia (h0 ;; (f ;; f') ;; (inv_from_iso h0'' ;; h0'') ;; inv_from_iso h''). repeat rewrite assoc; apply idpath. rewrite iso_after_iso_inv, id_right, (functor_comp _ _ H). inv_functor fH a0 a. repeat rewrite <- assoc. apply maponpaths, pathsinv0, iso_inv_on_right. repeat rewrite assoc. apply iso_inv_on_left, pathsinv0. repeat rewrite <- assoc. apply alpha. assert (star5 : inv_from_iso m ;; l0'' == l ;; inv_from_iso m'). apply iso_inv_on_right. rewrite assoc. apply iso_inv_on_left. apply (equal_transport_along_weq _ _ (weq_from_fully_faithful fH a0 a'' )). apply pathsinv0, sssss. set (sss':= base_paths _ _ sss); simpl in sss'. assert (sss'' : k b a h ;; inv_from_iso (k b a0 h0) == inv_from_iso (functor_on_iso _ _ F _ _ m)). apply pathsinv0, iso_inv_on_left, pathsinv0, iso_inv_on_right. unfold m; simpl. apply pathsinv0, sss'. repeat rewrite assoc. rewrite sss''. clear sss'' sss' sss. rewrite <- functor_on_inv_from_iso. rewrite <- (functor_comp _ _ F). rewrite star5. clear star5 sssss. rewrite functor_comp, functor_on_inv_from_iso. assert (star4 : inv_from_iso (functor_on_iso A C F a0'' a'' m');; k b'' a0'' h0'' == k b'' a'' h'' ). apply iso_inv_on_right, pathsinv0, (base_paths _ _ ssss). rewrite <- assoc. rewrite star4. apply idpath. assert (HGff' : G (f ;; f') == inv_from_iso (k b a0 h0) ;; #F l0'' ;; k b'' a0'' h0''). set (Gbrtilde := tpair _ (inv_from_iso (k b a0 h0) ;; #F l0'' ;; k b'' a0'' h0'') PR2 : Y b b'' (f ;; f')). rewrite <- (pr2 (Y_iscontr b b'' (f ;; f')) Gbrtilde). apply idpath. clear PR2. rewrite HGf, HGf'. pathvia (inv_from_iso (k b a0 h0);; #F l0;; (k b' a0' h0';; inv_from_iso (k b' a0' h0'));; #F l0';; k b'' a0'' h0''). rewrite iso_inv_after_iso, id_right. rewrite HGff'. repeat rewrite <- assoc. apply maponpaths. rewrite <- L. rewrite (functor_comp _ _ F). repeat rewrite <- assoc. apply idpath. repeat rewrite <- assoc. apply idpath. Qed. (** We call the functor [GG] ... *) Definition GG : [B, C] := tpair _ preimage_functor_data is_functor_preimage_functor_data. (** ** [G] is the preimage of [F] under [ _ O H] *) (** Given any [a : A], we produce an element in [X (H a)], whose first component is [F a]. This allows to prove [G (H a) == F a]. *) Lemma qF (a0 : A) : forall (t t' : total2 (fun a : A => iso (H a) (H a0))) (f : pr1 t --> pr1 t'), #H f;; pr2 t' == pr2 t -> #F f;; #F (fH^-1 (pr2 t')) == #F (fH^-1 (pr2 t)). Proof. simpl. intros [a h] [a' h'] f L. simpl in L; simpl. rewrite <- (functor_comp A C F). apply maponpaths. apply (equal_transport_along_weq _ _ (weq_from_fully_faithful fH a a0) (f;; fH^-1 h') (fH^-1 h) ). inv_functor fH a a0. rewrite functor_comp. inv_functor fH a' a0. apply L. Qed. Definition kFa (a0 : A) : forall a : A, iso (H a) (H a0) -> iso (F a) (F a0) := fun (a : A) (h : iso (H a) (H a0)) => functor_on_iso A C F a a0 (iso_from_fully_faithful_reflection fH a a0 h). Definition XtripleF (a0 : A) : X (H a0) := tpair _ (tpair _ (F a0) (kFa a0)) (qF a0). Lemma phi (a0 : A) : pr1 (pr1 (GG O H)) a0 == pr1 (pr1 F) a0. Proof. exact (!Xphi _ (XtripleF a0)). Defined. Lemma extphi : pr1 (pr1 (GG O H)) == pr1 (pr1 F). Proof. apply funextsec. apply phi. Defined. (** Now for the functor as a whole. It remains to prove equality on morphisms, modulo transport. *) Lemma is_preimage_for_pre_composition : GG O H == F. Proof. apply (functor_eq _ _ (GG O H) F). apply (total2_paths extphi). apply funextsec; intro a0; apply funextsec; intro a0'; apply funextsec; intro f. rewrite transport_of_functor_map_is_pointwise. unfold extphi. rewrite toforallpaths_funextsec. rewrite <- idtoiso_postcompose. rewrite <- idtoiso_precompose. rewrite idtoiso_inv. rewrite <- assoc. assert (PSIf : forall (a : A) (h : iso (H a) (H a0)) (a' : A) (h' : iso (H a') (H a0')) (l : a --> a'), #H l;; h' == h;; #H f -> #F l;; k (H a0') a' h' == k (H a0) a h;; ((idtoiso (phi a0);; #F f);; inv_from_iso (idtoiso (phi a0')))). intros a h a' h' l alpha. rewrite assoc. apply iso_inv_on_left. unfold phi. repeat rewrite assoc. rewrite (Xkphi_idtoiso (H a0) (XtripleF a0)). repeat rewrite <- assoc. rewrite (Xkphi_idtoiso (H a0') (XtripleF a0')). simpl. assert (HH4 : fH^-1 h ;; f == l ;; fH^-1 h'). apply (equal_transport_along_weq _ _ (weq_from_fully_faithful fH a a0')). simpl; repeat rewrite functor_comp. inv_functor fH a a0. inv_functor fH a' a0'. apply pathsinv0, alpha. pathvia (#F (fH^-1 h;; f)). rewrite (functor_comp _ _ F). apply idpath. rewrite HH4. rewrite (functor_comp _ _ F). apply idpath. set (Ybla := tpair _ (idtoiso (phi a0) ;; #F f ;; inv_from_iso (idtoiso (phi a0'))) PSIf : Y _ _ (#H f)). set (Ycontr := pr2 (Y_iscontr _ _ (#(pr1 H) f)) Ybla). set (Ycontr2 := base_paths _ _ Ycontr); simpl in *. change (G (#H f)) with (G (#(pr1 H) f)). rewrite <- Ycontr2. repeat rewrite assoc. rewrite iso_after_iso_inv, id_left. repeat rewrite <- assoc. rewrite iso_after_iso_inv, id_right. apply idpath. Qed. End preimage. End essentially_surjective. (** * Precomposition with an ess. surj. and f. f. functor is ess. surj. *) (** Abstracting from [F] by closing the previous section, we can prove essential surjectivity of [_ O H]. *) Lemma pre_composition_essentially_surjective : essentially_surjective (pre_composition_functor A B C H). Proof. intros F p' f. apply f. exists (GG F). apply idtoiso. apply is_preimage_for_pre_composition. Qed. End precomp_w_ess_surj_ff_is_ess_surj. Ahrens-Coq/._precomp_fully_faithful.v000777 000765 000024 00000000260 12262322302 020573 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/precomp_fully_faithful.v000777 000765 000024 00000030155 12262322302 020364 0ustar00nicolastaff000000 000000 (** ********************************************************** Benedikt Ahrens, Chris Kapulkin, Mike Shulman january 2013 ************************************************************) (** ********************************************************** Contents : Precomposition with a fully faithful and essentially surjective functor yields a full and faithful, i.e. a fully faithful, functor ************************************************************) Require Import Foundations.Generalities.uu0. Require Import Foundations.hlevel1.hProp. Require Import Foundations.hlevel2.hSet. Require Import RezkCompletion.pathnotations. Import RezkCompletion.pathnotations.PathNotations. Require Import RezkCompletion.auxiliary_lemmas_HoTT. Require Import RezkCompletion.precategories. Require Import RezkCompletion.functors_transformations. Require Import RezkCompletion.whiskering. Ltac pathvia b := (apply (@pathscomp0 _ _ b _ )). Ltac simp_rew lem := let H:=fresh in assert (H:= lem); simpl in *; rewrite H; clear H. Ltac simp_rerew lem := let H:=fresh in assert (H:= lem); simpl in *; rewrite <- H; clear H. Ltac inv_functor HF x y := let H:=fresh in set (H:= homotweqinvweq (weq_from_fully_faithful HF x y)); simpl in H; unfold fully_faithful_inv_hom; simpl; rewrite H; clear H. Local Notation "a --> b" := (precategory_morphisms a b)(at level 50). (*Local Notation "'hom' C" := (precategory_morphisms (C := C)) (at level 2).*) Local Notation "f ;; g" := (compose f g)(at level 50). Notation "[ C , D ]" := (functor_precategory C D). Local Notation "# F" := (functor_on_morphisms F)(at level 3). Local Notation "G 'O' F" := (functor_compose _ _ _ F G : functor _ _ ) (at level 25). Local Notation "FF ^-1" := (fully_faithful_inv_hom FF _ _ ) (at level 20). Local Notation "F '^-i'" := (iso_from_fully_faithful_reflection F _ _) (at level 20). (** * Precomposition with an essentially surjective functor is faithful. *) Lemma pre_composition_with_ess_surj_is_faithful (A B C : precategory) (H : [A, B]) (p : essentially_surjective H) : faithful (pre_composition_functor A B C H). Proof. intros F G gamma delta ex. simpl in *. apply nat_trans_eq. intro b. assert (Heq : isaprop (gamma b == delta b)). apply (pr2 (_ --> _)). apply (p b (tpair (fun x => isaprop x) (gamma b == delta b) Heq)). simpl in *; clear Heq. intros [a f]. apply (pre_comp_with_iso_is_inj C (F (H a)) (F b) (G b) (# F f) (functor_on_iso_is_iso _ _ _ _ _ f)). repeat rewrite nat_trans_ax. change (gamma (H a)) with (pr1 gamma ((pr1 H) a)). simp_rew (nat_trans_eq_pointwise _ _ _ _ _ _ ex a). apply idpath. Qed. (** * Precomposition with an essentially surjective and f. f. functor is full *) Section precomp_with_ess_surj_ff_functor_is_full. (** Section variables *) Variables A B C : precategory. Variable H : functor A B. Hypothesis p : essentially_surjective H. Hypothesis Hff : fully_faithful H. (** We prove that [_ O H] yields a full functor. *) Section full. Variables F G : functor B C. (** We have to show that for [F] and [G], the map [(_ O H) (F,G) : (F --> G) -> (F O H --> G O H)] is full. *) Section preimage. (** Fixing a [gamma], we produce its preimage. *) Variable gamma : nat_trans (F O H) (G O H). Lemma isaprop_aux_space (b : B) : isaprop (total2 (fun g : F b --> G b => forall a : A, forall f : iso (H a) b, gamma a == #F f ;; g ;; #G (inv_from_iso f))). Proof. apply invproofirrelevance. intros x x'. apply total2_paths_hProp. intro; repeat (apply impred; intro). apply (pr2 (_ --> _)). destruct x as [g q]. destruct x' as [g' q']. simpl. apply (p b (tpair (fun x => isaprop x) (g == g') (pr2 (F b --> G b) _ _ ))). intro anoth. destruct anoth as [anot h]. set (qanoth := q anot h). assert (H1 : g == iso_inv_from_iso (functor_on_iso _ _ F _ _ h) ;; gamma anot ;; functor_on_iso _ _ G _ _ h). apply (pre_comp_with_iso_is_inj _ _ _ _ (functor_on_iso _ _ F _ _ h) (pr2 (functor_on_iso _ _ F _ _ h))). repeat rewrite assoc. rewrite iso_inv_after_iso, id_left. apply (post_comp_with_iso_is_inj _ _ _ (iso_inv_from_iso (functor_on_iso _ _ G _ _ h)) (pr2 (iso_inv_from_iso (functor_on_iso _ _ G _ _ h)))). simpl. simp_rerew (base_paths _ _ (functor_on_iso_inv _ _ G _ _ h)). repeat rewrite <- assoc. rewrite <- functor_comp. rewrite iso_inv_after_iso, functor_id, id_right. apply pathsinv0. rewrite assoc. apply qanoth. set (q'anoth := q' anot h). assert (H2 : g' == iso_inv_from_iso (functor_on_iso _ _ F _ _ h) ;; pr1 gamma anot ;; functor_on_iso _ _ G _ _ h). apply (pre_comp_with_iso_is_inj _ _ _ _ (functor_on_iso _ _ F _ _ h) (pr2 (functor_on_iso _ _ F _ _ h))). repeat rewrite assoc. rewrite iso_inv_after_iso, id_left. apply ( post_comp_with_iso_is_inj _ _ _ (iso_inv_from_iso (functor_on_iso _ _ G _ _ h)) (pr2 (iso_inv_from_iso (functor_on_iso _ _ G _ _ h)))). simpl. simp_rerew(base_paths _ _ (functor_on_iso_inv _ _ G _ _ h)). repeat rewrite <- assoc. rewrite <- functor_comp. rewrite iso_inv_after_iso, functor_id, id_right. apply pathsinv0. rewrite assoc; apply q'anoth. rewrite H1, H2. apply idpath. Qed. Lemma iscontr_aux_space (b : B) : iscontr (total2 (fun g : F b --> G b => forall a : A, forall f : iso (H a) b, gamma a == #F f ;; g ;; #G (inv_from_iso f) )). Proof. set (X := isapropiscontr (total2 (fun g : F b --> G b => forall (a : A) (f : iso (H a) b), gamma a == (#F f;; g);; #G (inv_from_iso f)))). apply (p b (tpair (fun x => isaprop x) _ X)). intros [anot h]. simpl in *. set (g := #F (inv_from_iso h) ;; gamma anot ;; #G h). assert (gp : forall (a : A) (f : iso (H a) b), gamma a == #F f ;; g ;; #G (inv_from_iso f)). clear X. intros a f. set (k := iso_from_fully_faithful_reflection Hff _ _ (iso_comp f (iso_inv_from_iso h))). set (GHk := functor_on_iso _ _ G _ _ (functor_on_iso _ _ H _ _ k)). pathvia (#F (#H k) ;; gamma anot ;; iso_inv_from_iso GHk). apply (post_comp_with_iso_is_inj _ _ _ GHk (pr2 GHk)). rewrite <- assoc. change (iso_inv_from_iso GHk ;; GHk) with (inv_from_iso GHk ;; GHk). rewrite iso_after_iso_inv, id_right. simp_rew (nat_trans_ax _ _ gamma). apply idpath. unfold GHk. rewrite <- functor_on_iso_inv. unfold k; simpl. rewrite functor_on_iso_iso_from_fully_faithful_reflection. simp_rew (base_paths _ _ (iso_inv_of_iso_comp _ _ _ _ f (iso_inv_from_iso h))). rewrite functor_comp. inv_functor Hff a anot. simp_rew (base_paths _ _ (iso_inv_iso_inv _ _ _ h)). rewrite functor_comp. unfold g; repeat rewrite assoc. apply idpath. apply iscontraprop1. apply isaprop_aux_space. exists g. apply gp. Qed. Definition pdelta : forall b : B, F b --> G b := fun b => pr1 (pr1 (iscontr_aux_space b)). Lemma is_nat_trans_pdelta : is_nat_trans F G pdelta. Proof. intros b b' f. apply pathsinv0. apply (p b (tpair (fun x => isaprop x) (pdelta b;; #G f == #F f;; pdelta b') (pr2 (F b --> G b') _ _ ))). intro t; destruct t as [a h]. simpl in *. apply (p b' (tpair (fun x => isaprop x) (pdelta b;; #G f == #F f;; pdelta b') (pr2 (F b --> G b') _ _ ))). simpl in *. intro t; destruct t as [a' h']. assert (Hb : pdelta b == inv_from_iso (functor_on_iso _ _ F _ _ h) ;; gamma a ;; #G h). apply (pre_comp_with_iso_is_inj _ _ _ _ (functor_on_iso _ _ F _ _ h) (pr2 (functor_on_iso _ _ F _ _ h))). repeat rewrite assoc. rewrite iso_inv_after_iso, id_left. apply ( post_comp_with_iso_is_inj _ _ _ (iso_inv_from_iso (functor_on_iso _ _ G _ _ h)) (pr2 (iso_inv_from_iso (functor_on_iso _ _ G _ _ h)))). simpl. simp_rerew (base_paths _ _ (functor_on_iso_inv _ _ G _ _ h)). repeat rewrite <- assoc. rewrite <- functor_comp. rewrite iso_inv_after_iso, functor_id, id_right. apply pathsinv0. rewrite assoc. apply (pr2 ((pr1 (iscontr_aux_space b))) a h). assert (Hb' : pdelta b' == inv_from_iso (functor_on_iso _ _ F _ _ h') ;; gamma a' ;; #G h'). apply (pre_comp_with_iso_is_inj _ _ _ _ (functor_on_iso _ _ F _ _ h') (pr2 (functor_on_iso _ _ F _ _ h'))). repeat rewrite assoc. rewrite iso_inv_after_iso, id_left. apply ( post_comp_with_iso_is_inj _ _ _ (iso_inv_from_iso (functor_on_iso _ _ G _ _ h')) (pr2 (iso_inv_from_iso (functor_on_iso _ _ G _ _ h')))). simpl. simp_rerew (base_paths _ _ (functor_on_iso_inv _ _ G _ _ h')). repeat rewrite <- assoc. rewrite <- functor_comp. rewrite iso_inv_after_iso, functor_id, id_right. apply pathsinv0. rewrite assoc. apply (pr2 (pr1 (iscontr_aux_space b')) a' h'). rewrite Hb. repeat rewrite <- assoc. simpl in *. rewrite <- (functor_comp _ _ G _ _ _ h f). pathvia (inv_from_iso (functor_on_iso B C F (H a) b h);; (gamma a;; #G (h;; f ;; iso_inv_from_iso h' ;; h')) ). repeat rewrite <- assoc. simpl. rewrite iso_after_iso_inv, id_right. apply idpath. repeat rewrite precategory_assoc. rewrite (functor_comp _ _ G). set (k := Hff^-1 (h ;; (f ;; (iso_inv_from_iso h')))). assert (P := nat_trans_ax _ _ gamma _ _ k). simpl in *. unfold k in P. simpl in P. set (H3 := homotweqinvweq (weq_from_fully_faithful Hff a a')). simpl in H3. unfold fully_faithful_inv_hom in P. simpl in P. rewrite H3 in P. clear H3. repeat rewrite <- assoc. rewrite (assoc _ _ _ _ _ (gamma a)). simpl in *. rewrite <- P; clear P. set (H4 := functor_on_iso_inv _ _ F _ _ h). set (H5 := base_paths _ _ H4). simpl in H5. rewrite <- H5. repeat rewrite assoc. rewrite <- (functor_comp _ _ F). repeat rewrite assoc. rewrite iso_after_iso_inv, id_left, (functor_comp _ _ F), functor_on_inv_from_iso. apply pathsinv0. rewrite Hb'. repeat rewrite assoc. apply idpath. Qed. Definition delta : nat_trans F G. Proof. exists pdelta. apply is_nat_trans_pdelta. Defined. Lemma pdelta_preimage : pre_whisker _ _ _ H _ _ delta == gamma. Proof. simpl in *. apply nat_trans_eq; intro a. unfold pre_whisker. simpl. set (tr := pr1 (iscontr_aux_space (H a))). change (gamma a) with (pr1 gamma a). pathvia ((#F (identity (H a));; pr1 tr);; #G (inv_from_iso (identity_iso (H a)))). rewrite (functor_id _ _ F). rewrite id_left. set (P := iso_inv_of_iso_id _ (H a)). set (Pr := base_paths _ _ P); simpl in Pr. rewrite Pr. clear Pr P. simpl in *. rewrite (functor_id _ _ G) . rewrite id_right. apply idpath. apply pathsinv0. apply (pr2 tr a (identity_iso _ )). Qed. End preimage. End full. (** * Precomposition with an essentially surjective and f. f. functor is fully faithful *) Lemma pre_composition_with_ess_surj_and_fully_faithful_is_full : full (pre_composition_functor A B C H). Proof. unfold full. intros F G gamma. apply hinhpr. exists (delta F G gamma). apply pdelta_preimage. Defined. Lemma pre_composition_with_ess_surj_and_fully_faithful_is_full_and_faithful : full_and_faithful (pre_composition_functor A B C H). Proof. split. apply pre_composition_with_ess_surj_and_fully_faithful_is_full. apply pre_composition_with_ess_surj_is_faithful. assumption. Qed. Lemma pre_composition_with_ess_surj_and_fully_faithful_is_fully_faithful : fully_faithful (pre_composition_functor A B C H). Proof. apply full_and_faithful_implies_fully_faithful. apply pre_composition_with_ess_surj_and_fully_faithful_is_full_and_faithful. Qed. End precomp_with_ess_surj_ff_functor_is_full. Ahrens-Coq/._README.md000777 000765 000024 00000000260 12262322302 015121 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/README.md000777 000765 000024 00000001231 12262322302 014703 0ustar00nicolastaff000000 000000 Rezk Completion =============== This Coq library mechanizes the Rezk completion as described in http://arxiv.org/abs/1303.0584 It builds upon V. Voevodsky's Foundations library, available on http://arxiv.org/abs/1401.0053 ## Requirements ### Coq The library compiles under Coq8.3pl5, patched according to the instructions given in http://arxiv.org/abs/1401.0053. Lower patch levels of Coq8.3, e.g., Coq8.3pl2, are likely to work as well. ### Libraries Files used from V. Voevodsky's Foundations: - uuu.v - uu0.v - hProp.v - hSet.v - funextfun.v They should be installed in the user-contrib/Foundations directory of Coq, so Coq can find them. Ahrens-Coq/._rezk_completion.v000777 000765 000024 00000000260 12262322302 017235 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/rezk_completion.v000777 000765 000024 00000006123 12262322302 017024 0ustar00nicolastaff000000 000000 (** ********************************************************** Benedikt Ahrens, Chris Kapulkin, Mike Shulman january 2013 ************************************************************) (** ********************************************************** Contents : Rezk completion - Construction of the Rezk completion via Yoneda - Universal property of the Rezk completion ************************************************************) Require Import Foundations.Generalities.uu0. Require Import Foundations.hlevel1.hProp. Require Import Foundations.hlevel2.hSet. Require Import RezkCompletion.pathnotations. Import RezkCompletion.pathnotations.PathNotations. Require Import RezkCompletion.auxiliary_lemmas_HoTT. Require Import RezkCompletion.precategories. Require Import RezkCompletion.functors_transformations. Require Import RezkCompletion.category_hset. Require Import RezkCompletion.yoneda. Require Import RezkCompletion.sub_precategories. Require Import RezkCompletion.equivalences. Require Import RezkCompletion.whiskering. Require Import RezkCompletion.precomp_fully_faithful. Require Import RezkCompletion.precomp_ess_surj. Ltac pathvia b := (apply (@pathscomp0 _ _ b _ )). (** * Construction of the Rezk completion via Yoneda *) Section rezk. Variable A : precategory. Definition Rezk_completion : category. Proof. exists (full_img_sub_precategory (yoneda A)). apply is_category_full_subcat. apply is_category_functor_category. apply is_category_HSET. Defined. Definition Rezk_eta : functor A Rezk_completion. Proof. apply (functor_full_img (yoneda A)). Defined. Lemma Rezk_eta_is_fully_faithful : fully_faithful Rezk_eta. Proof. apply (functor_full_img_fully_faithful_if_fun_is _ _ (yoneda A)). apply yoneda_fully_faithful. Qed. Lemma Rezk_eta_essentially_surjective : essentially_surjective Rezk_eta. Proof. apply (functor_full_img_essentially_surjective _ _ (yoneda A)). Qed. End rezk. (** * Universal property of the Rezk completion *) Section rezk_universal_property. Variables A C : precategory. Hypothesis Ccat : is_category C. Lemma pre_comp_rezk_eta_is_fully_faithful : fully_faithful (pre_composition_functor A (Rezk_completion A) C (Rezk_eta A)). Proof. apply pre_composition_with_ess_surj_and_fully_faithful_is_fully_faithful. apply Rezk_eta_essentially_surjective. apply Rezk_eta_is_fully_faithful. Qed. Lemma pre_comp_rezk_eta_is_ess_surj : essentially_surjective (pre_composition_functor A (Rezk_completion A) C (Rezk_eta A)). Proof. apply pre_composition_essentially_surjective. assumption. apply Rezk_eta_essentially_surjective. apply Rezk_eta_is_fully_faithful. Qed. Theorem Rezk_eta_Universal_Property : isweq (pre_composition_functor A (Rezk_completion A) C (Rezk_eta A)). Proof. apply equiv_of_cats_is_weq_of_objects. apply is_category_functor_category; assumption. apply is_category_functor_category; assumption. apply rad_equivalence_of_precats. apply is_category_functor_category; assumption. apply pre_comp_rezk_eta_is_fully_faithful. apply pre_comp_rezk_eta_is_ess_surj. Qed. End rezk_universal_property. Ahrens-Coq/._sub_precategories.v000777 000765 000024 00000000260 12262322302 017536 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/sub_precategories.v000777 000765 000024 00000043514 12262322302 017332 0ustar00nicolastaff000000 000000 (** ********************************************************** Benedikt Ahrens, Chris Kapulkin, Mike Shulman january 2013 ************************************************************) (** ********************************************************** Contents : Subcategories, Full subcats Image of a functor, full subcat specified by a functor Subcategories, back to Inclusion functor Full image of a functor Factorization of a functor via its full image This factorization is fully faithful if the functor is [functor_full_img_fully_faithful_if_fun_is] Isos in full subcategory are equiv to isos in the precategory Full subcategory of a category is a category [is_category_full_subcat] ************************************************************) Require Import Foundations.hlevel2.hSet. Require Import RezkCompletion.pathnotations. Import RezkCompletion.pathnotations.PathNotations. Require Import RezkCompletion.auxiliary_lemmas_HoTT. Require Import RezkCompletion.precategories. Require Import RezkCompletion.functors_transformations. Local Notation "a --> b" := (precategory_morphisms a b)(at level 50). Local Notation "f ;; g" := (compose f g)(at level 50). Local Notation "# F" := (functor_on_morphisms F)(at level 3). (** * Sub-precategories *) (** A sub-precategory is specified through a predicate on objects and a dependent predicate on morphisms which is compatible with identity and composition *) Definition is_sub_precategory {C : precategory} (C' : hsubtypes C) (Cmor' : forall a b : C, hsubtypes (a --> b)) := dirprod (forall a : C, C' a -> Cmor' _ _ (identity a )) (forall (a b c : C) (f: a --> b) (g : b --> c), Cmor' _ _ f -> Cmor' _ _ g -> Cmor' _ _ (f ;; g)). Definition sub_precategories (C : precategory) := total2 ( fun C' : dirprod (hsubtypes (ob C)) (forall a b:ob C, hsubtypes (a --> b)) => is_sub_precategory (pr1 C') (pr2 C')). (** A full subcategory has the true predicate on morphisms *) Lemma is_sub_precategory_full (C : precategory) (C':hsubtypes (ob C)) : is_sub_precategory C' (fun a b => fun f => htrue). Proof. split; intros; exact tt. Defined. Definition full_sub_precategory {C : precategory} (C': hsubtypes (ob C)) : sub_precategories C := tpair _ (dirprodpair C' (fun a b f => htrue)) (is_sub_precategory_full C C'). (** We have a coercion [carrier] turning every predicate [P] on a type [A] into the total space [ { a : A & P a} ]. For later, we define some projections with the appropriate type, also to avoid confusion with the aforementioned coercion. *) Definition sub_precategory_predicate_objects {C : precategory} (C': sub_precategories C): hsubtypes (ob C) := pr1 (pr1 C'). Definition sub_ob {C : precategory}(C': sub_precategories C): UU := (*carrier*) (sub_precategory_predicate_objects C'). Definition sub_precategory_predicate_morphisms {C : precategory} (C':sub_precategories C) (a b : C) : hsubtypes (a --> b) := pr2 (pr1 C') a b. Definition sub_precategory_morphisms {C : precategory}(C':sub_precategories C) (a b : C) : UU := sub_precategory_predicate_morphisms C' a b. (** Projections for compatibility of the predicate with identity and composition. *) Definition sub_precategory_id (C : precategory)(C':sub_precategories C) : forall a : ob C, sub_precategory_predicate_objects C' a -> sub_precategory_predicate_morphisms C' _ _ (identity a) := pr1 (pr2 C'). Definition sub_precategory_comp (C : precategory)(C':sub_precategories C) : forall (a b c: ob C) (f: a --> b) (g : b --> c), sub_precategory_predicate_morphisms C' _ _ f -> sub_precategory_predicate_morphisms C' _ _ g -> sub_precategory_predicate_morphisms C' _ _ (f ;; g) := pr2 (pr2 C'). (** the following lemma should be an instance of a general theorem saying that subtypes of a type of hlevel n are of hlevel n, but i haven't found that theorem *) Lemma is_set_sub_precategory_morphisms {C : precategory}(C':sub_precategories C) (a b : ob C) : isaset (sub_precategory_morphisms C' a b). Proof. change (isaset) with (isofhlevel 2). apply isofhleveltotal2. apply setproperty. intro f. apply isasetaprop. apply propproperty. Qed. Definition sub_precategory_morphisms_set {C : precategory}(C':sub_precategories C) (a b : ob C) : hSet := tpair _ (sub_precategory_morphisms C' a b) (is_set_sub_precategory_morphisms C' a b). (** An object of a subcategory is an object of the original precategory. *) Definition precategory_object_from_sub_precategory_object (C:precategory) (C':sub_precategories C) (a : sub_ob C') : ob C := pr1 a. Coercion precategory_object_from_sub_precategory_object : sub_ob >-> ob. (** A morphism of a subcategory is also a morphism of the original precategory. *) Definition precategory_morphism_from_sub_precategory_morphism (C:precategory) (C':sub_precategories C) (a b : ob C) (f : sub_precategory_morphisms C' a b) : a --> b := pr1 f . Coercion precategory_morphism_from_sub_precategory_morphism : sub_precategory_morphisms >-> pr1hSet. (** ** A sub-precategory forms a precategory. *) Definition sub_precategory_ob_mor (C : precategory)(C':sub_precategories C) : precategory_ob_mor. Proof. exists (sub_ob C'). exact (fun a b => @sub_precategory_morphisms_set _ C' a b). Defined. (* Coercion sub_precategory_ob_mor : sub_precategories >-> precategory_ob_mor. *) Definition sub_precategory_data (C : precategory)(C':sub_precategories C) : precategory_data. Proof. exists (sub_precategory_ob_mor C C'). split. intro c. exists (identity (C:=C) (pr1 c)). apply sub_precategory_id. apply (pr2 c). intros a b c f g. exists (compose (pr1 f) (pr1 g)). apply sub_precategory_comp. apply (pr2 f). apply (pr2 g). Defined. (** A useful lemma for equality in the sub-precategory. *) Lemma eq_in_sub_precategory (C : precategory)(C':sub_precategories C) (a b : sub_ob C') (f g : sub_precategory_morphisms C' a b) : pr1 f == pr1 g -> f == g. Proof. intro H. destruct f as [f p]. destruct g as [g p']. apply (total2_paths H). apply proofirrelevance. apply pr2. Qed. (* Lemma eq_in_sub_precategory2 (C : precategory)(C':sub_precategories C) (a b : sub_ob C') (f g : a --> b) (pf : sub_precategory_predicate_morphisms C' _ _ f) (pg : sub_precategory_predicate_morphisms C' _ _ g): f == g -> (tpair (fun f => sub_precategory_predicate_morphisms _ _ _ f) f pf) == (tpair (fun f => sub_precategory_predicate_morphisms _ _ _ f) g pg). Proof. intro H. apply (total2_paths2 H). destruct H. apply (total2_paths2 (idpath _ )). *) Definition is_precategory_sub_category (C : precategory)(C':sub_precategories C) : is_precategory (sub_precategory_data C C'). Proof. repeat split; simpl; intros. unfold sub_precategory_comp; apply eq_in_sub_precategory; simpl; apply id_left. apply eq_in_sub_precategory. simpl. apply id_right. apply eq_in_sub_precategory. simpl. apply assoc. Qed. Definition carrier_of_sub_precategory (C : precategory)(C':sub_precategories C) : precategory := tpair _ _ (is_precategory_sub_category C C'). Coercion carrier_of_sub_precategory : sub_precategories >-> precategory. (** An object satisfying the predicate is an object of the subcategory *) Definition precategory_object_in_subcat {C : precategory} {C':sub_precategories C} (a : ob C)(p : sub_precategory_predicate_objects C' a) : ob C' := tpair _ a p. (** A morphism satisfying the predicate is a morphism of the subcategory *) Definition precategory_morphisms_in_subcat {C : precategory} {C':sub_precategories C} {a b : ob C'}(f : pr1 a --> pr1 b) (p : sub_precategory_predicate_morphisms C' (pr1 a) (pr1 b) (f)) : precategory_morphisms (C:=C') a b := tpair _ f p. (** ** Functor from a sub-precategory to the ambient precategory *) Definition sub_precategory_inclusion_data (C : precategory) (C':sub_precategories C): functor_data C' C. Proof. exists (@pr1 _ _ ). intros a b. exact (@pr1 _ _ ). Defined. Definition is_functor_sub_precategory_inclusion (C : precategory) (C':sub_precategories C) : is_functor (sub_precategory_inclusion_data C C'). Proof. split; simpl; intros; apply (idpath _ ). Qed. Definition sub_precategory_inclusion (C : precategory)(C': sub_precategories C) : functor C' C := tpair _ _ (is_functor_sub_precategory_inclusion C C'). (** ** The (full) image of a functor *) Definition full_img_sub_precategory {C D : precategory}(F : functor C D) : sub_precategories D := full_sub_precategory (sub_img_functor F). (** ** Given a functor F : C -> D, we obtain a functor F : C -> Img(F) *) Definition full_img_functor_obj {C D : precategory}(F : functor C D) : ob C -> ob (full_img_sub_precategory F). Proof. intro c. exists (F c). intros a b. apply b. exists c. apply identity_iso. Defined. Definition full_img_functor_data {C D : precategory}(F : functor C D) : functor_data C (full_img_sub_precategory F). Proof. exists (full_img_functor_obj F). intros a b f. exists (#F f). exact tt. Defined. Lemma is_functor_full_img (C D: precategory) (F : functor C D) : is_functor (full_img_functor_data F). Proof. split. intro a; simpl. apply total2_paths_hProp. intro; apply propproperty. apply functor_id. intros a b c f g. set ( H := eq_in_sub_precategory D (full_img_sub_precategory F)). apply (H (full_img_functor_obj F a)(full_img_functor_obj F c)). simpl; apply functor_comp. Qed. Definition functor_full_img {C D: precategory} (F : functor C D) : functor C (full_img_sub_precategory F) := tpair _ _ (is_functor_full_img C D F). (** *** Morphisms in the full subprecat are equiv to morphisms in the precategory *) (** does of course not need the category hypothesis *) Definition hom_in_subcat_from_hom_in_precat (C : precategory) (C' : hsubtypes (ob C)) (a b : ob (full_sub_precategory C')) (f : pr1 a --> pr1 b) : a --> b := tpair _ f tt. Definition hom_in_precat_from_hom_in_full_subcat (C : precategory) (C' : hsubtypes (ob C)) (a b : ob (full_sub_precategory C')) : a --> b -> pr1 a --> pr1 b := @pr1 _ _ . Lemma isweq_hom_in_precat_from_hom_in_full_subcat (C : precategory) (C' : hsubtypes (ob C)) (a b : ob (full_sub_precategory C')): isweq (hom_in_precat_from_hom_in_full_subcat _ _ a b). Proof. apply (gradth _ (hom_in_subcat_from_hom_in_precat _ _ a b)). intro f. destruct f. simpl. apply eq_in_sub_precategory. apply idpath. intros. apply idpath. Defined. Lemma isweq_hom_in_subcat_from_hom_in_precat (C : precategory) (C' : hsubtypes (ob C)) (a b : ob (full_sub_precategory C')): isweq (hom_in_subcat_from_hom_in_precat _ _ a b). Proof. apply (gradth _ (hom_in_precat_from_hom_in_full_subcat _ _ a b)). intro f. intros. apply idpath. intro f. destruct f. simpl. apply eq_in_sub_precategory. apply idpath. Defined. Definition weq_hom_in_subcat_from_hom_in_precat (C : precategory) (C' : hsubtypes (ob C)) (a b : ob (full_sub_precategory C')): weq (pr1 a --> pr1 b) (a-->b) := tpair _ _ (isweq_hom_in_subcat_from_hom_in_precat C C' a b). Lemma image_is_in_image (C D : precategory) (F : functor C D) (a : ob C): is_in_img_functor F (F a). Proof. apply hinhpr. exists a. apply identity_iso. Defined. Lemma functor_full_img_fully_faithful_if_fun_is (C D : precategory) (F : functor C D) (H : fully_faithful F) : fully_faithful (functor_full_img F). Proof. unfold fully_faithful in *. intros a b. set (H' := weq_hom_in_subcat_from_hom_in_precat). set (H'' := H' D (is_in_img_functor F)). set (Fa := tpair (fun a : ob D => is_in_img_functor F a) (F a) (image_is_in_image _ _ F a)). set (Fb := tpair (fun a : ob D => is_in_img_functor F a) (F b) (image_is_in_image _ _ F b)). set (H3 := (H'' Fa Fb)). assert (H2 : functor_on_morphisms (functor_full_img F) (a:=a) (b:=b) == funcomp (functor_on_morphisms F (a:=a) (b:=b)) ((H3))). apply funextsec. intro f. apply idpath. rewrite H2. apply twooutof3c. apply H. apply pr2. Qed. (** *** Image factorization C -> Img(F) -> D *) Lemma functor_full_img_factorization_ob (C D: precategory) (F : functor C D): functor_on_objects F == functor_on_objects (functor_composite _ _ _ (functor_full_img F) (sub_precategory_inclusion D _)). Proof. simpl. apply etacorrection. Defined. (** works up to eta conversion *) (* Lemma functor_full_img_factorization (C D: precategory) (F : functor C D) : F == functor_composite _ _ _ (functor_full_img F) (sub_precategory_inclusion D _). Proof. apply functor_eq. About functor_full_img_factorization_ob. set (H := functor_full_img_factorization_ob C D F). simpl in *. destruct F as [F Fax]. simpl. destruct F as [Fob Fmor]; simpl in *. apply (total2_paths2 (H)). unfold functor_full_img_factorization_ob in H. simpl in *. apply dep_funextfunax. intro a. apply dep_funextfunax. intro b. apply funextfunax. intro f. generalize Fmor. clear Fax. assert (H' : Fob == (fun a : ob C => Fob a)). apply H. generalize dependent a . generalize dependent b. clear Fmor. generalize H. clear H. intro H. clear H'. destruct H. tion H. induction H'. induction H'. clear H. *) (** ** Any full subprecategory of a category is a category. *) Section full_sub_cat. Variable C : precategory. Hypothesis H : is_category C. Variable C' : hsubtypes (ob C). (** *** Isos in the full subcategory are equivalent to isos in the precategory *) Lemma iso_in_subcat_is_iso_in_precat (a b : ob (full_sub_precategory C')) (f : iso a b): is_isomorphism (C:=C) (a:=pr1 a) (b:=pr1 b) (pr1 (pr1 f)). Proof. destruct f as [f fp]. destruct fp as [g gx]. simpl in *. exists g. destruct gx as [t tp]; simpl in *. split; simpl. apply (base_paths _ _ t). apply (base_paths _ _ tp). Qed. Lemma iso_in_precat_is_iso_in_subcat (a b : ob (full_sub_precategory C')) (f : iso (pr1 a) (pr1 b)) : is_isomorphism (C:=full_sub_precategory C') (precategory_morphisms_in_subcat f tt). Proof. destruct f as [f fp]. destruct fp as [g gax]. destruct gax as [g1 g2]. exists (precategory_morphisms_in_subcat g tt). split; simpl in *. apply eq_in_sub_precategory. simpl. assumption. apply eq_in_sub_precategory. simpl. assumption. Qed. Definition iso_from_iso_in_sub (a b : ob (full_sub_precategory C')) (f : iso a b) : iso (pr1 a) (pr1 b) := tpair _ _ (iso_in_subcat_is_iso_in_precat a b f). Definition iso_in_sub_from_iso (a b : ob (full_sub_precategory C')) (f : iso (pr1 a) (pr1 b)) : iso a b := tpair _ _ (iso_in_precat_is_iso_in_subcat a b f). Lemma isweq_iso_from_iso_in_sub (a b : ob (full_sub_precategory C')): isweq (iso_from_iso_in_sub a b). Proof. apply (gradth _ (iso_in_sub_from_iso a b)). intro f. apply eq_iso; simpl. apply eq_in_sub_precategory, idpath. intro f; apply eq_iso, idpath. Defined. Lemma isweq_iso_in_sub_from_iso (a b : ob (full_sub_precategory C')): isweq (iso_in_sub_from_iso a b). Proof. apply (gradth _ (iso_from_iso_in_sub a b)). intro f; apply eq_iso, idpath. intro f; apply eq_iso; simpl; apply eq_in_sub_precategory, idpath. Defined. (** *** From Identity in the subcategory to isos in the category *) (** This gives a weak equivalence *) Definition Id_in_sub_to_iso (a b : ob (full_sub_precategory C')): a == b -> iso (pr1 a) (pr1 b) := funcomp (@idtoiso _ a b) (iso_from_iso_in_sub a b). Lemma Id_in_sub_to_iso_equal_iso (a b : ob (full_sub_precategory C')) : Id_in_sub_to_iso a b == funcomp (total_paths2_hProp_equiv C' a b) (@idtoiso _ (pr1 a) (pr1 b)). Proof. apply funextfunax. intro p. destruct p. apply eq_iso; simpl; apply idpath. Qed. Lemma isweq_Id_in_sub_to_iso (a b : ob (full_sub_precategory C')): isweq (Id_in_sub_to_iso a b). Proof. rewrite Id_in_sub_to_iso_equal_iso. apply twooutof3c. apply pr2. apply H. Defined. (** *** Decomp of map from id in the subcat to isos in the subcat via isos in ambient precat *) Lemma precat_paths_in_sub_as_3_maps (a b : ob (full_sub_precategory C')): @idtoiso _ a b == funcomp (Id_in_sub_to_iso a b) (iso_in_sub_from_iso a b). Proof. apply funextfunax. intro p; destruct p. apply eq_iso; simpl. unfold precategory_morphisms_in_subcat. apply eq_in_sub_precategory, idpath. Qed. (** *** The aforementioned decomposed map is a weak equivalence *) Lemma isweq_sub_precat_paths_to_iso (a b : ob (full_sub_precategory C')) : isweq (@idtoiso _ a b). Proof. rewrite precat_paths_in_sub_as_3_maps. apply twooutof3c. apply isweq_Id_in_sub_to_iso. apply isweq_iso_in_sub_from_iso. Defined. (** ** Proof of the targeted theorem: full subcats of cats are cats *) Lemma is_category_full_subcat: is_category (full_sub_precategory C'). Proof. unfold is_category. apply isweq_sub_precat_paths_to_iso. Defined. End full_sub_cat. Lemma functor_full_img_essentially_surjective (A B : precategory) (F : functor A B) : essentially_surjective (functor_full_img F). Proof. intro b. apply (pr2 b). intros [c h] q Hq. apply Hq. exists c. apply iso_in_sub_from_iso. apply h. Qed. Ahrens-Coq/._whiskering.v000777 000765 000024 00000000260 12262322302 016203 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/whiskering.v000777 000765 000024 00000007157 12262322302 016002 0ustar00nicolastaff000000 000000 (** ********************************************************** Benedikt Ahrens, Chris Kapulkin, Mike Shulman january 2013 ************************************************************) (** ********************************************************** Contents : - Precomposition with a functor for - functors and - natural transformations (whiskering) - Functoriality of precomposition - Precomposition with an essentially surjective functor yields a faithful functor ************************************************************) Require Import Foundations.Generalities.uu0. Require Import Foundations.hlevel1.hProp. Require Import Foundations.hlevel2.hSet. Require Import RezkCompletion.pathnotations. Import RezkCompletion.pathnotations.PathNotations. Require Import RezkCompletion.auxiliary_lemmas_HoTT. Require Import RezkCompletion.precategories. Require Import RezkCompletion.functors_transformations. Ltac pathvia b := (apply (@pathscomp0 _ _ b _ )). Local Notation "a --> b" := (precategory_morphisms a b)(at level 50). (*Local Notation "'hom' C" := (precategory_morphisms (C := C)) (at level 2).*) Local Notation "f ;; g" := (compose f g)(at level 50). Notation "[ C , D ]" := (functor_precategory C D). Local Notation "# F" := (functor_on_morphisms F)(at level 3). Definition functor_compose (A B C : precategory) (F : ob [A, B]) (G : ob [B , C]) : ob [A , C] := functor_composite _ _ _ F G. Local Notation "G 'O' F" := (functor_compose _ _ _ F G) (at level 25). Local Notation "G 'o' F" := (functor_compose _ _ _ F G : functor _ _ ) (at level 25). (** * Whiskering: Composition of a natural transformation with a functor *) (** Prewhiskering *) Lemma is_nat_trans_pre_whisker (A B C : precategory) (F : functor A B) (G H : functor B C) (gamma : nat_trans G H) : is_nat_trans (G o F) (H o F) (fun a : ob A => gamma (F a)). Proof. unfold is_nat_trans. intros; simpl; rewrite nat_trans_ax. apply idpath. Qed. Definition pre_whisker (A B C : precategory) (F : ob [A, B]) (G H : ob [B, C]) (gamma : G --> H) : G O F --> H O F. Proof. exists (fun a => pr1 gamma (pr1 F a)). apply is_nat_trans_pre_whisker. Defined. (** Postwhiskering *) Lemma is_precat_fun_fun_post_whisker (B C D : precategory) (G H : functor B C) (gamma : nat_trans G H) (K : functor C D): is_nat_trans (functor_composite _ _ _ G K) (functor_composite _ _ _ H K) (fun b : B => #K (gamma b)). Proof. unfold is_nat_trans. simpl in *. intros; repeat rewrite <- functor_comp. rewrite (nat_trans_ax _ _ gamma). apply idpath. Qed. Definition post_whisker (B C D : precategory) (G H : ob [B, C]) (gamma : G --> H) (K : ob [C, D]) : K O G --> K O H. Proof. exists (fun a : ob B => #(pr1 K) (pr1 gamma a)). apply is_precat_fun_fun_post_whisker. Defined. (** Precomposition with a functor is functorial *) (** Postcomposition is, too, but that's not of our concern for now. *) Definition pre_composition_functor_data (A B C : precategory) (H : ob [A, B]) : functor_data [B,C] [A,C]. Proof. exists (fun G => G O H). exact (fun a b gamma => pre_whisker _ _ _ H _ _ gamma). Defined. Lemma pre_composition_is_functor (A B C : precategory) (H : [A, B]) : is_functor (pre_composition_functor_data A B C H). Proof. split; simpl. intro G. apply nat_trans_eq. intro a. apply idpath. intros; apply nat_trans_eq. intro; apply idpath. Qed. Definition pre_composition_functor (A B C : precategory) (H : [A , B]) : functor [B, C] [A, C]. Proof. exists (pre_composition_functor_data A B C H). apply pre_composition_is_functor. Defined. Ahrens-Coq/._yoneda.v000777 000765 000024 00000000260 12262322302 015310 0ustar00nicolastaff000000 000000 Mac OS X  2~°ATTR°˜˜com.apple.quarantineq/0001;53a8538a;Safari;Ahrens-Coq/yoneda.v000777 000765 000024 00000016504 12262322302 015103 0ustar00nicolastaff000000 000000 (** ********************************************************** Benedikt Ahrens, Chris Kapulkin, Mike Shulman january 2013 ************************************************************) (** ********************************************************** Contents : Definition of opposite category Definition of the Yoneda functor [yoneda(C) : [C, [C^op, HSET]]] Proof that [yoneda(C)] is fully faithful ************************************************************) Require Import Foundations.Generalities.uu0. Require Import Foundations.hlevel1.hProp. Require Import Foundations.hlevel2.hSet. Require Import RezkCompletion.pathnotations. Import RezkCompletion.pathnotations.PathNotations. Require Import RezkCompletion.auxiliary_lemmas_HoTT. Require Import RezkCompletion.precategories. Require Import RezkCompletion.category_hset. Require Import RezkCompletion.functors_transformations. (*Local Notation "a --> b" := (precategory_morphisms a b)(at level 50).*) Local Notation "'hom' C" := (precategory_morphisms (C := C)) (at level 2). Local Notation "f ;; g" := (compose f g)(at level 50). Notation "[ C , D ]" := (functor_precategory C D). Local Notation "# F" := (functor_on_morphisms F)(at level 3). Ltac pathvia b := (apply (@pathscomp0 _ _ b _ )). (** * The opposite precategory of a precategory *) Definition opp_precat_ob_mor (C : precategory_ob_mor) : precategory_ob_mor := tpair (fun ob : UU => ob -> ob -> hSet) (ob C) (fun a b : ob C => hom C b a ). Definition opp_precat_data (C : precategory_data) : precategory_data. Proof. exists (opp_precat_ob_mor C). split. exact (fun c => identity c). simpl. intros a b c f g. exact (g ;; f). Defined. Hint Unfold identity. Ltac unf := unfold identity, compose, precategory_morphisms; simpl. Lemma is_precat_opp_precat_data (C : precategory) : is_precategory (opp_precat_data C). Proof. repeat split; simpl. intros. unf. apply id_right. intros; unf. apply id_left. intros; unf. rewrite assoc. apply idpath. Qed. Definition opp_precat (C : precategory) : precategory := tpair _ (opp_precat_data C) (is_precat_opp_precat_data C). Notation "C '^op'" := (opp_precat C) (at level 3). (** * Yoneda functor *) (** ** On objects *) Definition yoneda_objects_ob (C : precategory) (c : C) (d : C) := hom C d c. Definition yoneda_objects_mor (C : precategory) (c : C) (d d' : C) (f : hom C d d') : yoneda_objects_ob C c d' -> yoneda_objects_ob C c d := fun g => f ;; g. Definition yoneda_ob_functor_data (C : precategory) (c : C) : functor_data (C^op) HSET. Proof. exists (yoneda_objects_ob C c). intros a b f g. unfold yoneda_objects_ob in *. simpl in *. exact (f ;; g). Defined. Lemma is_functor_yoneda_functor_data (C : precategory) (c : C) : is_functor (yoneda_ob_functor_data C c). Proof. repeat split; unf; simpl. intros. apply funextsec. intro f. unf. apply id_left. intros a b d f g. apply funextsec. intro h. apply (! assoc _ _ _ _ _ _ _ _ ). Qed. Definition yoneda_objects (C : precategory) (c : C) : functor C^op HSET := tpair _ _ (is_functor_yoneda_functor_data C c). (** ** On morphisms *) Definition yoneda_morphisms_data (C : precategory)(c c' : C) (f : hom C c c') : forall a : ob C^op, hom _ (yoneda_objects C c a) ( yoneda_objects C c' a) := fun a g => g ;; f. Lemma is_nat_trans_yoneda_morphisms_data (C : precategory) (c c' : ob C) (f : hom C c c') : is_nat_trans (yoneda_objects C c) (yoneda_objects C c') (yoneda_morphisms_data C c c' f). Proof. unfold is_nat_trans; simpl. unfold yoneda_morphisms_data; simpl. intros d d' g. apply funextsec; simpl in *. unfold yoneda_objects_ob; simpl. unf; intro; apply ( ! assoc _ _ _ _ _ _ _ _ ). Qed. Definition yoneda_morphisms (C : precategory) (c c' : C) (f : hom C c c') : nat_trans (yoneda_objects C c) (yoneda_objects C c') := tpair _ _ (is_nat_trans_yoneda_morphisms_data C c c' f). Definition yoneda_functor_data (C : precategory): functor_data C [C^op , HSET] := tpair _ (yoneda_objects C) (yoneda_morphisms C). (** ** Functorial properties of the yoneda assignments *) Lemma is_functor_yoneda (C : precategory) : is_functor (yoneda_functor_data C). Proof. unfold is_functor. repeat split; simpl. intro a; apply nat_trans_eq; simpl. unfold yoneda_morphisms_data, yoneda_objects_ob. intro c; apply funextsec; intro f. apply id_right. intros a b c f g. apply nat_trans_eq. unfold yoneda_morphisms_data, yoneda_objects_ob. simpl; intro d; apply funextsec; intro h. apply assoc. Qed. Definition yoneda (C : precategory) : functor C [C^op, HSET] := tpair _ _ (is_functor_yoneda C). (* Notation "'ob' F" := (precategory_ob_mor_fun_objects F)(at level 4). *) (** ** Yoneda lemma: natural transformations from [yoneda C c] to [F] are isomorphic to [F c] *) Definition yoneda_map_1 (C : precategory)(c : C) (F : functor C^op HSET) : hom _ (yoneda C c) F -> pr1(F c) := fun h => pr1 h c (identity c). Lemma yoneda_map_2_ax (C : precategory)(c : C) (F : functor C^op HSET) (x : pr1 (F c)) : is_nat_trans (pr1 (yoneda C c)) F (fun (d : C) (f : hom (C ^op) c d) => #F f x). Proof. intros a b f; simpl in *. apply funextsec. unfold yoneda_objects_ob; intro g. set (H:= @functor_comp _ _ F _ _ b g). unfold functor_comp in H; unfold opp_precat_data in H; simpl in *. apply (toforallpaths _ _ _ (H f) x). Qed. Definition yoneda_map_2 (C : precategory)(c : C) (F : functor C^op HSET) : pr1 (F c) -> hom _ (yoneda C c) F. Proof. intro x. exists (fun d : ob C => fun f => #F f x). apply yoneda_map_2_ax. Defined. Lemma yoneda_map_1_2 (C : precategory)(c : C) (F : functor C^op HSET) (alpha : hom _ (yoneda C c) F) : yoneda_map_2 _ _ _ (yoneda_map_1 _ _ _ alpha) == alpha. Proof. simpl in *; apply nat_trans_eq; intro a'; simpl. apply funextsec; intro f. unfold yoneda_map_1. pathvia ((alpha c ;; #F f) (identity c)). apply idpath. rewrite <- nat_trans_ax. unf; apply maponpaths. apply (id_right C a' c f ). Qed. Lemma yoneda_map_2_1 (C : precategory) (c : C) (F : functor C^op HSET) (x : pr1 (F c)) : yoneda_map_1 _ _ _ (yoneda_map_2 _ _ _ x) == x. Proof. simpl. rewrite (functor_id _ _ F). apply idpath. Qed. Lemma yoneda_iso_sets (C : precategory) (c : C) (F : functor C^op HSET) : is_isomorphism (C:=HSET) (a := hom _ ((yoneda C) c) F) (b := F c) (yoneda_map_1 C c F). Proof. exists (yoneda_map_2 C c F). repeat split; simpl. apply funextsec; intro alpha. unf; simpl. apply (yoneda_map_1_2 C c F). apply funextsec; intro x. unf; rewrite (functor_id _ _ F). apply idpath. Qed. (** ** The Yoneda embedding is fully faithful *) Lemma yoneda_fully_faithful (C : precategory) : fully_faithful (yoneda C). Proof. intros a b; simpl. set (H := yoneda_map_2 C b (yoneda C a)). set (H' := yoneda_map_2 C a (yoneda C b)). assert (eximio : yoneda_morphisms C a b == yoneda_map_2 C a (yoneda C b)). apply funextsec; intro f. apply nat_trans_eq; intro c; simpl. apply funextsec; intro g. apply idpath. rewrite eximio. apply (gradth _ (yoneda_map_1 C a (pr1 (yoneda C) b))). intro; apply yoneda_map_2_1. intro; apply yoneda_map_1_2. Qed.