proposition: Lemma path_operations_isomorphism (f : ∀ s, A s → B s) `{IsIsomorphism σ A B f} (u : Symbol σ) : transport (λ C : Carriers σ, Operation C (σ u)) (path_equiv_family (equiv_isomorphism f)) u.#A = u.#B.
proof: Proof. by apply path_operations_equiv. Defined.
imports: HoTT.Classes.interfaces.ua_setalgebra HoTT.Types HoTT.Tactics