proposition: Lemma sig_obj_eq `{Funext} : sig_functor_obj o sig_functor_obj_inv = 1 /\ sig_functor_obj_inv o sig_functor_obj = 1.
proof: Proof. split; path_functor; trivial. apply path_forall; intros []. apply path_forall; intros []. apply path_forall; intros [? []]. reflexivity. Qed.
imports: HoTT.Basics HoTT.Types Category.Core Functor.Core Category.Sigma.Core Functor.Paths