(** * The functor [ᵒᵖ : cat → cat] *)
Require Import Category.Core Functor.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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 Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

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 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
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 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) 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 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
x, x0: {C : PreCategory & P C}
x1: Functor x.1 x0.1
transport
  (fun
     x1 : {C : PreCategory & P C} ->
          {C : PreCategory & P C} =>
   Functor (x1 x).1 (x1 x0).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) (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 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
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 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
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 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
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
  x : {C
      : PreCategory
      & P C} =>
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): forall
x : {C
    : PreCategory
    & P C},
(((x.1)^op)^op%category;
has_op
  ((x.1)^op%category;
  has_op x)) = x
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
  x : {x : _ &
      P 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
    (has_op
       ((x.1)^op%category;
       has_op x))
    x.2): forall
x : {x : _ & P x},
(((x.1)^op)^op%category;
has_op
  ((x.1)^op%category;
  has_op x)) = x
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
  x : {x : _ &
      P 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
    (has_op
       ((x.1)^op%category;
       has_op x))
    x.2): forall
x : {x : _ & P x},
(((x.1)^op)^op%category;
has_op
  ((x.1)^op%category;
  has_op x)) = x
x, x0: {x : _ & P x}
x1: Functor x.1 x0.1
transport
  (fun x : PreCategory => Functor x ((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
  x : {x : _ &
      P 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
    (has_op
       ((x.1)^op%category;
       has_op x))
    x.2): forall
x : {x : _ & P x},
(((x.1)^op)^op%category;
has_op
  ((x.1)^op%category;
  has_op x)) = x
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 (x1 x2 x3 x4 : {C : PreCategory & P C})
      (m1 : Functor x1.1 x2.1)
      (m2 : Functor x2.1 x3.1)
      (m3 : Functor x3.1 x4.1) =>
    Laws.associativity m1 m2 m3;
  associativity_sym :=
    fun (x1 x2 x3 x4 : {C : PreCategory & P C})
      (m1 : Functor x1.1 x2.1)
      (m2 : Functor x2.1 x3.1)
      (m3 : Functor x3.1 x4.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 x : {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
  x : {x : _ &
      P 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
    (has_op
       ((x.1)^op%category;
       has_op x))
    x.2): forall
x : {x : _ & P x},
(((x.1)^op)^op%category;
has_op
  ((x.1)^op%category;
  has_op x)) = x
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.