(** * The functor [ᵒᵖ : cat → cat] *)
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.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope category_scope.

Section opposite.
  Context `{Funext}.

  Variable P : PreCategory -> Type.
  Context `{forall C, IsHProp (P C)}.
  Context `{HF : forall C D, P C -> P D -> IsHSet (Functor C D)}.

  Let cat := (@sub_pre_cat _ P HF).

  Hypothesis has_op : forall C : cat, P C.1^op.

  Definition opposite_functor : Functor cat cat
    := Build_Functor
         cat cat
         (fun C => (C.1^op; has_op _))
         (fun _ _ F => F^op)%functor
         (fun _ _ _ _ _ => idpath)
         (fun _ => idpath).

  Let opposite_functor_involutive_helper (x : cat)
  : (x.1^op^op; has_op (_; has_op _)) = x
    := path_sigma_uncurried
         P
         (((x.1^op)^op)%category;
          has_op ((x.1^op)%category;
                  has_op x))
         x
         (Category.Dual.opposite_involutive x.1;
          path_ishprop _ _).

  Local Open Scope functor_scope.

  Local Arguments path_sigma_uncurried : simpl never.

  Definition opposite_functor_involutive
  : opposite_functor o opposite_functor = 1.
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
cat:= sub_pre_cat P: PreCategory
has_op: forall C : cat, P (C.1)^op
opposite_functor_involutive_helper:= fun x : cat =>
path_sigma_uncurried P
  (((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)) x
  (Category.Dual.opposite_involutive x.1;
  path_ishprop
    (transport P (Category.Dual.opposite_involutive x.1)
       (((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)).2)
    x.2): forall x : cat,
(((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)) = x
opposite_functor o opposite_functor = 1
  Proof.
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
cat:= sub_pre_cat P: PreCategory
has_op: forall C : cat, P (C.1)^op
opposite_functor_involutive_helper:= fun x : cat =>
path_sigma_uncurried P
  (((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)) x
  (Category.Dual.opposite_involutive x.1;
  path_ishprop
    (transport P (Category.Dual.opposite_involutive x.1)
       (((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)).2)
    x.2): forall x : cat,
(((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)) = x
opposite_functor o opposite_functor = 1
    path_functor.
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
cat:= sub_pre_cat P: PreCategory
has_op: forall C : cat, P (C.1)^op
opposite_functor_involutive_helper:= fun x : cat =>
path_sigma_uncurried P
  (((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)) x
  (Category.Dual.opposite_involutive x.1;
  path_ishprop
    (transport P (Category.Dual.opposite_involutive x.1)
       (((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)).2)
    x.2): forall x : cat,
(((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)) = x
{HO
: (fun c : {C : PreCategory & P C} =>
   (((c.1)^op)^op%category; has_op ((c.1)^op%category; has_op c))) =
  idmap
&
transport
  (fun GO : {C : PreCategory & P C} -> {C : PreCategory & P C} =>
   forall s d : {C : PreCategory & P C},
   Functor s.1 d.1 -> Functor (GO s).1 (GO d).1)
  HO (fun (s d : {C : PreCategory & P C}) (m : Functor s.1 d.1) => (m^op)^op) =
(fun s d : {C : PreCategory & P C} => idmap)}
    refine (path_forall _ _ opposite_functor_involutive_helper; _).
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
cat:= sub_pre_cat P: PreCategory
has_op: forall C : cat, P (C.1)^op
opposite_functor_involutive_helper:= fun x : cat =>
path_sigma_uncurried P
  (((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)) x
  (Category.Dual.opposite_involutive x.1;
  path_ishprop
    (transport P (Category.Dual.opposite_involutive x.1)
       (((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)).2)
    x.2): forall x : cat,
(((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)) = x
transport
  (fun GO : {C : PreCategory & P C} -> {C : PreCategory & P C} =>
   forall s d : {C : PreCategory & P C},
   Functor s.1 d.1 -> Functor (GO s).1 (GO d).1)
  (path_forall
     (fun x : cat =>
      (((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)))
     idmap opposite_functor_involutive_helper)
  (fun (s d : {C : PreCategory & P C}) (m : Functor s.1 d.1) => (m^op)^op) =
(fun s d : {C : PreCategory & P C} => idmap)
    repeat (apply path_forall; intro).
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
cat:= sub_pre_cat P: PreCategory
has_op: forall C : cat, P (C.1)^op
opposite_functor_involutive_helper:= fun x2 : cat =>
path_sigma_uncurried P
  (((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) x2
  (Category.Dual.opposite_involutive x2.1;
  path_ishprop
    (transport P (Category.Dual.opposite_involutive x2.1)
       (((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)).2)
    x2.2): forall x2 : cat,
(((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) = x2
x, x0: {C : PreCategory & P C}
x1: Functor x.1 x0.1
transport
  (fun GO : {C : PreCategory & P C} -> {C : PreCategory & P C} =>
   forall s d : {C : PreCategory & P C},
   Functor s.1 d.1 -> Functor (GO s).1 (GO d).1)
  (path_forall
     (fun x2 : cat =>
      (((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)))
     idmap opposite_functor_involutive_helper)
  (fun (s d : {C : PreCategory & P C}) (m : Functor s.1 d.1) => (m^op)^op) x
  x0 x1 =
x1
    rewrite !transport_forall_constant.
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
cat:= sub_pre_cat P: PreCategory
has_op: forall C : cat, P (C.1)^op
opposite_functor_involutive_helper:= fun x2 : cat =>
path_sigma_uncurried P
  (((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) x2
  (Category.Dual.opposite_involutive x2.1;
  path_ishprop
    (transport P (Category.Dual.opposite_involutive x2.1)
       (((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)).2)
    x2.2): forall x2 : cat,
(((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) = x2
x, x0: {C : PreCategory & P C}
x1: Functor x.1 x0.1
transport
  (fun x2 : {C : PreCategory & P C} -> {C : PreCategory & P C} =>
   Functor (x2 x).1 (x2 x0).1)
  (path_forall
     (fun x2 : cat =>
      (((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)))
     idmap opposite_functor_involutive_helper)
  (x1^op)^op =
x1
    transport_path_forall_hammer.
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
cat:= sub_pre_cat P: PreCategory
has_op: forall C : cat, P (C.1)^op
opposite_functor_involutive_helper:= fun x2 : cat =>
path_sigma_uncurried P
  (((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) x2
  (Category.Dual.opposite_involutive x2.1;
  path_ishprop
    (transport P (Category.Dual.opposite_involutive x2.1)
       (((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)).2)
    x2.2): forall x2 : cat,
(((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) = x2
x, x0: {C : PreCategory & P C}
x1: Functor x.1 x0.1
transport (fun y : {C : PreCategory & P C} => Functor x.1 y.1)
  (opposite_functor_involutive_helper x0)
  (transport
     (fun y : {C : PreCategory & P C} =>
      Functor y.1
        (((x0.1)^op)^op%category; has_op ((x0.1)^op%category; has_op x0)).1)
     (opposite_functor_involutive_helper x) (x1^op)^op) =
x1
    unfold opposite_functor_involutive_helper.
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
cat:= sub_pre_cat P: PreCategory
has_op: forall C : cat, P (C.1)^op
opposite_functor_involutive_helper:= fun x2 : cat =>
path_sigma_uncurried P
  (((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) x2
  (Category.Dual.opposite_involutive x2.1;
  path_ishprop
    (transport P (Category.Dual.opposite_involutive x2.1)
       (((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)).2)
    x2.2): forall x2 : cat,
(((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) = x2
x, x0: {C : PreCategory & P C}
x1: Functor x.1 x0.1
transport (fun y : {C : PreCategory & P C} => Functor x.1 y.1)
  (path_sigma_uncurried P
     (((x0.1)^op)^op%category; has_op ((x0.1)^op%category; has_op x0)) x0
     (Category.Dual.opposite_involutive x0.1;
     path_ishprop
       (transport P (Category.Dual.opposite_involutive x0.1)
          (((x0.1)^op)^op%category; has_op ((x0.1)^op%category; has_op x0)).2)
       x0.2))
  (transport
     (fun y : {C : PreCategory & P C} =>
      Functor y.1
        (((x0.1)^op)^op%category; has_op ((x0.1)^op%category; has_op x0)).1)
     (path_sigma_uncurried P
        (((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)) x
        (Category.Dual.opposite_involutive x.1;
        path_ishprop
          (transport P (Category.Dual.opposite_involutive x.1)
             (((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)).2)
          x.2))
     (x1^op)^op) =
x1
    rewrite !transport_pr1_path_sigma_uncurried.
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
cat:= sub_pre_cat P: PreCategory
has_op: forall C : cat, P (C.1)^op
opposite_functor_involutive_helper:= fun x2 : cat =>
path_sigma_uncurried P
  (((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) x2
  (Category.Dual.opposite_involutive x2.1;
  path_ishprop
    (transport P (Category.Dual.opposite_involutive x2.1)
       (((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)).2)
    x2.2): forall x2 : cat,
(((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) = x2
x, x0: {C : PreCategory & P C}
x1: Functor x.1 x0.1
transport (Functor x.1)
  (Category.Dual.opposite_involutive x0.1;
  path_ishprop
    (transport P (Category.Dual.opposite_involutive x0.1)
       (((x0.1)^op)^op%category; has_op ((x0.1)^op%category; has_op x0)).2)
    x0.2).1
  (transport
     (fun y : {C : PreCategory & P C} =>
      Functor y.1
        (((x0.1)^op)^op%category; has_op ((x0.1)^op%category; has_op x0)).1)
     (path_sigma_uncurried P
        (((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)) x
        (Category.Dual.opposite_involutive x.1;
        path_ishprop
          (transport P (Category.Dual.opposite_involutive x.1)
             (((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)).2)
          x.2))
     (x1^op)^op) =
x1
    simpl in *.
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
cat:= sub_pre_cat P: PreCategory
has_op: forall C : {C : PreCategory & P C}, P (C.1)^op
opposite_functor_involutive_helper:= fun x2 : {C : PreCategory & P C} =>
path_sigma_uncurried P
  (((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) x2
  (Category.Dual.opposite_involutive x2.1;
  path_ishprop (has_op ((x2.1)^op%category; has_op x2)) x2.2): forall x2 : {C : PreCategory & P C},
(((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) = x2
x, x0: {C : PreCategory & P C}
x1: Functor x.1 x0.1
transport (fun y : {C : PreCategory & P C} => Functor y.1 ((x0.1)^op)^op)
  (path_sigma_uncurried P
     (((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)) x
     (Category.Dual.opposite_involutive x.1;
     path_ishprop (has_op ((x.1)^op%category; has_op x)) x.2))
  (x1^op)^op =
x1
    repeat progress change (fun x => ?f x) with f in *.
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
cat:= sub_pre_cat P: PreCategory
has_op: forall C : {x : _ & P x}, P (C.1)^op
opposite_functor_involutive_helper:= fun x2 : {x : _ & P x} =>
path_sigma_uncurried P
  (((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) x2
  (Category.Dual.opposite_involutive x2.1;
  path_ishprop (has_op ((x2.1)^op%category; has_op x2)) x2.2): forall x2 : {x : _ & P x},
(((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) = x2
x, x0: {x : _ & P x}
x1: Functor x.1 x0.1
transport (fun y : {x : _ & P x} => Functor y.1 ((x0.1)^op)^op)
  (path_sigma_uncurried P
     (((x.1)^op)^op%category; has_op ((x.1)^op%category; has_op x)) x
     (Category.Dual.opposite_involutive x.1;
     path_ishprop (has_op ((x.1)^op%category; has_op x)) x.2))
  (x1^op)^op =
x1
    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.
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
cat:= sub_pre_cat P: PreCategory
has_op: forall C : {x : _ & P x}, P (C.1)^op
opposite_functor_involutive_helper:= fun x2 : {x : _ & P x} =>
path_sigma_uncurried P
  (((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) x2
  (Category.Dual.opposite_involutive x2.1;
  path_ishprop (has_op ((x2.1)^op%category; has_op x2)) x2.2): forall x2 : {x : _ & P x},
(((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) = x2
x, x0: {x : _ & P x}
x1: Functor x.1 x0.1
transport (fun x2 : PreCategory => Functor x2 ((x0.1)^op)^op)
  (Category.Dual.opposite_involutive x.1;
  path_ishprop (has_op ((x.1)^op%category; has_op x)) x.2).1 
  (x1^op)^op =
x1
    simpl in *.
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
cat:= sub_pre_cat P: PreCategory
has_op: forall C : {x : _ & P x}, P (C.1)^op
opposite_functor_involutive_helper:= fun x2 : {x : _ & P x} =>
path_sigma_uncurried P
  (((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) x2
  (Category.Dual.opposite_involutive x2.1;
  path_ishprop (has_op ((x2.1)^op%category; has_op x2)) x2.2): forall x2 : {x : _ & P x},
(((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) = x2
x, x0: {x : _ & P x}
x1: Functor x.1 x0.1
(x1^op)^op = x1
    hnf in *.
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
cat:= {|
  object := {C : PreCategory & P C};
  morphism :=
    fun (C : {C : PreCategory & P C}) (D : {C0 : PreCategory & P C0}) =>
    Functor C.1 D.1;
  Core.identity := fun C : {C : PreCategory & P C} => 1;
  Category.Core.compose :=
    fun (s d d' : {C : PreCategory & P C}) (F : Functor d.1 d'.1)
      (G : Functor s.1 d.1) =>
    F o G;
  associativity :=
    fun (x2 x3 x4 x5 : {C : PreCategory & P C}) (m1 : Functor x2.1 x3.1)
      (m2 : Functor x3.1 x4.1) (m3 : Functor x4.1 x5.1) =>
    Laws.associativity m1 m2 m3;
  associativity_sym :=
    fun (x2 x3 x4 x5 : {C : PreCategory & P C}) (m1 : Functor x2.1 x3.1)
      (m2 : Functor x3.1 x4.1) (m3 : Functor x4.1 x5.1) =>
    symmetry (m3 o m2 o m1) (m3 o (m2 o m1)) (Laws.associativity m1 m2 m3);
  left_identity :=
    fun (a b : {C : PreCategory & P C}) (f : Functor a.1 b.1) =>
    Laws.left_identity f;
  right_identity :=
    fun (a b : {C : PreCategory & P C}) (f : Functor a.1 b.1) =>
    Laws.right_identity f;
  identity_identity :=
    fun x2 : {C : PreCategory & P C} => Laws.left_identity 1;
  trunc_morphism := fun s d : {C : PreCategory & P C} => HF s.2 d.2
|}: PreCategory
has_op: forall C : {x : _ & P x}, P (C.1)^op
opposite_functor_involutive_helper:= fun x2 : {x : _ & P x} =>
path_sigma_uncurried P
  (((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) x2
  (Category.Dual.opposite_involutive x2.1;
  path_ishprop (has_op ((x2.1)^op%category; has_op x2)) x2.2): forall x2 : {x : _ & P x},
(((x2.1)^op)^op%category; has_op ((x2.1)^op%category; has_op x2)) = x2
x, x0: {x : _ & P x}
x1: Functor x.1 x0.1
(x1^op)^op = x1
    subst_body.
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
has_op: forall C : {x : _ & P x}, P (C.1)^op
x, x0: {x : _ & P x}
x1: Functor x.1 x0.1
(x1^op)^op = x1
    destruct_head @sig.
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
has_op: forall C : {x : _ & P x}, P (C.1)^op
proj0: PreCategory
proj3: P proj0
proj1: PreCategory
proj2: P proj1
x1: Functor proj0 proj1
(x1^op)^op = x1
    destruct_head @Functor.
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
has_op: forall C : {x : _ & P x}, P (C.1)^op
proj0: PreCategory
proj3: P proj0
proj1: PreCategory
proj2: P proj1
object_of: proj0 -> proj1
morphism_of: forall s d : proj0,
morphism proj0 s d -> morphism proj1 (object_of s) (object_of d)
composition_of: forall (s d d' : proj0) (m1 : morphism proj0 s d) 
(m2 : morphism proj0 d d'),
morphism_of s d' (m2 o m1)%morphism =
(morphism_of d d' m2 o morphism_of s d m1)%morphism
identity_of: forall x : proj0, morphism_of x x 1%morphism = 1%morphism
({|
   object_of := object_of;
   morphism_of := morphism_of;
   composition_of := composition_of;
   identity_of := identity_of
 |}^op)^op =
{|
  object_of := object_of;
  morphism_of := morphism_of;
  composition_of := composition_of;
  identity_of := identity_of
|}
    destruct_head @PreCategory.
H: Funext
P: PreCategory -> Type
H0: forall C : PreCategory, IsHProp (P C)
HF: forall C D : PreCategory, P C -> P D -> IsHSet (Functor C D)
has_op: forall C : {x : _ & P x}, P (C.1)^op
object0: Type
morphism0: object0 -> object0 -> Type
identity0: forall x : object0, morphism0 x x
compose0: forall s d d' : object0, morphism0 d d' -> morphism0 s d -> morphism0 s d'
associativity0: forall (x1 x2 x3 x4 : object0) (m1 : morphism0 x1 x2) 
(m2 : morphism0 x2 x3) (m3 : morphism0 x3 x4),
compose0 x1 x2 x4 (compose0 x2 x3 x4 m3 m2) m1 =
compose0 x1 x3 x4 m3 (compose0 x1 x2 x3 m2 m1)
associativity_sym0: forall (x1 x2 x3 x4 : object0) (m1 : morphism0 x1 x2) 
(m2 : morphism0 x2 x3) (m3 : morphism0 x3 x4),
compose0 x1 x3 x4 m3 (compose0 x1 x2 x3 m2 m1) =
compose0 x1 x2 x4 (compose0 x2 x3 x4 m3 m2) m1
left_identity0: forall (a b : object0) (f : morphism0 a b),
compose0 a b b (identity0 b) f = f
right_identity0: forall (a b : object0) (f : morphism0 a b),
compose0 a a b f (identity0 a) = f
identity_identity0: forall x : object0, compose0 x x x (identity0 x) (identity0 x) = identity0 x
trunc_morphism0: forall s d : object0, IsHSet (morphism0 s d)
proj3: P
  {|
    object := object0;
    morphism := morphism0;
    Core.identity := identity0;
    Category.Core.compose := compose0;
    associativity := associativity0;
    associativity_sym := associativity_sym0;
    left_identity := left_identity0;
    right_identity := right_identity0;
    identity_identity := identity_identity0;
    trunc_morphism := trunc_morphism0
  |}
object: Type
morphism: object -> object -> Type
identity: forall x : object, morphism x x
compose: forall s d d' : object, morphism d d' -> morphism s d -> morphism s d'
associativity: forall (x1 x2 x3 x4 : object) (m1 : morphism x1 x2) 
(m2 : morphism x2 x3) (m3 : morphism x3 x4),
compose x1 x2 x4 (compose x2 x3 x4 m3 m2) m1 =
compose x1 x3 x4 m3 (compose x1 x2 x3 m2 m1)
associativity_sym: forall (x1 x2 x3 x4 : object) (m1 : morphism x1 x2) 
(m2 : morphism x2 x3) (m3 : morphism x3 x4),
compose x1 x3 x4 m3 (compose x1 x2 x3 m2 m1) =
compose x1 x2 x4 (compose x2 x3 x4 m3 m2) m1
left_identity: forall (a b : object) (f : morphism a b), compose a b b (identity b) f = f
right_identity: forall (a b : object) (f : morphism a b), compose a a b f (identity a) = f
identity_identity: forall x : object, compose x x x (identity x) (identity x) = identity x
trunc_morphism: forall s d : object, IsHSet (morphism s d)
proj2: P
  {|
    object := object;
    morphism := morphism;
    Core.identity := identity;
    Category.Core.compose := compose;
    associativity := associativity;
    associativity_sym := associativity_sym;
    left_identity := left_identity;
    right_identity := right_identity;
    identity_identity := identity_identity;
    trunc_morphism := trunc_morphism
  |}
object_of: object0 -> object
morphism_of: forall s d : object0, morphism0 s d -> morphism (object_of s) (object_of d)
composition_of: forall (s d d' : object0) (m1 : morphism0 s d) (m2 : morphism0 d d'),
morphism_of s d' (compose0 s d d' m2 m1) =
compose (object_of s) (object_of d) (object_of d') 
  (morphism_of d d' m2) (morphism_of s d m1)
identity_of: forall x : object0, morphism_of x x (identity0 x) = identity (object_of x)
({|
   object_of := object_of;
   morphism_of := morphism_of;
   composition_of := composition_of;
   identity_of := identity_of
 |}^op)^op =
{|
  object_of := object_of;
  morphism_of := morphism_of;
  composition_of := composition_of;
  identity_of := identity_of
|}
    reflexivity.
  Qed.
End opposite.