Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.OppositeCategory.Core.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.Categories.HSET.Core.
Require Import UniMath.CategoryTheory.Categories.HSET.Univalence.
Require Import UniMath.CategoryTheory.Categories.HSET.Colimits.
Require Import UniMath.CategoryTheory.Profunctors.Core.
Require Import UniMath.CategoryTheory.Limits.Coends.
Require Import UniMath.CategoryTheory.Limits.Coproducts.
Require Import UniMath.CategoryTheory.Limits.Coequalizers.

Local Open Scope cat.

Section CoendsHSET.
  Context {C : category}
          (F : profunctor C C).

  Definition HSET_coend_colimit
    : coend_colimit F
    := construction_of_coends
         F
         Coequalizers_HSET
         (CoproductsHSET_type _) (CoproductsHSET_type _).

  Definition HSET_coend
    : hSet
    := HSET_coend_colimit : HSET.

  Definition HSET_coend_in
             (x : C)
             (h : F x x)
    : HSET_coend
    := mor_of_cowedge _ HSET_coend_colimit x h.

  Proposition HSET_coend_comm
              {x y : C}
              (f : x --> y)
              (h : F y x)
    : HSET_coend_in y (rmap F f h)
      =
      HSET_coend_in x (lmap F f h).
  Proof.
    exact (eqtohomot (eq_of_cowedge _ HSET_coend_colimit f) h).
  Qed.

  Section MorToCoend.
    Context (X : hSet)
            (fs : ∏ (x : C), F x x → X)
            (ps : ∏ (x y : C)
                    (f : x --> y)
                    (h : F y x),
                  fs _ (rmap F f h)
                  =
                  fs _ (lmap F f h)).

    Definition mor_from_HSET_coend
               (x : HSET_coend)
      : X.
    Proof.
      refine (mor_to_coend' _ (pr2 HSET_coend_colimit) X fs _ x).
      abstract
        (intros y₁ y₂ g ;
         use funextsec ; intro h ;
         apply ps).
    Defined.

    Definition mor_from_HSET_coend_comm
               {x : C}
               (h : F x x)
      : mor_from_HSET_coend (HSET_coend_in x h)
        =
        fs x h.
    Proof.
      refine (eqtohomot (mor_to_coend'_comm _ (pr2 HSET_coend_colimit) X fs _ x) h).
      abstract
        (intros y₁ y₂ g ;
         use funextsec ; intro ;
         apply ps).
    Qed.
  End MorToCoend.

  Proposition mor_from_HSET_coend_eq
              (X : hSet)
              (f g : HSET_coend → X)
              (x : HSET_coend)
              (p : ∏ (y : C)
                     (h : F y y),
                   f (HSET_coend_in y h) = g (HSET_coend_in y h))
    : f x = g x.
  Proof.
    use (eqtohomot (mor_to_coend_eq F (pr2 HSET_coend_colimit) X _)).
    intro y.
    use funextsec.
    intro h.
    apply p.
  Qed.
End CoendsHSET.

#[global] Opaque HSET_coend HSET_coend_in mor_from_HSET_coend.