(** * Propositional self-duality of groupoid categories *)Require Import HoTT.Types. Require Import Basics.Trunc Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. Local Open Scope category_scope.H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X(groupoid_category X)^op = groupoid_category Xrepeat 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.H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X(groupoid_category X)^op = groupoid_category X