`{Univalence} `{IsTrunc 1 X} : (groupoid_category X)^op = groupoid_category X. Proof. repeat match goal with | _ => intro | _ => progress cbn | _ => reflexivity | _ => apply path_forall | _ => apply (path_universe (symmetry _ _)) | _ => exact (center _) | _ => progress rewrite ?transport_path_universe, ?transport_path_universe_V | _ => progress path_category | _ => progress path_induction end. Qed.
Require Import Category.Core GroupoidCategory.Core Category.Paths Category.Dual. Require Import HoTT.Types. Require Import Basics.Trunc Basics.Tactics.