Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.

Require Import UniMath.CategoryTheory.Categories.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.functor_categories.
Require Import UniMath.CategoryTheory.whiskering.

Ltac unf := unfold identity,
                   compose,
                   precategory_morphisms;
                   simpl.

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', hSetpair (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).

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

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