proposition: Lemma path_operations_equiv {w : SymbolType σ} (α : Operation A w) (β : Operation B w) (f : ∀ (s : Sort σ), A s <~> B s) (P : OpPreserving f α β) : transport (λ C : Carriers σ, Operation C w) (path_equiv_family f) α = β.
proof: Proof. induction w; simpl in *. - transport_path_forall_hammer. exact (ap10 (transport_idmap_path_universe (f t)) α @ P). - funext y. transport_path_forall_hammer. rewrite transport_forall_constant. rewrite transport_arrow_toconst. rewrite (transport_path_universe_V (f t)). apply IHw. specialize (P ((f t)^-1 y)). by rewrite (eisretr (f t) y) in P. Qed.
imports: HoTT.Classes.interfaces.ua_setalgebra HoTT.Types HoTT.Tactics