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 : category) (c : C ^op)
(d : C) := C ⟦c ,d ⟧.

Definition covyoneda_ob_functor_data (C : category) (c : C ^op) :
functor_data C HSET.
Show proof.

exists (λ 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).

Lemma is_functor_covyoneda_functor_data (C : category) (c : C ^op) :
is_functor (covyoneda_ob_functor_data C c).
Show proof.

split.
- intros c'; apply funextfun; intro x; apply id_right.
- intros a b d f g; apply funextfun; intro h; apply assoc.

Definition covyoneda_objects (C : category) (c : C ^op) :
functor C HSET :=
tpair _ _ (is_functor_covyoneda_functor_data C c).

On morphisms

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 ⟧.
Show proof.

simpl in f; intros a g.
apply (f · g).

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).
Show proof.

intros d d' g; apply funextsec; intro h; apply assoc.

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).

Functorial properties of the yoneda assignments

Lemma is_functor_covyoneda (C : category) :
is_functor (covyoneda_functor_data C).
Show 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.

Definition covyoneda (C : category) :
functor C ^op [C , HSET , has_homsets_HSET ] :=
tpair _ _ (is_functor_covyoneda C).

TODO: adapt the rest?