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.

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; cbv.
A: Type
H: IsGraph A
A -> A -> Type
  intros a b; exact (Hom b a).
Defined.

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; cbv.
A: Type
H: IsGraph A
H0: Is01Cat A
forall a : A, a $-> a
A: Type
H: IsGraph A
H0: Is01Cat A
forall a b c : A, (c $-> b) -> (b $-> a) -> c $-> a
  +
A: Type
H: IsGraph A
H0: Is01Cat A
forall a : A, a $-> a exact Id.
  +
A: Type
H: IsGraph A
H0: Is01Cat A
forall a b c : A, (c $-> b) -> (b $-> a) -> c $-> a intros a b c f g; exact (cat_comp g f).
Defined.

(** We don't invert 2-cells as this is op on the first level. *)
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
  cbv.
A: Type
H: IsGraph A
H0: Is2Graph A
forall a b : A, IsGraph (b $-> a)
  intros a b; exact (isgraph_hom b a).
Defined.

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
  snapply Build_Is1Cat; cbv.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
forall a b : A, Is01Cat (b $-> a)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
forall a b : A, Is0Gpd (b $-> a)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b c : A) (g : c $-> b),
Is0Functor (fun g0 : b $-> a => g0 $o g)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
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: Is2Graph A
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: Is2Graph A
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: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b : A) (f : b $-> a), f $o Id b $-> f
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b : A) (f : b $-> a), Id a $o f $-> f
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
forall a b : A, Is01Cat (b $-> a) intros a b; exact (is01cat_hom b a).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
forall a b : A, Is0Gpd (b $-> a) intros a b; exact (is0gpd_hom b a).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b c : A) (g : c $-> b),
Is0Functor (fun g0 : b $-> a => g0 $o g) intros a b c; exact (is0functor_precomp c b a).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
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; exact (is0functor_postcomp c b a).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
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: Is2Graph A
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: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b : A) (f : b $-> a), f $o Id b $-> f intros a b; exact cat_idr.
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b : A) (f : b $-> a), Id a $o f $-> f intros a b; exact cat_idl.
Defined.

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
  snapply Build_Is1Cat_Strong; cbv.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall a b : A, Is01Cat (b $-> a)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall a b : A, Is0Gpd (b $-> a)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b c : A) (g : c $-> b),
Is0Functor (fun g0 : b $-> a => g0 $o g)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b c : A) (f : b $-> a),
Is0Functor (fun g : c $-> b => f $o g)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong 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: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong 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: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b : A) (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) (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 : A, Is01Cat (b $-> a) intros a b; exact (is01cat_hom_strong b a).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall a b : A, Is0Gpd (b $-> a) intros a b; exact (is0gpd_hom_strong b a).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b c : A) (g : c $-> b),
Is0Functor (fun g0 : b $-> a => g0 $o g) intros a b c; exact (is0functor_precomp_strong c b a).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b c : A) (f : b $-> a),
Is0Functor (fun g : c $-> b => f $o g) intros a b c; exact (is0functor_postcomp_strong c b a).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong 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_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) (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) (f : b $-> a), f $o Id b = f intros a b; exact cat_idr_strong.
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
forall (a b : A) (f : b $-> a), Id a $o f = f intros a b; exact cat_idl_strong.
Defined.

(** Opposite groupoids *)

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; cbv.
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 gpd_rev.
Defined.

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; cbv.
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 *)

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; cbv.
A, B: Type
F: A -> B
H: IsGraph A
H0: IsGraph B
x: Is0Functor F
forall a b : A, (b $-> a) -> F b $-> F a
  intros a b; exact (fmap F).
Defined.

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; cbv.
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) (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, 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) (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) (f g : b $-> a),
(f $-> g) -> fmap F f $-> fmap F g intros a b f g; exact (fmap2 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 : A, 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) (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. *)
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. *)
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.

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
  unfold op.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
HasMorExt A
  intros a b; exact (isequiv_Htpy_path b a).
Defined.

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

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