`{Funext} : sig_functor_obj o sig_functor_obj_inv = 1 /\ sig_functor_obj_inv o sig_functor_obj = 1. Proof. split; path_functor; trivial. apply path_forall; intros []. apply path_forall; intros []. apply path_forall; intros [? []]. reflexivity. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import Category.Core Functor.Core Category.Sigma.Core. Require Import Functor.Paths. Import Functor.Identity.FunctorIdentityNotations. Import Functor.Composition.Core.FunctorCompositionCoreNotations.