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?

Covariant Yoneda functor

On objects

Definition covyoneda_objects_ob (C : precategory) (c : C ^op)
          (d : C) := C ⟦c ,d ⟧.

Definition covyoneda_ob_functor_data (C : precategory) (hs : has_homsets C) (c : C ^op) :
    functor_data C HSET.
Proof.
∃ (λ c', make_hSet (covyoneda_objects_ob C c c') (hs 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 : precategory) (hs: has_homsets C) (c : C ^op) :
  is_functor (covyoneda_ob_functor_data C hs 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 : precategory) (hs: has_homsets C) (c : C ^op) :
             functor C HSET :=
    tpair _ _ (is_functor_covyoneda_functor_data C hs c).

On morphisms

Definition covyoneda_morphisms_data (C : precategory) (hs: has_homsets C) (c c' : C ^op)
    (f : C ^op ⟦c ,c'⟧) : ∏ a : C ,
         HSET ⟦covyoneda_objects C hs c a ,covyoneda_objects C hs c' a ⟧.
Proof.
simpl in f; intros a g.
apply (f · g).
Defined.

Lemma is_nat_trans_covyoneda_morphisms_data (C : precategory) (hs: has_homsets C)
     (c c' : C ^op) (f : C ^op ⟦c ,c'⟧) :
  is_nat_trans (covyoneda_objects C hs c) (covyoneda_objects C hs c')
               (covyoneda_morphisms_data C hs c c' f).
Proof.
intros d d' g; apply funextsec; intro h; apply assoc.
Qed.

Definition covyoneda_morphisms (C : precategory) (hs: has_homsets C) (c c' : C ^op)
   (f : C ^op ⟦c ,c'⟧) : nat_trans (covyoneda_objects C hs c) (covyoneda_objects C hs c') :=
   tpair _ _ (is_nat_trans_covyoneda_morphisms_data C hs c c' f).

Definition covyoneda_functor_data (C : precategory) (hs : has_homsets C) :
   functor_data C ^op [C ,HSET ,has_homsets_HSET ] :=
   tpair _ (covyoneda_objects C hs) (covyoneda_morphisms C hs).

Functorial properties of the yoneda assignments

Lemma is_functor_covyoneda (C : precategory) (hs: has_homsets C):
  is_functor (covyoneda_functor_data C hs).
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 : precategory) (hs: has_homsets C) :
  functor C ^op [C , HSET , has_homsets_HSET ] :=
   tpair _ _ (is_functor_covyoneda C hs).

TODO: adapt the rest?