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
Require Import UniMath.Foundations.PartD.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.FunctorCategory.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.FunctorAlgebras.
Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
Require Import UniMath.CategoryTheory.PointedFunctors.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.HorizontalComposition.
Require Import UniMath.CategoryTheory.PointedFunctorsComposition.
Require Import UniMath.SubstitutionSystems.Signatures.
Require Import UniMath.SubstitutionSystems.Notation.
Local Open Scope subsys.
Section fix_a_category.
Context (C : category) (CP : BinCoproducts C).
Local Notation "'EndC'":= ([C, C]) .
Let CPEndC : BinCoproducts EndC := BinCoproducts_functor_precat _ _ CP.
The category of pointed endofunctors on C
The category of endofunctors on C
preparations for the definition of hss based on a functor H
Section prep_hss.
Context (H : functor [C, C] [C, C]).
Definition Const_plus_H (X : EndC) : functor EndC EndC
:= BinCoproduct_of_functors _ _ CPEndC (constant_functor _ _ X) H.
Definition Id_H : functor EndC EndC
:= Const_plus_H (functor_identity _ : EndC).
Definition eta_from_alg {X : EndC} (T : algebra_ob (Const_plus_H X)) : EndC ⟦ X , `T ⟧.
Show proof.
Local Notation η := eta_from_alg.
Definition ptd_from_alg (T : algebra_ob Id_H) : Ptd.
Show proof.
Definition tau_from_alg {X : EndC} (T : algebra_ob (Const_plus_H X)) : EndC ⟦H `T, `T⟧.
Show proof.
Local Notation τ := tau_from_alg.
Local Notation "f ⊕ g" := (BinCoproductOfArrows _ (CPEndC _ _ ) (CPEndC _ _ ) f g).
Context (H : functor [C, C] [C, C]).
Definition Const_plus_H (X : EndC) : functor EndC EndC
:= BinCoproduct_of_functors _ _ CPEndC (constant_functor _ _ X) H.
Definition Id_H : functor EndC EndC
:= Const_plus_H (functor_identity _ : EndC).
Definition eta_from_alg {X : EndC} (T : algebra_ob (Const_plus_H X)) : EndC ⟦ X , `T ⟧.
Show proof.
Local Notation η := eta_from_alg.
Definition ptd_from_alg (T : algebra_ob Id_H) : Ptd.
Show proof.
Definition tau_from_alg {X : EndC} (T : algebra_ob (Const_plus_H X)) : EndC ⟦H `T, `T⟧.
Show proof.
Local Notation τ := tau_from_alg.
Local Notation "f ⊕ g" := (BinCoproductOfArrows _ (CPEndC _ _ ) (CPEndC _ _ ) f g).
analysis of the "bracket operation" individually for each pointed functor
Section fix_a_pointed_functor.
Context {Z: Ptd}.
Context (θ : @PrestrengthForSignatureAtPoint C C C H Z).
Definition bracket_property (T : algebra_ob Id_H) (f : Z --> ptd_from_alg T)
(h : `T • (U Z) --> `T) : UU
:=
alg_map _ T •• (U Z) · h =
(identity (U Z) ⊕ θ `T) ·
(identity (U Z) ⊕ #H h) ·
(BinCoproductArrow (CPEndC _ _ ) (#U f) (tau_from_alg T)).
Definition bracket_at (T : algebra_ob Id_H) (f : Z --> ptd_from_alg T): UU :=
∃! h : `T • (U Z) --> `T, bracket_property T f h.
Definition bracket_property_parts (T : algebra_ob Id_H) (f : Z --> ptd_from_alg T)
(h : `T • (U Z) --> `T) : UU
:=
(#U f = η T •• (U Z) · h) ×
(θ `T · #H h · τ T = τ T •• (U Z) · h).
Definition bracket_parts_at (T : algebra_ob Id_H) (f : Z --> ptd_from_alg T) : UU :=
∃! h : `T • (U Z) --> `T, bracket_property_parts T f h.
Lemma parts_from_whole (T : algebra_ob Id_H) (f : Z --> ptd_from_alg T)
(h : `T • (U Z) --> `T) :
bracket_property T f h → bracket_property_parts T f h.
Show proof.
Lemma whole_from_parts (T : algebra_ob Id_H) (f : Z --> ptd_from_alg T)
(h : `T • (U Z) --> `T) :
bracket_property_parts T f h → bracket_property T f h.
Show proof.
End fix_a_pointed_functor.
Section instantiate_with_identity.
Context (T : algebra_ob Id_H).
Context (θ : @PrestrengthForSignatureAtPoint C C C H (ptd_from_alg T)).
Definition bracket_property_parts_identity_nicer (h : `T • `T --> `T) : UU
:= (identity `T = η T •• `T · h) × (θ `T · #H h · τ T = τ T •• `T · h).
Lemma bracket_property_parts_identity_nicer_impl1 (h : `T • `T --> `T):
bracket_property_parts θ T (identity _) h -> bracket_property_parts_identity_nicer h.
Show proof.
Context {Z: Ptd}.
Context (θ : @PrestrengthForSignatureAtPoint C C C H Z).
Definition bracket_property (T : algebra_ob Id_H) (f : Z --> ptd_from_alg T)
(h : `T • (U Z) --> `T) : UU
:=
alg_map _ T •• (U Z) · h =
(identity (U Z) ⊕ θ `T) ·
(identity (U Z) ⊕ #H h) ·
(BinCoproductArrow (CPEndC _ _ ) (#U f) (tau_from_alg T)).
Definition bracket_at (T : algebra_ob Id_H) (f : Z --> ptd_from_alg T): UU :=
∃! h : `T • (U Z) --> `T, bracket_property T f h.
Definition bracket_property_parts (T : algebra_ob Id_H) (f : Z --> ptd_from_alg T)
(h : `T • (U Z) --> `T) : UU
:=
(#U f = η T •• (U Z) · h) ×
(θ `T · #H h · τ T = τ T •• (U Z) · h).
Definition bracket_parts_at (T : algebra_ob Id_H) (f : Z --> ptd_from_alg T) : UU :=
∃! h : `T • (U Z) --> `T, bracket_property_parts T f h.
Lemma parts_from_whole (T : algebra_ob Id_H) (f : Z --> ptd_from_alg T)
(h : `T • (U Z) --> `T) :
bracket_property T f h → bracket_property_parts T f h.
Show proof.
intro Hyp.
split.
+ unfold eta_from_alg.
apply nat_trans_eq_alt.
intro c.
simpl.
unfold coproduct_nat_trans_in1_data.
assert (Hyp_inst := nat_trans_eq_pointwise Hyp c); clear Hyp.
apply (maponpaths (λ m, BinCoproductIn1 (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_alt.
intro c.
simpl.
unfold coproduct_nat_trans_in2_data.
assert (Hyp_inst := nat_trans_eq_pointwise Hyp c); clear Hyp.
apply (maponpaths (λ m, BinCoproductIn2 (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.
split.
+ unfold eta_from_alg.
apply nat_trans_eq_alt.
intro c.
simpl.
unfold coproduct_nat_trans_in1_data.
assert (Hyp_inst := nat_trans_eq_pointwise Hyp c); clear Hyp.
apply (maponpaths (λ m, BinCoproductIn1 (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_alt.
intro c.
simpl.
unfold coproduct_nat_trans_in2_data.
assert (Hyp_inst := nat_trans_eq_pointwise Hyp c); clear Hyp.
apply (maponpaths (λ m, BinCoproductIn2 (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.
Lemma whole_from_parts (T : algebra_ob Id_H) (f : Z --> ptd_from_alg T)
(h : `T • (U Z) --> `T) :
bracket_property_parts T f h → bracket_property T f h.
Show proof.
intros [Hyp1 Hyp2].
apply nat_trans_eq_alt.
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.
apply nat_trans_eq_alt.
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.
End fix_a_pointed_functor.
Section instantiate_with_identity.
Context (T : algebra_ob Id_H).
Context (θ : @PrestrengthForSignatureAtPoint C C C H (ptd_from_alg T)).
Definition bracket_property_parts_identity_nicer (h : `T • `T --> `T) : UU
:= (identity `T = η T •• `T · h) × (θ `T · #H h · τ T = τ T •• `T · h).
Lemma bracket_property_parts_identity_nicer_impl1 (h : `T • `T --> `T):
bracket_property_parts θ T (identity _) h -> bracket_property_parts_identity_nicer h.
Show proof.
intro Hyp. induction Hyp as [Hyp1 Hyp2].
split.
- etrans.
2: { exact Hyp1. }
apply nat_trans_eq_alt.
intro c.
apply idpath.
- etrans.
{ exact Hyp2. }
apply idpath.
split.
- etrans.
2: { exact Hyp1. }
apply nat_trans_eq_alt.
intro c.
apply idpath.
- etrans.
{ exact Hyp2. }
apply idpath.
basically the same proof
Lemma bracket_property_parts_identity_nicer_impl2 (h : `T • `T --> `T):
bracket_property_parts_identity_nicer h -> bracket_property_parts θ T (identity _) h.
intro Hyp. induction Hyp as [Hyp1 Hyp2].
split.
- etrans.
2: { exact Hyp1. }
apply nat_trans_eq_alt.
intro c.
apply idpath.
- etrans.
{ exact Hyp2. }
apply idpath.
Qed.
End instantiate_with_identity.
bracket_property_parts_identity_nicer h -> bracket_property_parts θ T (identity _) h.
intro Hyp. induction Hyp as [Hyp1 Hyp2].
split.
- etrans.
2: { exact Hyp1. }
apply nat_trans_eq_alt.
intro c.
apply idpath.
- etrans.
{ exact Hyp2. }
apply idpath.
Qed.
End instantiate_with_identity.
the notion one would be looking for: an algebra and a substitution operation that does lookup on
variables and behaves homomorphically elsewhere, as instructed by the pre-strength at that point
Definition heterogeneous_substitution : UU := ∑ (T: algebra_ob Id_H),
∑ (θ : @PrestrengthForSignatureAtPoint C C C H (ptd_from_alg T)), bracket_at θ T (identity _).
Coercion alg_from_hetsubst (T : heterogeneous_substitution) : algebra_ob Id_H := pr1 T.
Definition θ_from_hetsubst (T : heterogeneous_substitution) : @PrestrengthForSignatureAtPoint C C C H (ptd_from_alg T)
:= pr1 (pr2 T).
∑ (θ : @PrestrengthForSignatureAtPoint C C C H (ptd_from_alg T)), bracket_at θ T (identity _).
Coercion alg_from_hetsubst (T : heterogeneous_substitution) : algebra_ob Id_H := pr1 T.
Definition θ_from_hetsubst (T : heterogeneous_substitution) : @PrestrengthForSignatureAtPoint C C C H (ptd_from_alg T)
:= pr1 (pr2 T).
we write prejoin as a warning that the monad laws are not necessarily fulfilled
Definition prejoin_from_hetsubst (T : heterogeneous_substitution) : `T • `T --> `T
:= pr1 (pr1 (pr2 (pr2 T))).
Lemma prejoin_from_hetsubst_η (T : heterogeneous_substitution) :
identity `T = η T •• `T · (prejoin_from_hetsubst T).
Show proof.
Lemma prejoin_from_hetsubst_τ (T : heterogeneous_substitution) :
θ_from_hetsubst T `T · #H (prejoin_from_hetsubst T) · τ T = τ T •• `T · (prejoin_from_hetsubst T).
Show proof.
Section fix_a_prestrength.
Context (θ : @PrestrengthForSignature C C C H).
Definition bracket (T : algebra_ob Id_H) : UU
:= ∏ (Z : Ptd) (f : Z --> ptd_from_alg T), bracket_at (nat_trans_fix_snd_arg _ _ _ _ _ θ Z) T f.
Lemma isaprop_bracket (T : algebra_ob Id_H) : isaprop (bracket T).
Show proof.
Definition bracket_parts (T : algebra_ob Id_H) : UU
:= ∏ (Z : Ptd) (f : Z --> ptd_from_alg T), bracket_parts_at (nat_trans_fix_snd_arg _ _ _ _ _ θ Z) T f.
End fix_a_prestrength.
End prep_hss.
Arguments ptd_from_alg {_} _ .
Arguments prejoin_from_hetsubst {_} _ .
Arguments prejoin_from_hetsubst_η {_} _ .
Arguments prejoin_from_hetsubst_τ {_} _ .
Arguments bracket_parts {_} _ _ .
Section def_hss.
Context (H : Presignature C C C).
Local Notation η := (eta_from_alg H).
Local Notation τ := (tau_from_alg H).
Let θ : PrestrengthForSignature H := theta H.
Let Id_H : [C, C] ⟶ [C, C] := Id_H H.
:= pr1 (pr1 (pr2 (pr2 T))).
Lemma prejoin_from_hetsubst_η (T : heterogeneous_substitution) :
identity `T = η T •• `T · (prejoin_from_hetsubst T).
Show proof.
refine (pr1 (bracket_property_parts_identity_nicer_impl1 T (θ_from_hetsubst T) _ _)).
apply parts_from_whole.
exact (pr2 (pr1 (pr2 (pr2 T)))).
apply parts_from_whole.
exact (pr2 (pr1 (pr2 (pr2 T)))).
Lemma prejoin_from_hetsubst_τ (T : heterogeneous_substitution) :
θ_from_hetsubst T `T · #H (prejoin_from_hetsubst T) · τ T = τ T •• `T · (prejoin_from_hetsubst T).
Show proof.
refine (pr2 (bracket_property_parts_identity_nicer_impl1 T (θ_from_hetsubst T) _ _)).
apply parts_from_whole.
exact (pr2 (pr1 (pr2 (pr2 T)))).
apply parts_from_whole.
exact (pr2 (pr1 (pr2 (pr2 T)))).
Section fix_a_prestrength.
Context (θ : @PrestrengthForSignature C C C H).
Definition bracket (T : algebra_ob Id_H) : UU
:= ∏ (Z : Ptd) (f : Z --> ptd_from_alg T), bracket_at (nat_trans_fix_snd_arg _ _ _ _ _ θ Z) T f.
Lemma isaprop_bracket (T : algebra_ob Id_H) : isaprop (bracket T).
Show proof.
Definition bracket_parts (T : algebra_ob Id_H) : UU
:= ∏ (Z : Ptd) (f : Z --> ptd_from_alg T), bracket_parts_at (nat_trans_fix_snd_arg _ _ _ _ _ θ Z) T f.
End fix_a_prestrength.
End prep_hss.
Arguments ptd_from_alg {_} _ .
Arguments prejoin_from_hetsubst {_} _ .
Arguments prejoin_from_hetsubst_η {_} _ .
Arguments prejoin_from_hetsubst_τ {_} _ .
Arguments bracket_parts {_} _ _ .
Section def_hss.
Context (H : Presignature C C C).
Local Notation η := (eta_from_alg H).
Local Notation τ := (tau_from_alg H).
Let θ : PrestrengthForSignature H := theta H.
Let Id_H : [C, C] ⟶ [C, C] := Id_H H.
the notion of a heterogeneous substitution system that asks for more operations to uniquely exist
Definition hss : UU := ∑ (T: algebra_ob Id_H), bracket H θ T.
Coercion hetsubst_from_hss (T : hss) : heterogeneous_substitution H := pr1 T,, (nat_trans_fix_snd_arg _ _ _ _ _ θ (ptd_from_alg (pr1 T)) ,, pr2 T _ (identity _)).
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).
Coercion hetsubst_from_hss (T : hss) : heterogeneous_substitution H := pr1 T,, (nat_trans_fix_snd_arg _ _ _ _ _ θ (ptd_from_alg (pr1 T)) ,, pr2 T _ (identity _)).
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⦄.
Show proof.
intros α H1 H2.
apply path_to_ctr.
apply whole_from_parts.
split.
- apply nat_trans_eq_alt; assumption.
- apply nat_trans_eq_alt; assumption.
apply path_to_ctr.
apply whole_from_parts.
split.
- apply nat_trans_eq_alt; assumption.
- apply nat_trans_eq_alt; assumption.
Definition fbracket_unique (T : hss) {Z : Ptd} (f : Z --> ptd_from_alg T)
: ∏ α : `T • (U Z) --> `T,
bracket_property_parts H (nat_trans_fix_snd_arg _ _ _ _ _ θ Z) T f α
→
α = ⦃f⦄.
Show proof.
Definition fbracket_unique_target_pointwise (T : hss) {Z : Ptd} (f : Z --> ptd_from_alg T)
: ∏ α : `T • U Z --> `T,
bracket_property_parts H (nat_trans_fix_snd_arg _ _ _ _ _ θ Z) T f α
→
∏ c, pr1 α c = pr1 ⦃ f ⦄ c.
Show proof.
intros α H12.
set (t:= fbracket_unique _ _ α H12).
apply (nat_trans_eq_weq (homset_property C) _ _ t).
set (t:= fbracket_unique _ _ α H12).
apply (nat_trans_eq_weq (homset_property C) _ _ t).
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⦄.
Show proof.
Lemma fbracket_τ (T : hss) : ∏ {Z : Ptd} (f : Z --> ptd_from_alg T),
θ (`T ⊗ Z) · #H ⦃f⦄ · τ T
=
τ T •• U Z · ⦃f⦄.
Show proof.
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 ⦄.
Show proof.
apply fbracket_unique_pointwise.
- simpl. intro c.
rewrite assoc.
pose proof (nat_trans_ax (η T)) as H'.
simpl in H'.
rewrite <- H'; clear H'.
rewrite <- assoc.
apply maponpaths.
pose proof (nat_trans_eq_weq (homset_property C) _ _ (fbracket_η T g)) as X.
simpl in X. exact (X _ ).
- intro c; simpl.
assert (H':=nat_trans_ax (τ 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 (τ 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 C C C 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 C C).
rewrite A; try apply homset_property.
apply idpath.
- simpl. intro c.
rewrite assoc.
pose proof (nat_trans_ax (η T)) as H'.
simpl in H'.
rewrite <- H'; clear H'.
rewrite <- assoc.
apply maponpaths.
pose proof (nat_trans_eq_weq (homset_property C) _ _ (fbracket_η T g)) as X.
simpl in X. exact (X _ ).
- intro c; simpl.
assert (H':=nat_trans_ax (τ 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 (τ 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 C C C 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 C C).
rewrite A; try apply homset_property.
apply idpath.
Lemma compute_fbracket (T : hss) : ∏ {Z : Ptd} (f : Z --> ptd_from_alg T),
⦃ f ⦄ = (` T ∘ # U f : EndC ⟦ `T • U Z , `T • U (ptd_from_alg T) ⟧) · ⦃ identity (ptd_from_alg T) ⦄.
Show proof.
intros Z f.
assert (A : f = f · identity _ ).
{ rewrite id_right; apply idpath. }
rewrite A.
rewrite <- fbracket_natural.
rewrite id_right.
apply idpath.
assert (A : f = f · identity _ ).
{ rewrite id_right; apply idpath. }
rewrite A.
rewrite <- fbracket_natural.
rewrite id_right.
apply idpath.
Section from_identity_to_hss.
the operations of an hss can be obtained through this formula from
just a heterogeneous substitution
Context (T : algebra_ob Id_H).
Context (prejoin : bracket_at H (nat_trans_fix_snd_arg _ _ _ _ _ θ (ptd_from_alg T)) T (identity _)).
Let T0 : heterogeneous_substitution H :=
T ,, (nat_trans_fix_snd_arg _ _ _ _ _ θ (ptd_from_alg T) ,, prejoin).
Lemma heterogeneous_substitution_into_bracket {Z : Ptd} (f : Z --> ptd_from_alg T0) :
bracket_property H (nat_trans_fix_snd_arg _ _ _ _ _ θ Z) T0 f
((` T0 ∘ # U f : EndC ⟦ `T0 • U Z , `T0 • U (ptd_from_alg T0) ⟧) · prejoin_from_hetsubst T0).
Show proof.
apply whole_from_parts.
split.
- apply nat_trans_eq_alt.
intro c.
induction f as [f pt].
simpl.
assert (alg_map_nat := nat_trans_ax (alg_map Id_H T0) _ _ (pr1 f c)).
etrans.
2: { rewrite <- assoc. apply maponpaths. rewrite assoc.
apply cancel_postcomposition.
exact alg_map_nat.
}
clear alg_map_nat.
etrans.
2: { do 2 rewrite assoc. do 2 apply cancel_postcomposition.
apply pathsinv0. unfold Id_H. simpl. apply BinCoproductIn1Commutes. }
simpl.
etrans.
{ apply pathsinv0.
apply id_right.
}
do 2 rewrite <- assoc.
apply maponpaths.
rewrite assoc.
assert (prejoin_ok := prejoin_from_hetsubst_η T0).
apply (maponpaths pr1) in prejoin_ok.
apply toforallpaths in prejoin_ok.
apply prejoin_ok.
- rewrite functor_comp.
apply nat_trans_eq_alt.
intro c.
induction f as [f pt].
simpl.
assert (alg_map_nat := nat_trans_ax (alg_map Id_H T0) _ _ (pr1 f c)).
etrans.
2: { rewrite <- assoc. apply maponpaths. rewrite assoc.
apply cancel_postcomposition.
exact alg_map_nat.
}
etrans.
2: { do 2 rewrite assoc. do 2 apply cancel_postcomposition.
apply pathsinv0. unfold Id_H. simpl. apply BinCoproductIn2Commutes. }
assert (prejoin_ok := prejoin_from_hetsubst_τ T0).
apply (maponpaths pr1) in prejoin_ok.
apply toforallpaths in prejoin_ok.
assert (prejoin_ok_inst := prejoin_ok c).
simpl in prejoin_ok_inst.
etrans.
{ repeat rewrite assoc. do 3 apply cancel_postcomposition.
apply pathsinv0.
assert (theta_nat_2 := θ_nat_2_pointwise _ _ _ H θ `T0 _ _ (f,,pt) c).
rewrite horcomp_id_postwhisker in theta_nat_2; try apply homset_property.
apply theta_nat_2.
}
etrans.
{ repeat rewrite <- assoc. apply maponpaths.
rewrite assoc.
exact prejoin_ok_inst.
}
clear prejoin_ok prejoin_ok_inst.
repeat rewrite assoc.
apply idpath.
split.
- apply nat_trans_eq_alt.
intro c.
induction f as [f pt].
simpl.
assert (alg_map_nat := nat_trans_ax (alg_map Id_H T0) _ _ (pr1 f c)).
etrans.
2: { rewrite <- assoc. apply maponpaths. rewrite assoc.
apply cancel_postcomposition.
exact alg_map_nat.
}
clear alg_map_nat.
etrans.
2: { do 2 rewrite assoc. do 2 apply cancel_postcomposition.
apply pathsinv0. unfold Id_H. simpl. apply BinCoproductIn1Commutes. }
simpl.
etrans.
{ apply pathsinv0.
apply id_right.
}
do 2 rewrite <- assoc.
apply maponpaths.
rewrite assoc.
assert (prejoin_ok := prejoin_from_hetsubst_η T0).
apply (maponpaths pr1) in prejoin_ok.
apply toforallpaths in prejoin_ok.
apply prejoin_ok.
- rewrite functor_comp.
apply nat_trans_eq_alt.
intro c.
induction f as [f pt].
simpl.
assert (alg_map_nat := nat_trans_ax (alg_map Id_H T0) _ _ (pr1 f c)).
etrans.
2: { rewrite <- assoc. apply maponpaths. rewrite assoc.
apply cancel_postcomposition.
exact alg_map_nat.
}
etrans.
2: { do 2 rewrite assoc. do 2 apply cancel_postcomposition.
apply pathsinv0. unfold Id_H. simpl. apply BinCoproductIn2Commutes. }
assert (prejoin_ok := prejoin_from_hetsubst_τ T0).
apply (maponpaths pr1) in prejoin_ok.
apply toforallpaths in prejoin_ok.
assert (prejoin_ok_inst := prejoin_ok c).
simpl in prejoin_ok_inst.
etrans.
{ repeat rewrite assoc. do 3 apply cancel_postcomposition.
apply pathsinv0.
assert (theta_nat_2 := θ_nat_2_pointwise _ _ _ H θ `T0 _ _ (f,,pt) c).
rewrite horcomp_id_postwhisker in theta_nat_2; try apply homset_property.
apply theta_nat_2.
}
etrans.
{ repeat rewrite <- assoc. apply maponpaths.
rewrite assoc.
exact prejoin_ok_inst.
}
clear prejoin_ok prejoin_ok_inst.
repeat rewrite assoc.
apply idpath.
End from_identity_to_hss.
Morphisms of heterogeneous substitution systems
a little preparation for much later
Lemma τ_part_of_alg_mor (T T' : @algebra_ob [C, C] Id_H)
(β : @algebra_mor [C, C] Id_H T T'): #H β · τ T' = compose (C:=EndC) (τ T) β.
Show proof.
(β : @algebra_mor [C, C] Id_H T T'): #H β · τ T' = compose (C:=EndC) (τ T) β.
Show proof.
assert (β_is_alg_mor := pr2 β).
simpl in β_is_alg_mor.
assert (β_is_alg_mor_inst := maponpaths (fun m:EndC⟦_,_⟧ => (BinCoproductIn2 (CPEndC _ _))· m)
β_is_alg_mor); clear β_is_alg_mor.
simpl in β_is_alg_mor_inst.
apply nat_trans_eq_alt.
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.
simpl in β_is_alg_mor.
assert (β_is_alg_mor_inst := maponpaths (fun m:EndC⟦_,_⟧ => (BinCoproductIn2 (CPEndC _ _))· m)
β_is_alg_mor); clear β_is_alg_mor.
simpl in β_is_alg_mor_inst.
apply nat_trans_eq_alt.
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.
A morphism β of pointed functors is a bracket morphism when...
Lemma is_ptd_mor_alg_mor (T T' : @algebra_ob [C, C] Id_H)
(β : @algebra_mor [C, C] Id_H T T') :
@is_ptd_mor C (ptd_from_alg T) (ptd_from_alg T') (pr1 β).
Show proof.
simpl.
unfold is_ptd_mor. simpl.
intro c.
rewrite <- assoc.
assert (X:=pr2 β).
assert (X':= nat_trans_eq_pointwise X c).
simpl in *.
etrans. { apply maponpaths. apply X'. }
unfold coproduct_nat_trans_in1_data.
repeat rewrite assoc.
unfold coproduct_nat_trans_data.
etrans.
{ apply cancel_postcomposition.
apply BinCoproductIn1Commutes. }
simpl.
repeat rewrite <- assoc.
apply id_left.
unfold is_ptd_mor. simpl.
intro c.
rewrite <- assoc.
assert (X:=pr2 β).
assert (X':= nat_trans_eq_pointwise X c).
simpl in *.
etrans. { apply maponpaths. apply X'. }
unfold coproduct_nat_trans_in1_data.
repeat rewrite assoc.
unfold coproduct_nat_trans_data.
etrans.
{ apply cancel_postcomposition.
apply BinCoproductIn1Commutes. }
simpl.
repeat rewrite <- assoc.
apply id_left.
Definition ptd_from_alg_mor {T T' : algebra_ob Id_H} (β : algebra_mor _ T T')
: ptd_from_alg T --> ptd_from_alg T'.
Show proof.
show functor laws for ptd_from_alg and ptd_from_alg_mor
Definition ptd_from_alg_functor_data : functor_data (category_FunctorAlg Id_H) Ptd.
Show proof.
Lemma is_functor_ptd_from_alg_functor_data : is_functor ptd_from_alg_functor_data.
Show proof.
split; simpl; intros.
+ unfold functor_idax.
intro T.
apply (invmap (eq_ptd_mor_cat _ _ _)).
apply (invmap (eq_ptd_mor _ _)).
apply idpath.
+ unfold functor_compax.
intros T T' T'' β β'.
apply (invmap (eq_ptd_mor_cat _ _ _)).
apply (invmap (eq_ptd_mor _ _)).
apply idpath.
+ unfold functor_idax.
intro T.
apply (invmap (eq_ptd_mor_cat _ _ _)).
apply (invmap (eq_ptd_mor _ _)).
apply idpath.
+ unfold functor_compax.
intros T T' T'' β β'.
apply (invmap (eq_ptd_mor_cat _ _ _)).
apply (invmap (eq_ptd_mor _ _)).
apply idpath.
Definition ptd_from_alg_functor: functor (category_FunctorAlg Id_H) 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 β).
Show proof.
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 β.
Show that equality of hssMor is equality of underlying nat. transformations
Context (T T' : hss) (β β' : hssMor T T').
Definition hssMor_eq1 : β = β' ≃ (pr1 β = pr1 β').
Show proof.
Definition hssMor_eq : β = β' ≃ (β : EndC ⟦ _ , _ ⟧) = β'.
Show proof.
eapply weqcomp.
- apply hssMor_eq1.
- apply subtypeInjectivity.
intro.
apply isaset_nat_trans.
apply homset_property.
- apply hssMor_eq1.
- apply subtypeInjectivity.
intro.
apply isaset_nat_trans.
apply homset_property.
End hssMor_equality.
Lemma isaset_hssMor (T T' : hss) : isaset (hssMor T T').
Show proof.
intros β β'.
apply (isofhlevelweqb _ (hssMor_eq _ _ β β')).
apply isaset_nat_trans.
apply homset_property.
apply (isofhlevelweqb _ (hssMor_eq _ _ β β')).
apply isaset_nat_trans.
apply homset_property.
Lemma ishssMor_id (T : hss) : ishssMor (identity (C:=category_FunctorAlg _) (pr1 T)).
Show 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 (U Z)).
set (H2' := functor_id H2). simpl in H2'.
simpl.
rewrite H2'.
rewrite (@id_left EndC).
apply idpath.
unfold isbracketMor.
intros Z f.
rewrite id_right.
rewrite functor_id.
rewrite id_right.
apply pathsinv0.
set (H2:=pre_composition_functor _ _ C (U Z)).
set (H2' := functor_id H2). simpl in H2'.
simpl.
rewrite H2'.
rewrite (@id_left EndC).
apply idpath.
Definition hssMor_id (T : hss) : hssMor _ _ := tpair _ _ (ishssMor_id T).
Lemma ishssMor_comp {T T' T'' : hss} (β : hssMor T T') (γ : hssMor T' T'')
: ishssMor (compose (C:=category_FunctorAlg _) (pr1 β) (pr1 γ)).
Show proof.
unfold ishssMor.
unfold isbracketMor.
intros Z f.
eapply pathscomp0; [apply assoc|].
etrans.
{ apply cancel_postcomposition.
apply isbracketMor_hssMor. }
rewrite <- assoc.
etrans.
{ apply maponpaths.
apply isbracketMor_hssMor. }
rewrite assoc.
rewrite functor_comp.
rewrite assoc.
apply cancel_postcomposition.
apply pathsinv0, (functor_comp (pre_composition_functor _ _ C (U Z)) ).
unfold isbracketMor.
intros Z f.
eapply pathscomp0; [apply assoc|].
etrans.
{ apply cancel_postcomposition.
apply isbracketMor_hssMor. }
rewrite <- assoc.
etrans.
{ apply maponpaths.
apply isbracketMor_hssMor. }
rewrite assoc.
rewrite functor_comp.
rewrite assoc.
apply cancel_postcomposition.
apply pathsinv0, (functor_comp (pre_composition_functor _ _ C (U Z)) ).
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.
Show proof.
Definition hss_precategory_data : precategory_data.
Show proof.
Lemma is_precategory_hss : is_precategory hss_precategory_data.
Show proof.
apply is_precategory_one_assoc_to_two.
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).
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).
Definition hss_precategory : precategory := tpair _ _ is_precategory_hss.
Lemma has_homsets_precategory_hss : has_homsets hss_precategory.
Show proof.
Definition hss_category : category := hss_precategory ,, has_homsets_precategory_hss.
End def_hss.
End fix_a_category.
Arguments hss {_} _ _ .
Arguments hssMor {_ _ _ } _ _ .
Arguments fbracket {_ _ _} _ {_} _ .
Arguments fbracket_η {_ _ _} _ {_} _ .
Arguments fbracket_τ {_ _ _} _ {_} _ .
Arguments fbracket_unique_target_pointwise {_ _ _ } _ {_ _ _} _ _.
Arguments fbracket_unique {_ _ _ } _ {_} _ {_} _ .
Arguments hss_precategory {_} _ _ .
Arguments hss_category {_} _ _ .
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 {_ _ _} _ _.
Arguments prejoin_from_hetsubst {_ _ _} _ .
Arguments prejoin_from_hetsubst_η {_ _ _} _ .
Arguments prejoin_from_hetsubst_τ {_ _ _} _ .
Notation τ := tau_from_alg.
Notation η := eta_from_alg.