(* -*- mode: coq; mode: visual-line -*-  *)

Require Import Basics.Overture Basics.Tactics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.Core.

(** ** Opposite categories *)

Definition op (A : Type) := A.
Notation "A ^op" := (op A).

(** This stops typeclass search from trying to unfold op. *)
#[global] Typeclasses Opaque op.

Global Instance isgraph_op {A : Type} `{IsGraph A}
  : IsGraph A^op.
A: Type
H: IsGraph A
IsGraph A^op
Proof.
A: Type
H: IsGraph A
IsGraph A^op
  apply Build_IsGraph.
A: Type
H: IsGraph A
A^op -> A^op -> Type
  unfold op; exact (fun a b => b $-> a).
Defined.

Global Instance is01cat_op {A : Type} `{Is01Cat A} : Is01Cat A^op.
A: Type
H: IsGraph A
H0: Is01Cat A
Is01Cat A^op
Proof.
A: Type
H: IsGraph A
H0: Is01Cat A
Is01Cat A^op
  apply Build_Is01Cat.
A: Type
H: IsGraph A
H0: Is01Cat A
forall a : A^op, a $-> a
A: Type
H: IsGraph A
H0: Is01Cat A
forall a b c : A^op, (b $-> c) -> (a $-> b) -> a $-> c
  +
A: Type
H: IsGraph A
H0: Is01Cat A
forall a : A^op, a $-> a cbv; exact Id.
  +
A: Type
H: IsGraph A
H0: Is01Cat A
forall a b c : A^op, (b $-> c) -> (a $-> b) -> a $-> c cbv; exact (fun a b c g f => f $o g).
Defined.

(** We don't invert 2-cells as this is op on the first level. *)
Global Instance is2graph_op {A : Type} `{Is2Graph A} : Is2Graph A^op.
A: Type
H: IsGraph A
H0: Is2Graph A
Is2Graph A^op
Proof.
A: Type
H: IsGraph A
H0: Is2Graph A
Is2Graph A^op
  intros a b; unfold op in *; cbn; exact _.
Defined.

Global Instance is1cat_op {A : Type} `{Is1Cat A} : Is1Cat A^op.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is1Cat A^op
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is1Cat A^op
  snrapply Build_Is1Cat; unfold op in *; cbv in *.
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
forall a b : A, Is01Cat (b $-> a)
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
forall a b : A, Is0Gpd (b $-> a)
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b c : A) (g : c $-> b),
Is0Functor (fun f : b $-> a => f $o g)
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b c : A) (f : b $-> a),
Is0Functor (fun g : c $-> b => f $o g)
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b c d : A) (f : b $-> a) 
(g : c $-> b) (h : d $-> c),
f $o (g $o h) $-> f $o g $o h
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b c d : A) (f : b $-> a) 
(g : c $-> b) (h : d $-> c),
f $o g $o h $-> f $o (g $o h)
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b : A) (f : b $-> a), f $o Id b $-> f
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b : A) (f : b $-> a), Id a $o f $-> f
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
forall a b : A, Is01Cat (b $-> a) intros a b.
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b: A
Is01Cat (b $-> a)
    apply is01cat_hom.
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
forall a b : A, Is0Gpd (b $-> a) intros a b.
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b: A
Is0Gpd (b $-> a)
    apply is0gpd_hom.
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b c : A) (g : c $-> b),
Is0Functor (fun f : b $-> a => f $o g) intros a b c h.
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
h: c $-> b
Is0Functor (fun f : b $-> a => f $o h)
    srapply Build_Is0Functor.
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
h: c $-> b
forall a0 b0 : b $-> a,
(a0 $-> b0) ->
(fun f : b $-> a => f $o h) a0 $->
(fun f : b $-> a => f $o h) b0
    intros f g p.
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
h: c $-> b
f, g: b $-> a
p: f $-> g
(fun f : b $-> a => f $o h) f $->
(fun f : b $-> a => f $o h) g
    cbn in *.
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
h: c $-> b
f, g: b $-> a
p: f $-> g
f $o h $-> g $o h
    exact (p $@R h).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b c : A) (f : b $-> a),
Is0Functor (fun g : c $-> b => f $o g) intros a b c h.
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
h: b $-> a
Is0Functor (fun g : c $-> b => h $o g)
    srapply Build_Is0Functor.
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
h: b $-> a
forall a0 b0 : c $-> b,
(a0 $-> b0) ->
(fun g : c $-> b => h $o g) a0 $->
(fun g : c $-> b => h $o g) b0
    intros f g p.
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
h: b $-> a
f, g: c $-> b
p: f $-> g
(fun g : c $-> b => h $o g) f $->
(fun g : c $-> b => h $o g) g
    cbn in *.
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
h: b $-> a
f, g: c $-> b
p: f $-> g
h $o f $-> h $o g
    exact (h $@L p).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b c d : A) (f : b $-> a) 
(g : c $-> b) (h : d $-> c),
f $o (g $o h) $-> f $o g $o h intros a b c d f g h; exact (cat_assoc_opp h g f).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b c d : A) (f : b $-> a) 
(g : c $-> b) (h : d $-> c),
f $o g $o h $-> f $o (g $o h) intros a b c d f g h; exact (cat_assoc h g f).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b : A) (f : b $-> a), f $o Id b $-> f intros a b f; exact (cat_idr f).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: forall a b : A, IsGraph (a $-> b)
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b : A) (f : b $-> a), Id a $o f $-> f intros a b f; exact (cat_idl f).
Defined.

Global Instance is1cat_strong_op A `{Is1Cat_Strong A}
  : Is1Cat_Strong (A ^op).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
Is1Cat_Strong A^op
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
Is1Cat_Strong A^op
  snrapply Build_Is1Cat_Strong.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall a b : A^op, Is01Cat (a $-> b)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall a b : A^op, Is0Gpd (a $-> b)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b c : A^op) (g : b $-> c),
Is0Functor (cat_postcomp a g)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b c : A^op) (f : a $-> b),
Is0Functor (cat_precomp c f)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b c d : A^op) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o g $o f = h $o (g $o f)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b c d : A^op) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o (g $o f) = h $o g $o f
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b : A^op) (f : a $-> b), Id b $o f = f
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b : A^op) (f : a $-> b), f $o Id a = f
  1-4: exact _.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b c d : A^op) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o g $o f = h $o (g $o f)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b c d : A^op) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o (g $o f) = h $o g $o f
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b : A^op) (f : a $-> b), Id b $o f = f
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b : A^op) (f : a $-> b), f $o Id a = f
  all: cbn.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b c d : A^op) 
(f : b $-> a) (g : c $-> b) 
(h : d $-> c), f $o (g $o h) = f $o g $o h
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b c d : A^op) 
(f : b $-> a) (g : c $-> b) 
(h : d $-> c), f $o g $o h = f $o (g $o h)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b : A^op) (f : b $-> a), f $o Id b = f
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b : A^op) (f : b $-> a), Id a $o f = f
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b c d : A^op) 
(f : b $-> a) (g : c $-> b) 
(h : d $-> c), f $o (g $o h) = f $o g $o h intros a b c d f g h; exact (cat_assoc_opp_strong h g f).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b c d : A^op) 
(f : b $-> a) (g : c $-> b) 
(h : d $-> c), f $o g $o h = f $o (g $o h) intros a b c d f g h; exact (cat_assoc_strong h g f).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b : A^op) (f : b $-> a), f $o Id b = f intros a b f.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
a, b: A^op
f: b $-> a
f $o Id b = f
    apply cat_idr_strong.
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b : A^op) (f : b $-> a), Id a $o f = f intros a b f.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
a, b: A^op
f: b $-> a
Id a $o f = f
    apply cat_idl_strong.
Defined.

(** Opposite groupoids *)

Global Instance is0gpd_op A `{Is0Gpd A} : Is0Gpd (A^op).
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
Is0Gpd A^op
Proof.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
Is0Gpd A^op
  srapply Build_Is0Gpd; unfold op in *; cbn in *.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
forall a b : A, (b $-> a) -> a $-> b
  intros a b.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
a, b: A
(b $-> a) -> a $-> b
  apply gpd_rev.
Defined.

Global Instance op0gpd_fun A `{Is0Gpd A} :
  Is0Functor( (fun x => x) : A^op -> A).
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
Is0Functor (idmap : A^op -> A)
Proof.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
Is0Functor (idmap : A^op -> A)
  srapply Build_Is0Functor; unfold op in *; cbn.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
forall a b : A, (b $-> a) -> a $-> b
  intros a b.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
a, b: A
(b $-> a) -> a $-> b
  exact (fun f => f^$).
Defined.

(** ** Opposite functors *)

Global Instance is0functor_op A B (F : A -> B)
  `{IsGraph A, IsGraph B, x : !Is0Functor F}
  : Is0Functor (F : A^op -> B^op).
A, B: Type
F: A -> B
H: IsGraph A
H0: IsGraph B
x: Is0Functor F
Is0Functor (F : A^op -> B^op)
Proof.
A, B: Type
F: A -> B
H: IsGraph A
H0: IsGraph B
x: Is0Functor F
Is0Functor (F : A^op -> B^op)
  apply Build_Is0Functor.
A, B: Type
F: A -> B
H: IsGraph A
H0: IsGraph B
x: Is0Functor F
forall a b : A^op, (a $-> b) -> F a $-> F b
  intros a b; cbn.
A, B: Type
F: A -> B
H: IsGraph A
H0: IsGraph B
x: Is0Functor F
a, b: A^op
(b $-> a) -> F b $-> F a
  apply fmap.
A, B: Type
F: A -> B
H: IsGraph A
H0: IsGraph B
x: Is0Functor F
a, b: A^op
Is0Functor F
  assumption.
Defined.

Global Instance is1functor_op A B (F : A -> B)
  `{Is1Cat A, Is1Cat B, !Is0Functor F, !Is1Functor F}
  : Is1Functor (F : A^op -> B^op).
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
Is1Functor (F : A^op -> B^op)
Proof.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
Is1Functor (F : A^op -> B^op)
  apply Build_Is1Functor; cbn.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
forall (a b : A^op) (f g : b $-> a),
f $== g -> fmap F f $== fmap F g
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
forall a : A^op, fmap F (Id a) $== Id (F a)
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
forall (a b c : A^op) (f : b $-> a) 
(g : c $-> b),
fmap F (f $o g) $== fmap F f $o fmap F g
  -
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
forall (a b : A^op) (f g : b $-> a),
f $== g -> fmap F f $== fmap F g intros a b; rapply fmap2.
  -
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
forall a : A^op, fmap F (Id a) $== Id (F a) exact (fmap_id F).
  -
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
forall (a b c : A^op) (f : b $-> a) 
(g : c $-> b),
fmap F (f $o g) $== fmap F f $o fmap F g intros a b c f g; exact (fmap_comp F g f).
Defined.

(** Since [Is01Cat] structures are definitionally involutive (see test/WildCat/Opposite.v), we can use [is0functor_op] to transform in the reverse direction as well.  This result makes that much easier to use in practice. *)
Global Instance is0functor_op' A B (F : A^op -> B^op)
  `{IsGraph A, IsGraph B, Fop : !Is0Functor (F : A^op -> B^op)}
  : Is0Functor (F : A -> B)
  := is0functor_op A^op B^op F.

(** [Is1Cat] structures are also definitionally involutive. *)
Global Instance is1functor_op' A B (F : A^op -> B^op)
  `{Is1Cat A, Is1Cat B, !Is0Functor (F : A^op -> B^op), Fop2 : !Is1Functor (F : A^op -> B^op)}
  : Is1Functor (F : A -> B)
  := is1functor_op A^op B^op F.

Global Instance hasmorext_op {A : Type} `{H0 : HasMorExt A}
  : HasMorExt A^op.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
HasMorExt A^op
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
HasMorExt A^op
  snrapply Build_HasMorExt.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
forall (a b : A^op) (f g : a $-> b),
IsEquiv GpdHom_path
  intros a b f g.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
a, b: A^op
f, g: a $-> b
IsEquiv GpdHom_path
  refine (@isequiv_Htpy_path _ _ _ _ _ H0 b a f g).
Defined.

Global Instance isinitial_isterminal_op {A : Type} `{Is1Cat A} (x : A)
  {t : IsTerminal x} : IsInitial (A := A^op) x
  := t.

Global Instance isterminal_isinitial_op {A : Type} `{Is1Cat A} (x : A)
  {i : IsInitial x} : IsTerminal (A := A^op) x
  := i.