# Library UniMath.SubstitutionSystems.SubstitutionSystems

**********************************************************
Benedikt Ahrens, Ralph Matthes
SubstitutionSystems
2015
**********************************************************
Contents :
• Definition of heterogeneous substitution systems
• Various lemmas about the substitution ("bracket") operation
• Definition of precategory of substitution systems

## Some variables and assumptions

Assume having a precategory C whose hom-types are sets
Variable C : precategory.
Variable hs : has_homsets C.

Variable CP : BinCoproducts C.

Local Notation "'EndC'":= ([C, C, hs]) .
Let hsEndC : has_homsets EndC := functor_category_has_homsets C C hs.
Let CPEndC : BinCoproducts EndC := BinCoproducts_functor_precat _ _ CP hs.

Variable H : Signature C hs C hs C hs.

Let θ := theta H.

Let θ_strength1_int := Sig_strength_law1 _ _ _ _ _ _ H.
Let θ_strength2_int := Sig_strength_law2 _ _ _ _ _ _ H.

Let Id_H
: functor EndC EndC
:= BinCoproduct_of_functors _ _ CPEndC
(constant_functor _ _ (functor_identity _ : EndC))
H.

The precategory of pointed endofunctors on C
Local Notation "'Ptd'" := (precategory_Ptd C hs).
The category of endofunctors on C
Local Notation "'EndC'":= ([C, C, hs]) .

Definition eta_from_alg (T : algebra_ob Id_H) : EndC functor_identity _, `T .
Proof.
exact (BinCoproductIn1 _ (CPEndC _ _) · alg_map _ T).
Defined.

Local Notation η := eta_from_alg.

Definition ptd_from_alg (T : algebra_ob Id_H) : Ptd.
Proof.
(pr1 T).
exact (η T).
Defined.

Definition tau_from_alg (T : algebra_ob Id_H) : EndC H `T, `T.
Proof.
exact (BinCoproductIn2 _ (CPEndC _ _) · alg_map _ T).
Defined.
Local Notation τ := tau_from_alg.

Local Notation "'p' T" := (ptd_from_alg T) (at level 3).

Local Notation "f ⊕ g" := (BinCoproductOfArrows _ (CPEndC _ _ ) (CPEndC _ _ ) f g).

Definition bracket_property (T : algebra_ob Id_H) {Z : Ptd} (f : Z --> ptd_from_alg T)
(h : `T (U Z) --> `T) : UU
:=
alg_map _ T •• (U Z) · h =
(identity (U Z) θ (`T Z)) ·
(identity (U Z) #H h) ·
(BinCoproductArrow _ (CPEndC _ _ ) (#U f) (tau_from_alg T)).

Definition bracket_at (T : algebra_ob Id_H) {Z : Ptd} (f : Z --> ptd_from_alg T): UU :=
∃! h : `T (U Z) --> `T, bracket_property T f h.

Definition bracket (T : algebra_ob Id_H) : UU
:= (Z : Ptd) (f : Z --> ptd_from_alg T), bracket_at T f.

Lemma isaprop_bracket (T : algebra_ob Id_H) : isaprop (bracket T).
Proof.
apply impred_isaprop; intro Z.
apply impred_isaprop; intro f.
apply isapropiscontr.
Qed.

Definition bracket_property_parts (T : algebra_ob Id_H) {Z : Ptd} (f : Z --> ptd_from_alg T)
(h : `T (U Z) --> `T) : UU
:=
(#U f = η T •• (U Z) · h) ×
(θ (`T Z) · #H h · τ T = τ T •• (U Z) · h).

Definition bracket_parts_at (T : algebra_ob Id_H) {Z : Ptd} (f : Z --> ptd_from_alg T) : UU :=
∃! h : `T (U Z) --> `T, bracket_property_parts T f h.

Definition bracket_parts (T : algebra_ob Id_H) : UU
:= (Z : Ptd) (f : Z --> ptd_from_alg T), bracket_parts_at T f.

Lemma parts_from_whole (T : algebra_ob Id_H) (Z : Ptd) (f : Z --> ptd_from_alg T)
(h : `T (U Z) --> `T) :
bracket_property T f h bracket_property_parts T f h.
Proof.
intro Hyp.
split.
+ unfold eta_from_alg.
apply nat_trans_eq; try (exact hs).
intro c.
simpl.
unfold coproduct_nat_trans_in1_data.
assert (Hyp_inst := nat_trans_eq_pointwise Hyp c); clear Hyp.
apply (maponpaths (λ m, BinCoproductIn1 C (CP _ _)· m)) in Hyp_inst.
match goal with |[ H1 : _ = ?f |- _ = _ ] ⇒
intermediate_path (f) end.

× clear Hyp_inst.
rewrite <- assoc.
apply BinCoproductIn1Commutes_right_in_ctx_dir.
rewrite id_left.
apply BinCoproductIn1Commutes_right_in_ctx_dir.
rewrite id_left.
apply BinCoproductIn1Commutes_right_dir.
apply idpath.
× rewrite <- Hyp_inst; clear Hyp_inst.
rewrite <- assoc.
apply idpath.
+ unfold tau_from_alg.
apply nat_trans_eq; try (exact hs).
intro c.
simpl.
unfold coproduct_nat_trans_in2_data.
assert (Hyp_inst := nat_trans_eq_pointwise Hyp c); clear Hyp.
apply (maponpaths (λ m, BinCoproductIn2 C (CP _ _)· m)) in Hyp_inst.
match goal with |[ H1 : _ = ?f |- _ = _ ] ⇒
intermediate_path (f) end.

× clear Hyp_inst.
do 2 rewrite <- assoc.
apply BinCoproductIn2Commutes_right_in_ctx_dir.
simpl.
rewrite <- assoc.
apply maponpaths.
apply BinCoproductIn2Commutes_right_in_ctx_dir.
simpl.
rewrite <- assoc.
apply maponpaths.
unfold tau_from_alg.
apply BinCoproductIn2Commutes_right_dir.
apply idpath.
× rewrite <- Hyp_inst; clear Hyp_inst.
rewrite <- assoc.
apply idpath.
Qed.

Lemma whole_from_parts (T : algebra_ob Id_H) (Z : Ptd) (f : Z --> ptd_from_alg T)
(h : `T (U Z) --> `T) :
bracket_property_parts T f h bracket_property T f h.
Proof.
intros [Hyp1 Hyp2].
apply nat_trans_eq; try (exact hs).
intro c.
apply BinCoproductArrow_eq_cor.
+ clear Hyp2.
assert (Hyp1_inst := nat_trans_eq_pointwise Hyp1 c); clear Hyp1.
rewrite <- assoc.
apply BinCoproductIn1Commutes_right_in_ctx_dir.
rewrite id_left.
apply BinCoproductIn1Commutes_right_in_ctx_dir.
rewrite id_left.
apply BinCoproductIn1Commutes_right_dir.
simpl. simpl in Hyp1_inst.
rewrite Hyp1_inst.
simpl.
apply assoc.
+ clear Hyp1.
assert (Hyp2_inst := nat_trans_eq_pointwise Hyp2 c); clear Hyp2.
rewrite <- assoc.
apply BinCoproductIn2Commutes_right_in_ctx_dir.
simpl.
rewrite assoc.
eapply pathscomp0.
× eapply pathsinv0.
exact Hyp2_inst.
× clear Hyp2_inst.
simpl.
do 2 rewrite <- assoc.
apply maponpaths.
apply BinCoproductIn2Commutes_right_in_ctx_dir.
simpl.
rewrite <- assoc.
apply maponpaths.
apply BinCoproductIn2Commutes_right_dir.
apply idpath.
Qed.

Definition hss : UU := T, bracket T.

Coercion alg_from_hss (T : hss) : algebra_ob Id_H := pr1 T.

Definition fbracket (T : hss) {Z : Ptd} (f : Z --> ptd_from_alg T)
: `T (U Z) --> `T
:= pr1 (pr1 (pr2 T Z f)).

Notation "⦃ f ⦄" := (fbracket _ f)(at level 0).

The bracket operation fbracket is unique

Definition fbracket_unique_pointwise (T : hss) {Z : Ptd} (f : Z --> ptd_from_alg T)
: (α : functor_composite (U Z) `T pr1 `T),
( c : C, pr1 (#U f) c = pr1 (η T) (pr1 (U Z) c) · α c)
( c : C, pr1 (θ (`T Z)) c · pr1 (#H α) c · pr1 (τ T) c =
pr1 (τ T) (pr1 (U Z) c) · α c)

α = f.
Proof.
intros α H1 H2.
apply path_to_ctr.
apply whole_from_parts.
split.
- apply nat_trans_eq; try assumption.
- apply nat_trans_eq; assumption.
Qed.

Definition fbracket_unique (T : hss) {Z : Ptd} (f : Z --> ptd_from_alg T)
: α : `T (U Z) --> `T,
bracket_property_parts T f α

α = f.
Proof.
intros α [H1 H2].
apply path_to_ctr.
apply whole_from_parts.
split; assumption.
Qed.

Definition fbracket_unique_target_pointwise (T : hss) {Z : Ptd} (f : Z --> ptd_from_alg T)
: α : `T U Z --> `T,
bracket_property_parts T f α

c, pr1 α c = pr1 f c.
Proof.
intros α H12.
set (t:= fbracket_unique _ _ α H12).
apply (nat_trans_eq_weq hs _ _ t).
Qed.

Properties of fbracket by definition: commutative diagrams

Lemma fbracket_η (T : hss) : {Z : Ptd} (f : Z --> ptd_from_alg T),
#U f = η T •• U Z · f.
Proof.
intros Z f.
exact (pr1 (parts_from_whole _ _ _ _ (pr2 (pr1 (pr2 T Z f))))).
Qed.

Lemma fbracket_τ (T : hss) : {Z : Ptd} (f : Z --> ptd_from_alg T),
θ (`T Z) · #H f · τ T
=
τ T •• U Z · f.
Proof.
intros Z f.
exact (pr2 (parts_from_whole _ _ _ _ (pr2 (pr1 (pr2 T Z f))))).
Qed.

fbracket is also natural

Lemma fbracket_natural (T : hss) {Z Z' : Ptd} (f : Z --> Z') (g : Z' --> ptd_from_alg T)
: (` T # U f : EndC `T U Z , `T U Z' ) · g = f · g .
Proof.
apply fbracket_unique_pointwise.
- simpl. intro c.
rewrite assoc.
pose proof (nat_trans_ax (eta_from_alg T)) as H'.
simpl in H'.
rewrite <- H'; clear H'.
rewrite <- assoc.
apply maponpaths.
pose proof (nat_trans_eq_weq hs _ _ (fbracket_η T g)) as X.
simpl in X. exact (X _ ).
- intro c; simpl.
assert (H':=nat_trans_ax (tau_from_alg T)).
simpl in H'.
eapply pathscomp0. 2: apply (!assoc _ _ _ ).
eapply pathscomp0.
2: { apply cancel_postcomposition. apply H'. }
clear H'.
set (H':=fbracket_τ T g).
simpl in H'.
assert (X:= nat_trans_eq_pointwise H' c).
simpl in X.
rewrite <- assoc.
rewrite <- assoc.
transitivity ( # (pr1 (H ((`T)))) (pr1 (pr1 f) c) ·
(pr1 (θ ((`T) Z')) c pr1 (# H (fbracket T g)) c· pr1 (tau_from_alg T) c).
2: { rewrite <- assoc.
rewrite <- assoc.
apply maponpaths.
repeat rewrite assoc.
apply X.
}
clear X.
set (A:=θ_nat_2_pointwise).
simpl in ×.
set (A':= A _ hs _ hs _ hs H θ (`T) Z Z').
simpl in A'.
set (A2:= A' f).
clearbody A2; clear A'; clear A.
rewrite A2; clear A2.
repeat rewrite <- assoc.
apply maponpaths.
simpl.
repeat rewrite assoc.
apply cancel_postcomposition.
rewrite (functor_comp H).
apply cancel_postcomposition.
clear H'.
set (A:=horcomp_id_postwhisker C _ _ hs hs).
rewrite A.
apply idpath.
Qed.

As a consequence of naturality, we can compute fbracket f from fbracket identity

Lemma compute_fbracket (T : hss) : {Z : Ptd} (f : Z --> ptd_from_alg T),
f = (` T # U f : EndC `T U Z , `T U (p T) ) · identity p T .
Proof.
intros Z f.
assert (A : f = f · identity _ ).
{ rewrite id_right; apply idpath. }
rewrite A.
rewrite <- fbracket_natural.
rewrite id_right.
apply idpath.
Qed.

## Morphisms of heterogeneous substitution systems

A morphism f of pointed functors is an algebra morphism when...

a little preparation for much later
Lemma τ_part_of_alg_mor (T T' : @algebra_ob [C, C, hs] Id_H)
(β : @algebra_mor [C, C, hs] Id_H T T'): #H β · τ T' = compose (C:=EndC) (τ T) β.
Proof.
assert (β_is_alg_mor := pr2 β).
simpl in β_is_alg_mor.
assert (β_is_alg_mor_inst := maponpaths (fun m:EndC_,_(BinCoproductIn2 EndC (CPEndC _ _) m) β_is_alg_mor); clear β_is_alg_mor.
simpl in β_is_alg_mor_inst.
apply nat_trans_eq; try (exact hs).
intro c.
assert (β_is_alg_mor_inst':= nat_trans_eq_pointwise β_is_alg_mor_inst c); clear β_is_alg_mor_inst.
simpl in β_is_alg_mor_inst'.
rewrite assoc in β_is_alg_mor_inst'.
eapply pathscomp0.
2: { eapply pathsinv0.
exact β_is_alg_mor_inst'. }
clear β_is_alg_mor_inst'.
apply BinCoproductIn2Commutes_right_in_ctx_dir.
simpl.
rewrite <- assoc.
apply idpath.
Qed.

A morphism β of pointed functors is a bracket morphism when...

Lemma is_ptd_mor_alg_mor (T T' : @algebra_ob [C, C, hs] Id_H)
(β : @algebra_mor [C, C, hs] Id_H T T') :
@is_ptd_mor C (ptd_from_alg T) (ptd_from_alg T') (pr1 β).
Proof.
simpl.
unfold is_ptd_mor. simpl.
intro c.
rewrite <- assoc.
assert (X:=pr2 β).
assert (X':= nat_trans_eq_pointwise X c).
simpl in ×.
eapply pathscomp0. apply maponpaths. apply X'.
unfold coproduct_nat_trans_in1_data.
repeat rewrite assoc.
unfold coproduct_nat_trans_data.
eapply pathscomp0.
apply cancel_postcomposition.
apply BinCoproductIn1Commutes.
simpl.
repeat rewrite <- assoc.
apply id_left.
Qed.

Definition ptd_from_alg_mor {T T' : algebra_ob Id_H} (β : algebra_mor _ T T')
: ptd_from_alg T --> ptd_from_alg T'.
Proof.
(pr1 β).
apply is_ptd_mor_alg_mor.
Defined.

show functor laws for ptd_from_alg and ptd_from_alg_mor

Definition ptd_from_alg_functor_data : functor_data (precategory_FunctorAlg Id_H hsEndC) Ptd.
Proof.
ptd_from_alg.
intros T T' β.
apply ptd_from_alg_mor.
exact β.
Defined.

Lemma is_functor_ptd_from_alg_functor_data : is_functor ptd_from_alg_functor_data.
Proof.
split; simpl; intros.
+ unfold functor_idax.
intro T.
apply (invmap (eq_ptd_mor_precat _ hs _ _)).
apply (invmap (eq_ptd_mor _ hs _ _)).
apply idpath.
+ unfold functor_compax.
intros T T' T'' β β'.
apply (invmap (eq_ptd_mor_precat _ hs _ _)).
apply (invmap (eq_ptd_mor _ hs _ _)).
apply idpath.
Qed.

Definition ptd_from_alg_functor: functor (precategory_FunctorAlg Id_H hsEndC) Ptd :=
tpair _ _ is_functor_ptd_from_alg_functor_data.

Definition isbracketMor {T T' : hss} (β : algebra_mor _ T T') : UU :=
(Z : Ptd) (f : Z --> ptd_from_alg T),
f · β = β •• U Z · f · # ptd_from_alg_functor β .

Lemma isaprop_isbracketMor (T T':hss) (β : algebra_mor _ T T') : isaprop (isbracketMor β).
Proof.
do 2 (apply impred; intro).
apply isaset_nat_trans.
apply hs.
Qed.

A morphism of hss is a pointed morphism that is compatible with both τ and fbracket

Definition ishssMor {T T' : hss} (β : algebra_mor _ T T') : UU
:= isbracketMor β.

Definition hssMor (T T' : hss) : UU
:= β : algebra_mor _ T T', ishssMor β.

Coercion ptd_mor_from_hssMor (T T' : hss) (β : hssMor T T') : algebra_mor _ T T' := pr1 β.

Definition isbracketMor_hssMor {T T' : hss} (β : hssMor T T')
: isbracketMor β := pr2 β.

#### Equality of morphisms of hss

Section hssMor_equality.

Show that equality of hssMor is equality of underlying nat. transformations

Variables T T' : hss.
Variables β β' : hssMor T T'.
Definition hssMor_eq1 : β = β' (pr1 β = pr1 β').
Proof.
apply subtypeInjectivity.
intro γ.
apply isaprop_isbracketMor.
Defined.

Definition hssMor_eq : β = β' (β : EndC _ , _ ) = β'.
Proof.
eapply weqcomp.
- apply hssMor_eq1.
- apply subtypeInjectivity.
intro.
apply isaset_nat_trans.
apply hs.
Defined.

End hssMor_equality.

Lemma isaset_hssMor (T T' : hss) : isaset (hssMor T T').
Proof.
intros β β'.
apply (isofhlevelweqb _ (hssMor_eq _ _ β β')).
apply isaset_nat_trans.
apply hs.
Qed.

## The precategory of hss

### Identity morphism of hss

Lemma ishssMor_id (T : hss) : ishssMor (identity (C:=precategory_FunctorAlg _ hsEndC ) (pr1 T)).
Proof.
unfold ishssMor.
unfold isbracketMor.
intros Z f.
rewrite id_right.
rewrite functor_id.
rewrite id_right.
apply pathsinv0.
set (H2:=pre_composition_functor _ _ C _ hs (U Z)).
set (H2' := functor_id H2). simpl in H2'.
simpl.
rewrite H2'.
rewrite (@id_left EndC).
apply idpath.
Qed.

Definition hssMor_id (T : hss) : hssMor _ _ := tpair _ _ (ishssMor_id T).

### Composition of morphisms of hss

Lemma ishssMor_comp {T T' T'' : hss} (β : hssMor T T') (γ : hssMor T' T'')
: ishssMor (compose (C:=precategory_FunctorAlg _ hsEndC) (pr1 β) (pr1 γ)).
Proof.
unfold ishssMor.
unfold isbracketMor.
intros Z f.
eapply pathscomp0.
apply assoc.
eapply pathscomp0.
apply cancel_postcomposition.
apply isbracketMor_hssMor.
rewrite <- assoc.
eapply pathscomp0.
apply maponpaths.
apply isbracketMor_hssMor.
rewrite assoc.
rewrite functor_comp.
rewrite assoc.
apply cancel_postcomposition.
apply pathsinv0, (functor_comp (pre_composition_functor _ _ C _ hs (U Z)) ).
Qed.

Definition hssMor_comp {T T' T'' : hss} (β : hssMor T T') (γ : hssMor T' T'')
: hssMor T T'' := tpair _ _ (ishssMor_comp β γ).

Definition hss_obmor : precategory_ob_mor.
Proof.
hss.
exact hssMor.
Defined.

Definition hss_precategory_data : precategory_data.
Proof.
hss_obmor.
split.
- exact hssMor_id.
- exact @hssMor_comp.
Defined.

Lemma is_precategory_hss : is_precategory hss_precategory_data.
Proof.
repeat split; intros.
- apply (invmap (hssMor_eq _ _ _ _ )).
apply (@id_left EndC).
- apply (invmap (hssMor_eq _ _ _ _ )).
apply (@id_right EndC).
- apply (invmap (hssMor_eq _ _ _ _ )).
apply (@assoc EndC).
- apply (invmap (hssMor_eq _ _ _ _ )).
apply (@assoc' EndC).
Qed.

Definition hss_precategory : precategory := tpair _ _ is_precategory_hss.

End def_hss.

Arguments hss {_ _} _ _ .
Arguments hssMor {_ _ _ _ } _ _ .
Arguments fbracket {_ _ _ _ } _ {_} _ .
Arguments fbracket_η {_ _ _ _ } _ {_} _ .
Arguments fbracket_τ {_ _ _ _} _ {_} _ .
Arguments fbracket_unique_target_pointwise {_ _ _ _ } _ {_ _ _} _ _ .
Arguments fbracket_unique {_ _ _ _ } _ {_} _ _ _ .
Arguments hss_precategory {_ _} _ _ .
Arguments eta_from_alg {_ _ _ _} _.
Arguments tau_from_alg {_ _ _ _} _.
Arguments ptd_from_alg {_ _ _ _} _.
Arguments ptd_from_alg_functor {_ _} _ _ .
Arguments bracket_property {_ _ _ _ _ _} _ _ .
Arguments bracket_property_parts {_ _ _ _ _ _} _ _ .
Arguments bracket {_ _ _ _} _.

Notation τ := tau_from_alg.
Notation η := eta_from_alg.