# Library UniMath.SubstitutionSystems.SignatureCategory

Definition of the category of signatures with strength (Signature_precategory) with
Written by: Anders Mörtberg in October 2016 based on a note of Benedikt Ahrens.

# The category of signatures with strength

Section SignatureCategory.

Variables (C D D': category).

Let hsC : has_homsets C := homset_property C.
Let hsD : has_homsets D := homset_property D.
Let hsD' : has_homsets D' := homset_property D'.

Local Notation "'U'" := (functor_ptd_forget C hsC).
Local Notation "'Ptd'" := (precategory_Ptd C hsC).

Define the commutative diagram used in the morphisms
Section Signature_category_mor.

Variables (Ht Ht' : Signature C hsC D hsD D' hsD').

Let H := Signature_Functor _ _ _ _ _ _ Ht.
Let H' := Signature_Functor _ _ _ _ _ _ Ht'.
Let θ : nat_trans (θ_source Ht) (θ_target Ht) := theta Ht.
Let θ' : nat_trans (θ_source Ht') (θ_target Ht') := theta Ht'.

Variables (α : nat_trans H H').
Variables (X : [C,D']) (Y : Ptd).

Let f1 : [C,D] H X U Y,H (X U Y) := θ (X,,Y).
Let f2 : [C,D] H (X U Y),H' (X U Y) := α (X U Y).

Let g1 : [C,D] H X U Y,H' X U Y := α X ∙∙ identity (U Y).
Let g2 : [C,D] H' X U Y,H' (X U Y) := θ' (X,,Y).

Definition Signature_category_mor_diagram : UU := f1 · f2 = g1 · g2.

Special comparison lemma that speeds things up a lot
Lemma Signature_category_mor_diagram_pointwise
(Hc : c, pr1 f1 c · pr1 f2 c = pr1 (α X) ((pr1 Y) c) · pr1 g2 c) :
Signature_category_mor_diagram.
Proof.
apply (nat_trans_eq hsD); intro c; simpl.
rewrite functor_id, id_right; apply (Hc c).
Qed.

End Signature_category_mor.

Definition SignatureMor : Signature C hsC D hsD D' hsD' Signature C hsC D hsD D' hsD' UU.
Proof.
intros Ht Ht'.
use total2.
+ apply (nat_trans Ht Ht').
+ intros α; apply ( X Y, Signature_category_mor_diagram Ht Ht' α X Y).
Defined.

Lemma SignatureMor_eq (Ht Ht' : Signature C hsC D hsD D' hsD') (f g : SignatureMor Ht Ht') :
pr1 f = pr1 g f = g.
Proof.
intros H.
apply subtypePath; trivial.
now intros α; repeat (apply impred; intro); apply functor_category_has_homsets.
Qed.

Local Lemma SignatureMor_id_subproof (Ht : Signature C hsC D hsD D' hsD') X Y :
Signature_category_mor_diagram Ht Ht (nat_trans_id Ht) X Y.
Proof.
apply Signature_category_mor_diagram_pointwise; intro c; simpl.
now rewrite id_left, id_right.
Qed.

Definition SignatureMor_id (Ht : Signature C hsC D hsD D' hsD') : SignatureMor Ht Ht :=
(nat_trans_id Ht,,SignatureMor_id_subproof Ht).

Definition SignatureMor_comp_subproof (Ht1 Ht2 Ht3 : Signature C hsC D hsD D' hsD')
(α : SignatureMor Ht1 Ht2) (β : SignatureMor Ht2 Ht3) X Y :
Signature_category_mor_diagram Ht1 Ht3 (nat_trans_comp (pr1 α) (pr1 β)) X Y.
Proof.
destruct α as [α ]; destruct β as [β ].
unfold Signature_category_mor_diagram in *; simpl.
rewrite (assoc ((theta Ht1) (X,,Y))).
etrans; [apply (cancel_postcomposition ((theta Ht1) (X,,Y) · _)), |].
rewrite <- assoc; etrans; [apply maponpaths, |].
rewrite assoc; apply (cancel_postcomposition (C:=[C,D]) _ (_ ∙∙ identity (U Y))).
apply (nat_trans_eq hsD); intro c; simpl.
now rewrite assoc, !functor_id, !id_right.
Qed.

Definition SignatureMor_comp (Ht1 Ht2 Ht3 : Signature C hsC D hsD D' hsD')
(α : SignatureMor Ht1 Ht2) (β : SignatureMor Ht2 Ht3) : SignatureMor Ht1 Ht3 :=
(nat_trans_comp (pr1 α) (pr1 β),,SignatureMor_comp_subproof Ht1 Ht2 Ht3 α β).

Definition Signature_precategory_data : precategory_data.
Proof.
apply (tpair _ (Signature C hsC D hsD D' hsD',,SignatureMor)), (SignatureMor_id,,SignatureMor_comp).
Defined.

Lemma is_precategory_Signature_precategory_data :
is_precategory Signature_precategory_data.
Proof.
repeat split; simpl.
- intros Ht Ht' F; apply SignatureMor_eq; simpl.
apply (nat_trans_eq (functor_category_has_homsets _ _ hsD)); intros X; apply id_left.
- intros Ht Ht' F; apply SignatureMor_eq; simpl.
apply (nat_trans_eq (functor_category_has_homsets _ _ hsD)); intros X; apply id_right.
- intros Ht1 Ht2 Ht3 Ht4 F1 F2 F3; apply SignatureMor_eq; simpl.
apply (nat_trans_eq (functor_category_has_homsets _ _ hsD)); intros X; apply assoc.
- intros Ht1 Ht2 Ht3 Ht4 F1 F2 F3; apply SignatureMor_eq; simpl.
apply (nat_trans_eq (functor_category_has_homsets _ _ hsD)); intros X; apply assoc'.
Defined.

Definition Signature_precategory : precategory :=
(Signature_precategory_data,,is_precategory_Signature_precategory_data).

Lemma has_homsets_Signature_precategory : has_homsets Signature_precategory.
Proof.
intros Ht1 Ht2.
apply (isofhleveltotal2 2).
× apply isaset_nat_trans, functor_category_has_homsets.
× intros α.
apply isasetaprop.
apply impred; intros X; apply impred; intros Y.
apply functor_category_has_homsets.
Qed.

Definition SignatureForgetfulFunctor : functor Signature_precategory [[C,D'],[C,D]].
Proof.
use tpair.
- use tpair.
+ intros F; apply(Signature_Functor _ _ _ _ _ _ F).
+ intros F G α; apply α.
- abstract (now split).
Defined.

Lemma SignatureForgetfulFunctorFaithful : faithful SignatureForgetfulFunctor.
Proof.
intros F G.
apply isinclbetweensets.
+ apply has_homsets_Signature_precategory.
+ apply functor_category_has_homsets.
+ apply SignatureMor_eq.
Qed.

End SignatureCategory.

# Binary products in the category of signatures

Section BinProducts.

Variables (C : category) (BC : BinProducts C) (D : category) (BD : BinProducts D) (D' : category).

Let hsC : has_homsets C := homset_property C.
Let hsD : has_homsets D := homset_property D.
Let hsD' : has_homsets D' := homset_property D'.

Local Definition BCD : BinProducts [[C,D'],[C,D]].
Proof.
apply BinProducts_functor_precat, (BinProducts_functor_precat C _ BD).
Defined.

Local Lemma Signature_precategory_pr1_diagram (Ht1 Ht2 : Signature C hsC D hsD D' hsD') X Y :
Signature_category_mor_diagram _ _ _ (BinProduct_of_Signatures _ _ _ _ _ _ _ Ht1 Ht2) _
(BinProductPr1 _ (BCD _ _)) X Y.
Proof.
apply Signature_category_mor_diagram_pointwise; intro c; apply BinProductOfArrowsPr1.
Qed.

Local Definition Signature_precategory_pr1 (Ht1 Ht2 : Signature C hsC D hsD D' hsD') :
SignatureMor C D D' (BinProduct_of_Signatures C hsC D hsD D' hsD' BD Ht1 Ht2) Ht1.
Proof.
use tpair.
+ apply (BinProductPr1 _ (BCD (pr1 Ht1) (pr1 Ht2))).
+ cbn. apply Signature_precategory_pr1_diagram.
Defined.

Local Lemma Signature_precategory_pr2_diagram (Ht1 Ht2 : Signature C hsC D hsD D' hsD') X Y :
Signature_category_mor_diagram _ _ _ (BinProduct_of_Signatures _ _ _ _ _ _ _ Ht1 Ht2) _
(BinProductPr2 _ (BCD _ _)) X Y.
Proof.
apply Signature_category_mor_diagram_pointwise; intro c; apply BinProductOfArrowsPr2.
Qed.

Local Definition Signature_precategory_pr2 (Ht1 Ht2 : Signature C hsC D hsD D' hsD') :
SignatureMor C D D' (BinProduct_of_Signatures C hsC D hsD D' hsD' BD Ht1 Ht2) Ht2.
Proof.
use tpair.
+ apply (BinProductPr2 _ (BCD (pr1 Ht1) (pr1 Ht2))).
+ cbn. apply Signature_precategory_pr2_diagram.
Defined.

Local Lemma BinProductArrow_diagram Ht1 Ht2 Ht3
(F : SignatureMor C D D' Ht3 Ht1) (G : SignatureMor C D D' Ht3 Ht2) X Y :
Signature_category_mor_diagram _ _ _ _ (BinProduct_of_Signatures _ _ _ _ _ _ _ Ht1 Ht2)
(BinProductArrow _ (BCD _ _) (pr1 F) (pr1 G)) X Y.
Proof.
apply Signature_category_mor_diagram_pointwise; intro c.
apply pathsinv0.
etrans; [apply postcompWithBinProductArrow|].
apply pathsinv0, BinProductArrowUnique; rewrite <- assoc.
+ etrans; [apply maponpaths, BinProductPr1Commutes|].
etrans; [apply (nat_trans_eq_pointwise (pr2 F X Y) c)|].
now etrans; [apply cancel_postcomposition, horcomp_id_left|].
+ etrans; [apply maponpaths, BinProductPr2Commutes|].
etrans; [apply (nat_trans_eq_pointwise (pr2 G X Y) c)|].
now etrans; [apply cancel_postcomposition, horcomp_id_left|].
Qed.

Local Lemma isBinProduct_Signature_precategory (Ht1 Ht2 : Signature C hsC D hsD D' hsD') :
isBinProduct (Signature_precategory C D D') Ht1 Ht2
(BinProduct_of_Signatures C hsC D hsD D' hsD' BD Ht1 Ht2)
(Signature_precategory_pr1 Ht1 Ht2) (Signature_precategory_pr2 Ht1 Ht2).
Proof.
apply (make_isBinProduct _ (has_homsets_Signature_precategory C D D')).
simpl; intros Ht3 F G.
use unique_exists; simpl.
- apply (tpair _ (BinProductArrow _ (BCD (pr1 Ht1) (pr1 Ht2)) (pr1 F) (pr1 G))).
apply BinProductArrow_diagram.
- abstract (split;
[ apply SignatureMor_eq, (BinProductPr1Commutes _ _ _ (BCD _ _))
| apply SignatureMor_eq, (BinProductPr2Commutes _ _ _ (BCD _ _))]).
- abstract (intros X; apply isapropdirprod; apply has_homsets_Signature_precategory).
- abstract (intros X H1H2; apply SignatureMor_eq; simpl;
apply (BinProductArrowUnique _ _ _ (BCD _ _));
[ apply (maponpaths pr1 (pr1 H1H2)) | apply (maponpaths pr1 (pr2 H1H2)) ]).
Defined.

Lemma BinProducts_Signature_precategory : BinProducts (Signature_precategory C D D').
Proof.
intros Ht1 Ht2.
use make_BinProduct.
- apply (BinProduct_of_Signatures _ _ _ _ _ _ BD Ht1 Ht2).
- apply Signature_precategory_pr1.
- apply Signature_precategory_pr2.
- apply isBinProduct_Signature_precategory.
Defined.

End BinProducts.

# Coproducts in the category of signatures

Section Coproducts.

Variables (I : UU).
Variables (C D D' : category) (CD : Coproducts I D).

Let hsC : has_homsets C := homset_property C.
Let hsD : has_homsets D := homset_property D.
Let hsD' : has_homsets D' := homset_property D'.

Local Definition CCD : Coproducts I [[C,D'],[C,D]].
Proof.
now repeat apply Coproducts_functor_precat.
Defined.

Local Lemma Signature_precategory_in_diagram (Ht : I Signature_precategory C D D') i X Y :
Signature_category_mor_diagram _ _ _ _ (Sum_of_Signatures I C _ _ _ _ _ CD Ht)
(CoproductIn _ _ (CCD (λ j : I, pr1 (Ht j))) i) X Y.
Proof.
apply Signature_category_mor_diagram_pointwise; intro c.
apply pathsinv0.
set (C1 := CD (λ j, pr1 (pr1 (Ht j) X) ((pr1 Y) c))).
set (C2 := CD (λ j, pr1 (pr1 (Ht j) (functor_composite (pr1 Y) X)) c)).
apply (@CoproductOfArrowsIn I D _ C1 _ C2).
Defined.

Local Definition Signature_precategory_in (Ht : I Signature_precategory C D D') (i : I) :
SignatureMor C D D' (Ht i) (Sum_of_Signatures I C _ D _ D' _ CD Ht).
Proof.
use tpair.
+ apply (CoproductIn _ _ (CCD (λ j, pr1 (Ht j))) i).
+ cbn. apply Signature_precategory_in_diagram.
Defined.

Lemma CoproductArrow_diagram (Hti : I Signature_precategory C D D')
(Ht : Signature C hsC D hsD D' hsD') (F : i : I, SignatureMor C D D' (Hti i) Ht) X Y :
Signature_category_mor_diagram C D D' (Sum_of_Signatures I C hsC D hsD D' hsD' CD Hti) Ht
(CoproductArrow I _ (CCD _) (λ i, pr1 (F i))) X Y.
Proof.
apply Signature_category_mor_diagram_pointwise; intro c.
etrans; [apply precompWithCoproductArrow|].
apply pathsinv0, CoproductArrowUnique; intro i; rewrite assoc; simpl.
etrans;
[apply cancel_postcomposition, (CoproductInCommutes _ _ _ (CD (λ j, pr1 (pr1 (Hti j) X) _)))|].
apply pathsinv0; etrans; [apply (nat_trans_eq_pointwise (pr2 (F i) X Y) c)|].
now etrans; [apply cancel_postcomposition, horcomp_id_left|].
Qed.

Local Lemma isCoproduct_Signature_precategory (Hti : I Signature_precategory C D D') :
isCoproduct I (Signature_precategory C D D') _
(Sum_of_Signatures I C hsC D hsD D' hsD' CD Hti) (Signature_precategory_in Hti).
Proof.
apply (make_isCoproduct _ _ (has_homsets_Signature_precategory C D D')); simpl.
intros Ht F.
use unique_exists; simpl.
+ use tpair.
- apply (CoproductArrow I _ (CCD (λ j, pr1 (Hti j))) (λ i, pr1 (F i))).
- cbn. apply CoproductArrow_diagram.
+ abstract (intro i; apply SignatureMor_eq, (CoproductInCommutes _ _ _ (CCD (λ j, pr1 (Hti j))))).
+ abstract (intros X; apply impred; intro i; apply has_homsets_Signature_precategory).
+ abstract (intros X Hi; apply SignatureMor_eq; simpl;
apply (CoproductArrowUnique _ _ _ (CCD (λ j, pr1 (Hti j)))); intro i;
apply (maponpaths pr1 (Hi i))).
Defined.

Lemma Coproducts_Signature_precategory : Coproducts I (Signature_precategory C D D').
Proof.
intros Ht.
use make_Coproduct.
- apply (Sum_of_Signatures I _ _ _ _ _ _ CD Ht).
- apply Signature_precategory_in.
- apply isCoproduct_Signature_precategory.
Defined.

End Coproducts.