proposition: Lemma sig_mor_eq `{Funext} : sig_functor_mor o sig_functor_mor_inv = 1 /\ sig_functor_mor_inv o sig_functor_mor = 1.
proof: 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.
imports: HoTT.Tactics Types.Forall Types.Sigma Basics.Trunc Category.Core Functor.Core Category.Sigma.Core Functor.Paths