Library UniMath.CategoryTheory.limits.FinOrdCoproducts

A direct definition of finite ordered coproducts by using coproducts
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.

Require Import UniMath.Combinatorics.StandardFiniteSets.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.ProductCategory.
Require Import UniMath.CategoryTheory.limits.coproducts.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Require Import UniMath.CategoryTheory.limits.initial.

Local Open Scope cat.

Definition of finite ordered coproducts.
Section def_FinOrdCoproducts.

  Variable C : category.

  Definition FinOrdCoproducts : UU :=
    ∏ (n : nat) (a : stn n → C), Coproduct (stn n) C a.
  Definition hasFinOrdCoproducts : UU :=
    ∏ (n : nat) (a : stn n → C), ∥ Coproduct (stn n) C a ∥.

End def_FinOrdCoproducts.

Construction of FinOrdCoproducts from Initial and BinCoproducts.
Section FinOrdCoproduct_criteria.

  Variable C : category.

Case n = 0 of the theorem.
  Lemma InitialToCoproduct (I : Initial C):
    ∏ (a : stn 0 → C), Coproduct (stn 0) C a.
  Proof.
    intros a.
    use (make_Coproduct _ _ _ I
                            (λ i : stn 0, fromempty (weqstn0toempty i))).
    use (make_isCoproduct _ _ C).
    intros c g. use unique_exists.

    apply (InitialArrow I c).
    intros i. apply (fromempty (weqstn0toempty i)).
    intros y. apply impred_isaprop. intros t. apply C.
    intros y X. apply InitialArrowUnique.
  Defined.

Case n = 1 of the theorem.
  Lemma ObjectToCoproduct:
    ∏ (a : stn 1 → C), Coproduct (stn 1) C a.
  Proof.
    intros a.
    set (stn1ob := invweq(weqstn1tounit) tt).
    use (make_Coproduct _ _ _ (a stn1ob)).
    intros i. exact (idtoiso (! (maponpaths a (isconnectedstn1 stn1ob i)))).

    use (make_isCoproduct _ _ C).
    intros c g.
    use (unique_exists (g stn1ob)).

    intros i. rewrite <- (isconnectedstn1 stn1ob i). apply id_left.

    intros y. apply impred_isaprop. intros t. apply C.

    intros y X. rewrite <- (X stn1ob). apply pathsinv0. apply id_left.
  Defined.

Finite ordered coproducts from initial and binary coproducts.
  Theorem FinOrdCoproducts_from_Initial_and_BinCoproducts :
    Initial C → BinCoproducts C → FinOrdCoproducts C.
  Proof.
    intros I BinCoprods. unfold FinOrdCoproducts. intros n. induction n as [|n IHn].

    apply (InitialToCoproduct I).

    intros a.
    set (a1 := λ (i : stn n), a (dni_lastelement i)).
    set (Cone1 := IHn a1).
    set (a2 := (λ _ : stn 1, a lastelement)).
    set (Cone2 := ObjectToCoproduct a2).     set (Cone1In := CoproductIn _ _ Cone1).
    set (Cone2In := CoproductIn _ _ Cone2).
    set (BinCone := BinCoprods (CoproductObject (stn n) C Cone1)
                               (CoproductObject (stn 1) C Cone2)).
    set (in1 := BinCoproductIn1 BinCone).
    set (in2 := BinCoproductIn2 BinCone).
    set (m1 := λ i1 : stn n, (Cone1In i1) · in1).
    set (m2 := λ i2 : stn 1, (Cone2In i2) · in2).

    use (make_Coproduct (stn (S n)) C a (BinCoproductObject BinCone) _).

    intros i. induction (natlehchoice4 (pr1 i) _ (pr2 i)) as [a0|b].
    exact (idtoiso (maponpaths a (dni_lastelement_eq n i a0))
                   · m1 (make_stn n (pr1 i) a0)).
    exact (idtoiso (maponpaths a (lastelement_eq n i b))
                   · m2 (invweq(weqstn1tounit) tt)).

    use (make_isCoproduct _ _ C).

    intros c g.
    set (g1 := λ i : stn n, g(dni_lastelement i)).
    set (ar1 := CoproductArrow _ _ Cone1 g1).
    set (com1 := BinCoproductIn1Commutes _ _ _ BinCone c ar1
                                          (g lastelement)).
    set (com2 := BinCoproductIn2Commutes _ _ _ BinCone c ar1
                                         (g lastelement)).
    set (com3 := CoproductInCommutes _ _ _ Cone1 _ g1).
    set (com4 := CoproductInCommutes _ _ _ Cone2 _
                                     (λ _ : stn 1, g lastelement)).

    use (unique_exists).

    use (BinCoproductArrow BinCone).
    use (CoproductArrow _ _ Cone1). intros i. exact (g (dni_lastelement i)).
    use (CoproductArrow _ _ Cone2). intros i. exact (g lastelement).

    intros i. unfold coprod_rect. induction (natlehchoice4 (pr1 i) n (pr2 i)) as [a0|b].
    rewrite (dni_lastelement_eq n i a0). repeat rewrite <- assoc.
    apply remove_id_left. apply idpath.

    unfold m1. unfold in1. rewrite <- assoc. fold g1. fold ar1.
    use (pathscomp0 (maponpaths (λ f : _, Cone1In (make_stn n (pr1 i) a0) · f)
                                com1)).
    fold ar1 in com3. rewrite com3. unfold g1. apply idpath.

    rewrite (lastelement_eq n i b). repeat rewrite <- assoc.
    apply remove_id_left. apply idpath.

    unfold m2. unfold in2. rewrite <- assoc. fold g1. fold ar1.
    use (pathscomp0 (maponpaths (λ f : _, Cone2In lastelement · f) com2)).
    rewrite com4. apply idpath.

    intros y. apply impred_isaprop. intros t. apply C.

    unfold coprod_rect. intros k X.
    apply BinCoproductArrowUnique.

    apply CoproductArrowUnique.
    intros i. rewrite <- (X (dni_lastelement i)). rewrite assoc.
    apply cancel_postcomposition.
    induction (natlehchoice4 (pr1 (dni_lastelement i)) n
                             (pr2 (dni_lastelement i))) as [a0|b].
    unfold m1. rewrite assoc. unfold in1.
    apply cancel_postcomposition.
    unfold Cone1In. apply pathsinv0.

    set (e := dni_lastelement_is_inj (dni_lastelement_eq n (dni_lastelement i)
                                                         a0)).
    use (pathscomp0 _ (CoproductIn_idtoiso (stn n) C (a ∘ dni_lastelement)%functions Cone1
                                           e)).
    apply cancel_postcomposition.
    apply maponpaths. apply maponpaths.     rewrite <- (maponpathscomp _ a).
    apply maponpaths. apply isasetstn.

    apply fromempty. induction i as [i i'].
    cbn in b. induction (!b).
    apply (isirreflnatlth _ i').

    apply CoproductArrowUnique.
    intros i. rewrite <- (X lastelement). rewrite assoc.
    apply cancel_postcomposition.
    induction (natlehchoice4 (pr1 lastelement) n (pr2 lastelement)) as [a0|b].

    apply fromempty. cbn in a0. apply (isirreflnatlth _ a0).

    apply pathsinv0. unfold m2. rewrite assoc. unfold in2.
    apply cancel_postcomposition. unfold Cone2In.

    set (e := isconnectedstn1 i (invweq(weqstn1tounit) tt)).
    use (pathscomp0 _ (CoproductIn_idtoiso (stn 1) C
                                           (λ _ : _, a lastelement)
                                           Cone2 e)).
    apply cancel_postcomposition.
    apply maponpaths. apply maponpaths.     fold (@funcomp (stn 1) _ _ (λ _ : stn 1, lastelement) a).
    rewrite <- (maponpathscomp (λ _ : stn 1, lastelement) a).
    apply maponpaths. apply isasetstn.
  Defined.

End FinOrdCoproduct_criteria.