proposition: Theorem path_isomorphism (f : ∀ s, A s → B s) `{IsIsomorphism σ A B f} : A = B.
proof: Proof. apply (path_algebra _ _ (path_equiv_family (equiv_isomorphism f))). abstract ( funext u; exact (transport_forall_constant _ _ u @ path_operations_isomorphism f u)). Defined.
imports: HoTT.Classes.interfaces.ua_setalgebra HoTT.Types HoTT.Tactics