fact: Fixpoint op_subalgebra {w : SymbolType σ} : ∀ (α : Operation A w), ClosedUnderOp A P α → Operation carriers_subalgebra w := match w with | [:t:] => λ α c, (α; c) | s ::: w' => λ α c x, op_subalgebra (α x.1) (c x.1 x.2) end.
imports: HoTT.HProp HoTT.Types HoTT.Classes.theory.ua_homomorphism