# Library UniMath.CategoryTheory.limits.FinOrdCoproducts

A direct definition of finite ordered coproducts by using coproducts
Definition of finite ordered coproducts.
Section def_FinOrdCoproducts.

Variable C : precategory.

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 : precategory.
Hypothesis hs : has_homsets C.

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 _ _ hs).
intros c g. use unique_exists.

apply (InitialArrow I c).
intros i. apply (fromempty (weqstn0toempty i)).
intros y. apply impred_isaprop. intros t. apply hs.
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 _ _ hs).
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 hs.

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

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

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.