Library UniMath.CategoryTheory.covyoneda
**********************************************************
Benedikt Ahrens, Anders Mörtberg (adapted from yoneda.v)
2016
**********************************************************
Contents : Definition of the covariant Yoneda functor
covyoneda(C) : [C^op, [C, HSET]]
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Export UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Export UniMath.CategoryTheory.FunctorCategory.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.whiskering.
Ltac unf := unfold identity,
compose,
precategory_morphisms;
simpl.
The following lemma is already in precategories.v . It should be transparent?
Definition covyoneda_objects_ob (C : category) (c : C^op)
(d : C) := C⟦c,d⟧.
Definition covyoneda_ob_functor_data (C : category) (c : C^op) :
functor_data C HSET.
Proof.
∃ (λ c', make_hSet (covyoneda_objects_ob C c c') (homset_property C c c')) .
intros a b f g. unfold covyoneda_objects_ob in ×. simpl in ×.
exact (g · f).
Defined.
Lemma is_functor_covyoneda_functor_data (C : category) (c : C^op) :
is_functor (covyoneda_ob_functor_data C c).
Proof.
split.
- intros c'; apply funextfun; intro x; apply id_right.
- intros a b d f g; apply funextfun; intro h; apply assoc.
Qed.
Definition covyoneda_objects (C : category) (c : C^op) :
functor C HSET :=
tpair _ _ (is_functor_covyoneda_functor_data C c).
Definition covyoneda_morphisms_data (C : category) (c c' : C^op)
(f : C^op⟦c,c'⟧) : ∏ a : C,
HSET⟦covyoneda_objects C c a,covyoneda_objects C c' a⟧.
Proof.
simpl in f; intros a g.
apply (f · g).
Defined.
Lemma is_nat_trans_covyoneda_morphisms_data (C : category)
(c c' : C^op) (f : C^op⟦c,c'⟧) :
is_nat_trans (covyoneda_objects C c) (covyoneda_objects C c')
(covyoneda_morphisms_data C c c' f).
Proof.
intros d d' g; apply funextsec; intro h; apply assoc.
Qed.
Definition covyoneda_morphisms (C : category) (c c' : C^op)
(f : C^op⟦c,c'⟧) : nat_trans (covyoneda_objects C c) (covyoneda_objects C c') :=
tpair _ _ (is_nat_trans_covyoneda_morphisms_data C c c' f).
Definition covyoneda_functor_data (C : category) :
functor_data C^op [C,HSET,has_homsets_HSET] :=
tpair _ (covyoneda_objects C) (covyoneda_morphisms C).
Lemma is_functor_covyoneda (C : category) :
is_functor (covyoneda_functor_data C).
Proof.
split.
- intro a.
apply (@nat_trans_eq C _ has_homsets_HSET).
intro c; apply funextsec; intro f; simpl in ×.
apply id_left.
- intros a b c f g.
apply (@nat_trans_eq C _ has_homsets_HSET).
simpl; intro d; apply funextsec; intro h; apply pathsinv0, assoc.
Qed.
Definition covyoneda (C : category) :
functor C^op [C, HSET, has_homsets_HSET] :=
tpair _ _ (is_functor_covyoneda C).
TODO: adapt the rest?