(** * Propositional self-duality of groupoid categories *)
Require Import Category.Core GroupoidCategory.Core Category.Paths Category.Dual.
Require Import HoTT.Types.
Require Import Basics.Trunc Basics.Tactics.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope category_scope.

Lemma path_groupoid_dual `{Univalence} `{IsTrunc 1 X}
: (groupoid_category X)^op = groupoid_category X.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
(groupoid_category X)^op = groupoid_category X
Proof.
H: Univalence
X: Type
IsTrunc0: IsTrunc 1 X
(groupoid_category X)^op = groupoid_category X
  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.