Library UniMath.CategoryTheory.RepresentableFunctors.Test

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

Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.

Require Import UniMath.CategoryTheory.RepresentableFunctors.Representation.
Require UniMath.CategoryTheory.RepresentableFunctors.Precategories.

Section interface.

Variable C : category.

Definition isCoproductCocone (a b co : C) (ia : a --> co) (ib : b --> co) :=
  binarySumProperty ia ib.

Definition make_isCoproductCocone (a b co : C) (ia : a --> co) (ib : b --> co) :
   (∏ (c : C) (f : a --> c) (g : b --> c),
    ∃! k : C ⟦co, c⟧,
      ia · k = f ×
      ib · k = g)
   →
   isCoproductCocone a b co ia ib.
Proof.
  intros u c fg. refine (iscontrweqf _ (u c (pr1 fg) (pr2 fg))).
  apply weqfibtototal. intro d. apply weqiff.
  { split.
    { intros ee. apply dirprodeq.
      { simpl. exact (pr1 ee). }
      { simpl. exact (pr2 ee). } }
    { intros ee. split.
      { simpl. exact (maponpaths (HomPair_1 _ _ _) ee). }
      { simpl. exact (maponpaths (HomPair_2 _ _ _) ee). } } }
  { apply isapropdirprod; apply (homset_property C). }
  { apply setproperty. }
Defined.

Definition CoproductCocone (a b : C) := BinarySum a b.

Definition make_CoproductCocone (a b : C) :
  ∏ (c : C) (f : a --> c) (g : b --> c),
    isCoproductCocone _ _ _ f g → CoproductCocone a b
  := λ c f g i, c,,(f,,g),,i.

Definition Coproducts := BinarySums C.
Definition hasCoproducts (C:category) := ∏ (a b:C), ∥ BinarySum a b ∥.

Definition CoproductObject {a b : C} (CC : CoproductCocone a b) : C :=
  universalObject CC.

Definition CoproductIn1 {a b : C} (CC : CoproductCocone a b): a --> CoproductObject CC
  := in_1 CC.

Definition CoproductIn2 {a b : C} (CC : CoproductCocone a b) : b --> CoproductObject CC
  := in_2 CC.

Definition CoproductArrow {a b : C} (CC : CoproductCocone a b) {c : C} (f : a --> c) (g : b --> c) :
  CoproductObject CC --> c
  := binarySumMap CC f g.

Lemma CoproductIn1Commutes (a b : C) (CC : CoproductCocone a b):
     ∏ (c : C) (f : a --> c) g, CoproductIn1 CC · CoproductArrow CC f g = f.
Proof.
  intros c f g.
  exact (binarySum_in_1_eqn CC f g).
Qed.

Lemma CoproductIn2Commutes (a b : C) (CC : CoproductCocone a b):
     ∏ (c : C) (f : a --> c) g, CoproductIn2 CC · CoproductArrow CC f g = g.
Proof.
  intros c f g.
  exact (binarySum_in_2_eqn CC f g).
Qed.

Lemma CoproductArrowUnique (a b : C) (CC : CoproductCocone a b) (x : C)
    (f : a --> x) (g : b --> x) (k : CoproductObject CC --> x) :
    CoproductIn1 CC · k = f → CoproductIn2 CC · k = g →
      k = CoproductArrow CC f g.
Proof.
  intros u v.
  apply binarySumMapUniqueness.
  { refine (u @ _). apply pathsinv0, CoproductIn1Commutes. }
  { refine (v @ _). apply pathsinv0, CoproductIn2Commutes. }
Qed.

Lemma CoproductArrowEta (a b : C) (CC : CoproductCocone a b) (x : C)
    (f : CoproductObject CC --> x) :
    f = CoproductArrow CC (CoproductIn1 CC · f) (CoproductIn2 CC · f).
Proof.
  apply CoproductArrowUnique;
  apply idpath.
Qed.

Definition CoproductOfArrows {a b : C} (CCab : CoproductCocone a b) {c d : C}
    (CCcd : CoproductCocone c d) (f : a --> c) (g : b --> d) :
          CoproductObject CCab --> CoproductObject CCcd :=
    CoproductArrow CCab (f · CoproductIn1 CCcd) (g · CoproductIn2 CCcd).

Lemma CoproductOfArrowsIn1 {a b : C} (CCab : CoproductCocone a b) {c d : C}
    (CCcd : CoproductCocone c d) (f : a --> c) (g : b --> d) :
    CoproductIn1 CCab · CoproductOfArrows CCab CCcd f g = f · CoproductIn1 CCcd.
Proof.
  unfold CoproductOfArrows.
  apply CoproductIn1Commutes.
Qed.

Lemma CoproductOfArrowsIn2 {a b : C} (CCab : CoproductCocone a b) {c d : C}
    (CCcd : CoproductCocone c d) (f : a --> c) (g : b --> d) :
    CoproductIn2 CCab · CoproductOfArrows CCab CCcd f g = g · CoproductIn2 CCcd.
Proof.
  unfold CoproductOfArrows.
  apply CoproductIn2Commutes.
Qed.

Lemma precompWithCoproductArrow {a b : C} (CCab : CoproductCocone a b) {c d : C}
    (CCcd : CoproductCocone c d) (f : a --> c) (g : b --> d)
    {x : C} (k : c --> x) (h : d --> x) :
        CoproductOfArrows CCab CCcd f g · CoproductArrow CCcd k h =
         CoproductArrow CCab (f · k) (g · h).
Proof.
  apply CoproductArrowUnique.
  - rewrite assoc. rewrite CoproductOfArrowsIn1.
    rewrite <- assoc, CoproductIn1Commutes.
    apply idpath.
  - rewrite assoc, CoproductOfArrowsIn2.
    rewrite <- assoc, CoproductIn2Commutes.
    apply idpath.
Qed.

Lemma postcompWithCoproductArrow {a b : C} (CCab : CoproductCocone a b) {c : C}
    (f : a --> c) (g : b --> c) {x : C} (k : c --> x) :
       CoproductArrow CCab f g · k = CoproductArrow CCab (f · k) (g · k).
Proof.
  apply CoproductArrowUnique.
  - rewrite assoc, CoproductIn1Commutes;
     apply idpath.
  - rewrite assoc, CoproductIn2Commutes;
     apply idpath.
Qed.

Section coproduct_unique.

Hypothesis H : is_univalent C.

Variables a b : C.

Definition from_Coproduct_to_Coproduct (CC CC' : CoproductCocone a b)
  : CoproductObject CC --> CoproductObject CC'.
Proof.
  apply (CoproductArrow CC (CoproductIn1 _ ) (CoproductIn2 _ )).
Defined.

Lemma Coproduct_endo_is_identity (CC : CoproductCocone a b)
  (k : CoproductObject CC --> CoproductObject CC)
  (H1 : CoproductIn1 CC · k = CoproductIn1 CC)
  (H2 : CoproductIn2 CC · k = CoproductIn2 CC)
  : identity _ = k.
Proof.
Abort.

End coproduct_unique.

End interface.

Section def_functor_pointwise_coprod.

Variable C D : category.
Variable HD : Coproducts D.

Definition hsD := homset_property D.

Section coproduct_functor.

Variables F G : functor C D.

Definition Coproducts_functor_precat : Coproducts (functor_category C D).
Proof.
  apply functorBinarySum.
  exact HD.
Defined.

Definition coproduct_functor : functor C D := universalObject (functorBinarySum HD F G).

End coproduct_functor.
End def_functor_pointwise_coprod.