proposition: Lemma path_groupoid_dual `{Univalence} `{IsTrunc 1 X} : (groupoid_category X)^op = groupoid_category X.
proof: 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.
imports: Category.Core GroupoidCategory.Core Category.Paths Category.Dual HoTT.Types Basics.Trunc Basics.Tactics