Composition respects fragment equivalence

Interface gluing and composition are congruences for the relabelling equivalence of fragments: equivalent inputs glue to equivalent outputs. These are the transport lemmas through which every up-to-isomorphism identity about composition is proved.

noncomputable def RS.glueInterfaceCongr (s t u : ℕ) {W₁ W₂ : Fragment (Fin (s + t) ⊕ Fin (t + u))} : W₁.Equiv W₂ → (glueInterface s t u W₁).Equiv (glueInterface s t u W₂)

Interface gluing respects fragment equivalence.

Equations

• RS.glueInterfaceCongr s 0 x✝³ x✝ = x✝.relabelCongr ((finCongr ⋯).sumCongr (finCongr ⋯))
• RS.glueInterfaceCongr s t.succ x✝³ x✝ = RS.glueInterfaceCongr s t x✝³ ((x✝.gluePairCongr ⋯).relabelCongr (RS.interfaceStepEquiv s t x✝³))

noncomputable def RS.Fragment.composeCongr {s t u : ℕ} {F₁ F₂ : Fragment (Fin (s + t))} {G₁ G₂ : Fragment (Fin (t + u))} (hF : F₁.Equiv F₂) (hG : G₁.Equiv G₂) : (F₁.compose G₁).Equiv (F₂.compose G₂)

Composition respects fragment equivalence in both arguments.

Equations

• RS.Fragment.composeCongr hF hG = (RS.glueInterfaceCongr s t u (hF.disjUnionCongr hG)).relabelCongr finSumFinEquiv