fact: Fixpoint path_forall_ap_operation `{Funext} {σ : Signature} {A : Carriers σ} {w : SymbolType σ} : ∀ (f g : Operation A w), (∀ a : FamilyProd A (dom_symboltype w), ap_operation f a = ap_operation g a) -> f = g := match w with | [:s:] => λ (f g : A s) p, p tt | s ::: w' => λ (f g : A s → Operation A w') p, path_forall f g (λ x, path_forall_ap_operation (f x) (g x) (λ a, p (x,a))) end.
imports: HoTT.Utf8Minimal HoTT.Basics HoTT.Classes.implementations.ne_list HoTT.Classes.implementations.family_prod HoTT.Types HoTT.HSet HoTT.Classes.implementations.list