`{Funext} : sig_functor_mor o sig_functor_mor_inv = 1 /\ sig_functor_mor_inv o sig_functor_mor = 1. Proof. split; path_functor; simpl; trivial. refine (exist _ (path_forall _ _ (fun x => match x as x return (x.1; tt) = x with | (_; tt) => idpath end)) _). repeat (apply path_forall; intro). destruct_head @sig_type. destruct_head Unit. rewrite !transport_forall_constant. transport_path_forall_hammer. reflexivity. Qed.
Require Import HoTT.Tactics Types.Forall Types.Sigma Basics.Trunc. Require Import Category.Core Functor.Core Category.Sigma.Core. Require Import Functor.Paths. Import Functor.Identity.FunctorIdentityNotations. Import Functor.Composition.Core.FunctorCompositionCoreNotations.