opposite_functor o opposite_functor = 1. Proof. path_functor. refine (path_forall _ _ opposite_functor_involutive_helper; _). repeat (apply path_forall; intro). rewrite !transport_forall_constant. transport_path_forall_hammer. unfold opposite_functor_involutive_helper. rewrite !transport_pr1_path_sigma_uncurried. simpl in *. repeat progress change (fun x => ?f x) with f in *. match goal with | [ |- context[transport (fun x' => ?f x'.1 ?y) (@path_sigma_uncurried ?A ?P ?u ?v ?pq)] ] => rewrite (@transport_pr1_path_sigma_uncurried A P u v pq (fun x => f x y)) end. simpl in *. hnf in *. subst_body. destruct_head @sig. destruct_head @Functor. destruct_head @PreCategory. reflexivity. Qed.
Require Import Category.Core Functor.Core. Require Import Category.Dual Functor.Dual. Require Import Functor.Composition.Core Functor.Identity. Require Import Cat.Core Functor.Paths. Require Import Basics.Trunc Types.Sigma HoTT.Tactics Types.Forall.