(* -*- 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.
Require Import WildCat.Opposite.
Require Import WildCat.Equiv.
Require Import WildCat.Induced.
Require Import WildCat.NatTrans.

(** * Wild functor categories *)

(** ** Categories of 0-coherent 1-functors *)

Record Fun01 (A B : Type) `{IsGraph A} `{IsGraph B} := {
  fun01_F : A -> B;
  fun01_is0functor : Is0Functor fun01_F;
}.

Coercion fun01_F : Fun01 >-> Funclass.
Global Existing Instance fun01_is0functor.

Arguments Build_Fun01 A B {isgraph_A isgraph_B} F {fun01_is0functor} : rename.

Definition issig_Fun01 (A B : Type) `{IsGraph A} `{IsGraph B}
  : _  <~> Fun01 A B := ltac:(issig).

(* Note that even if [A] and [B] are fully coherent oo-categories, the objects of our "functor category" are not fully coherent.  Thus we cannot in general expect this "functor category" to itself be fully coherent.  However, it is at least a 0-coherent 1-category, as long as [B] is a 1-coherent 1-category. *)

Global Instance isgraph_fun01 (A B : Type) `{IsGraph A} `{Is1Cat B} : IsGraph (Fun01 A B).
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph (Fun01 A B)
Proof.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph (Fun01 A B)
  srapply Build_IsGraph.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
Fun01 A B -> Fun01 A B -> Type
  intros [F ?] [G ?].
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
Type
  exact (NatTrans F G).
Defined.

Global Instance is01cat_fun01 (A B : Type) `{IsGraph A} `{Is1Cat B} : Is01Cat (Fun01 A B).
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
Is01Cat (Fun01 A B)
Proof.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
Is01Cat (Fun01 A B)
  srapply Build_Is01Cat.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall a : Fun01 A B, a $-> a
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall a b c : Fun01 A B,
(b $-> c) -> (a $-> b) -> a $-> c
  -
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall a : Fun01 A B, a $-> a intros [F ?]; cbn.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
NatTrans F F
    exists (id_transformation F); exact _.
  -
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall a b c : Fun01 A B,
(b $-> c) -> (a $-> b) -> a $-> c intros [F ?] [G ?] [K ?] [gamma ?] [alpha ?]; cbn in *.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
K: A -> B
fun01_is0functor2: Is0Functor K
gamma: G $=> K
is1natural_nattrans: Is1Natural G K gamma
alpha: F $=> G
is1natural_nattrans0: Is1Natural F G alpha
NatTrans F K
    exists (trans_comp gamma alpha); exact _.
Defined.

Global Instance is2graph_fun01 (A B : Type) `{IsGraph A, Is1Cat B}
  : Is2Graph (Fun01 A B).
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
Is2Graph (Fun01 A B)
Proof.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
Is2Graph (Fun01 A B)
  intros [F ?] [G ?]; apply Build_IsGraph.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
({|
   fun01_F := F; fun01_is0functor := fun01_is0functor0
 |} $->
 {|
   fun01_F := G; fun01_is0functor := fun01_is0functor1
 |}) ->
({|
   fun01_F := F; fun01_is0functor := fun01_is0functor0
 |} $->
 {|
   fun01_F := G; fun01_is0functor := fun01_is0functor1
 |}) -> Type
  intros [alpha ?] [gamma ?].
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
is1natural_nattrans: Is1Natural F G alpha
gamma: F $=> G
is1natural_nattrans0: Is1Natural F G gamma
Type
  exact (forall a, alpha a $== gamma a).
Defined.

(** In fact, in this case it is automatically also a 0-coherent 2-category and a 1-coherent 1-category, with a totally incoherent notion of 2-cell between 1-coherent natural transformations. *)

Global Instance is1cat_fun01 (A B : Type) `{IsGraph A} `{Is1Cat B} : Is1Cat (Fun01 A B).
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
Is1Cat (Fun01 A B)
Proof.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
Is1Cat (Fun01 A B)
  srapply Build_Is1Cat.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall a b : Fun01 A B, Is01Cat (a $-> b)
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall a b : Fun01 A B, Is0Gpd (a $-> b)
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall (a b c : Fun01 A B) 
(g : b $-> c), Is0Functor (cat_postcomp a g)
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall (a b c : Fun01 A B) 
(f : a $-> b), Is0Functor (cat_precomp c f)
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall (a b c d : Fun01 A B) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o g $o f $== h $o (g $o f)
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall (a b c d : Fun01 A B) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o (g $o f) $== h $o g $o f
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall (a b : Fun01 A B) 
(f : a $-> b), Id b $o f $== f
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall (a b : Fun01 A B) 
(f : a $-> b), f $o Id a $== f
  -
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall a b : Fun01 A B, Is01Cat (a $-> b) intros [F ?] [G ?]; srapply Build_Is01Cat.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
forall
a : {|
      fun01_F := F;
      fun01_is0functor := fun01_is0functor0
    |} $->
    {|
      fun01_F := G;
      fun01_is0functor := fun01_is0functor1
    |}, a $-> a
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
forall
a b
 c : {|
       fun01_F := F;
       fun01_is0functor := fun01_is0functor0
     |} $->
     {|
       fun01_F := G;
       fun01_is0functor := fun01_is0functor1
     |}, (b $-> c) -> (a $-> b) -> a $-> c
    +
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
forall
a : {|
      fun01_F := F;
      fun01_is0functor := fun01_is0functor0
    |} $->
    {|
      fun01_F := G;
      fun01_is0functor := fun01_is0functor1
    |}, a $-> a intros [alpha ?] a; cbn.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
is1natural_nattrans: Is1Natural F G alpha
a: A
alpha a $== alpha a
      reflexivity.
    +
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
forall
a b
 c : {|
       fun01_F := F;
       fun01_is0functor := fun01_is0functor0
     |} $->
     {|
       fun01_F := G;
       fun01_is0functor := fun01_is0functor1
     |}, (b $-> c) -> (a $-> b) -> a $-> c intros [alpha ?] [gamma ?] [phi ?] nu mu a.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
is1natural_nattrans: Is1Natural F G alpha
gamma: F $=> G
is1natural_nattrans0: Is1Natural F G gamma
phi: F $=> G
is1natural_nattrans1: Is1Natural F G phi
nu: {|
  trans_nattrans := gamma;
  is1natural_nattrans := is1natural_nattrans0
|} $->
{|
  trans_nattrans := phi;
  is1natural_nattrans := is1natural_nattrans1
|}
mu: {|
  trans_nattrans := alpha;
  is1natural_nattrans := is1natural_nattrans
|} $->
{|
  trans_nattrans := gamma;
  is1natural_nattrans := is1natural_nattrans0
|}
a: A
alpha a $== phi a
      exact (mu a $@ nu a).
  -
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall a b : Fun01 A B, Is0Gpd (a $-> b) intros [F ?] [G ?]; srapply Build_Is0Gpd.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
forall
a
 b : {|
       fun01_F := F;
       fun01_is0functor := fun01_is0functor0
     |} $->
     {|
       fun01_F := G;
       fun01_is0functor := fun01_is0functor1
     |}, (a $-> b) -> b $-> a
    intros [alpha ?] [gamma ?] mu a.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
is1natural_nattrans: Is1Natural F G alpha
gamma: F $=> G
is1natural_nattrans0: Is1Natural F G gamma
mu: {|
  trans_nattrans := alpha;
  is1natural_nattrans := is1natural_nattrans
|} $->
{|
  trans_nattrans := gamma;
  is1natural_nattrans := is1natural_nattrans0
|}
a: A
gamma a $== alpha a
    exact ((mu a)^$).
  -
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall (a b c : Fun01 A B) 
(g : b $-> c), Is0Functor (cat_postcomp a g) intros [F ?] [G ?] [K ?] [alpha ?].
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
K: A -> B
fun01_is0functor2: Is0Functor K
alpha: G $=> K
is1natural_nattrans: Is1Natural G K alpha
Is0Functor
  (cat_postcomp
     {|
       fun01_F := F;
       fun01_is0functor := fun01_is0functor0
     |}
     {|
       trans_nattrans := alpha;
       is1natural_nattrans := is1natural_nattrans
     |})
    srapply Build_Is0Functor.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
K: A -> B
fun01_is0functor2: Is0Functor K
alpha: G $=> K
is1natural_nattrans: Is1Natural G K alpha
forall
a
 b : {|
       fun01_F := F;
       fun01_is0functor := fun01_is0functor0
     |} $->
     {|
       fun01_F := G;
       fun01_is0functor := fun01_is0functor1
     |},
(a $-> b) ->
cat_postcomp
  {|
    fun01_F := F;
    fun01_is0functor := fun01_is0functor0
  |}
  {|
    trans_nattrans := alpha;
    is1natural_nattrans := is1natural_nattrans
  |} a $->
cat_postcomp
  {|
    fun01_F := F;
    fun01_is0functor := fun01_is0functor0
  |}
  {|
    trans_nattrans := alpha;
    is1natural_nattrans := is1natural_nattrans
  |} b
    intros [phi ?] [mu ?] f a.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
K: A -> B
fun01_is0functor2: Is0Functor K
alpha: G $=> K
is1natural_nattrans: Is1Natural G K alpha
phi: F $=> G
is1natural_nattrans0: Is1Natural F G phi
mu: F $=> G
is1natural_nattrans1: Is1Natural F G mu
f: {|
  trans_nattrans := phi;
  is1natural_nattrans := is1natural_nattrans0
|} $->
{|
  trans_nattrans := mu;
  is1natural_nattrans := is1natural_nattrans1
|}
a: A
cat_postcomp
  {|
    fun01_F := F;
    fun01_is0functor := fun01_is0functor0
  |}
  {|
    trans_nattrans := alpha;
    is1natural_nattrans := is1natural_nattrans
  |}
  {|
    trans_nattrans := phi;
    is1natural_nattrans := is1natural_nattrans0
  |} a $==
cat_postcomp
  {|
    fun01_F := F;
    fun01_is0functor := fun01_is0functor0
  |}
  {|
    trans_nattrans := alpha;
    is1natural_nattrans := is1natural_nattrans
  |}
  {|
    trans_nattrans := mu;
    is1natural_nattrans := is1natural_nattrans1
  |} a
    exact (alpha a $@L f a).
  -
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall (a b c : Fun01 A B) 
(f : a $-> b), Is0Functor (cat_precomp c f) intros [F ?] [G ?] [K ?] [alpha ?].
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
K: A -> B
fun01_is0functor2: Is0Functor K
alpha: F $=> G
is1natural_nattrans: Is1Natural F G alpha
Is0Functor
  (cat_precomp
     {|
       fun01_F := K;
       fun01_is0functor := fun01_is0functor2
     |}
     {|
       trans_nattrans := alpha;
       is1natural_nattrans := is1natural_nattrans
     |})
    srapply Build_Is0Functor.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
K: A -> B
fun01_is0functor2: Is0Functor K
alpha: F $=> G
is1natural_nattrans: Is1Natural F G alpha
forall
a
 b : {|
       fun01_F := G;
       fun01_is0functor := fun01_is0functor1
     |} $->
     {|
       fun01_F := K;
       fun01_is0functor := fun01_is0functor2
     |},
(a $-> b) ->
cat_precomp
  {|
    fun01_F := K;
    fun01_is0functor := fun01_is0functor2
  |}
  {|
    trans_nattrans := alpha;
    is1natural_nattrans := is1natural_nattrans
  |} a $->
cat_precomp
  {|
    fun01_F := K;
    fun01_is0functor := fun01_is0functor2
  |}
  {|
    trans_nattrans := alpha;
    is1natural_nattrans := is1natural_nattrans
  |} b
    intros [phi ?] [mu ?] f a.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
K: A -> B
fun01_is0functor2: Is0Functor K
alpha: F $=> G
is1natural_nattrans: Is1Natural F G alpha
phi: G $=> K
is1natural_nattrans0: Is1Natural G K phi
mu: G $=> K
is1natural_nattrans1: Is1Natural G K mu
f: {|
  trans_nattrans := phi;
  is1natural_nattrans := is1natural_nattrans0
|} $->
{|
  trans_nattrans := mu;
  is1natural_nattrans := is1natural_nattrans1
|}
a: A
cat_precomp
  {|
    fun01_F := K;
    fun01_is0functor := fun01_is0functor2
  |}
  {|
    trans_nattrans := alpha;
    is1natural_nattrans := is1natural_nattrans
  |}
  {|
    trans_nattrans := phi;
    is1natural_nattrans := is1natural_nattrans0
  |} a $==
cat_precomp
  {|
    fun01_F := K;
    fun01_is0functor := fun01_is0functor2
  |}
  {|
    trans_nattrans := alpha;
    is1natural_nattrans := is1natural_nattrans
  |}
  {|
    trans_nattrans := mu;
    is1natural_nattrans := is1natural_nattrans1
  |} a
    exact (f a $@R alpha a).
  -
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall (a b c d : Fun01 A B) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o g $o f $== h $o (g $o f) intros [F ?] [G ?] [K ?] [L ?] [alpha ?] [gamma ?] [phi ?] a; cbn.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
K: A -> B
fun01_is0functor2: Is0Functor K
L: A -> B
fun01_is0functor3: Is0Functor L
alpha: F $=> G
is1natural_nattrans: Is1Natural F G alpha
gamma: G $=> K
is1natural_nattrans0: Is1Natural G K gamma
phi: K $=> L
is1natural_nattrans1: Is1Natural K L phi
a: A
trans_comp (trans_comp phi gamma) alpha a $==
trans_comp phi (trans_comp gamma alpha) a
    srapply cat_assoc.
  -
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall (a b c d : Fun01 A B) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o (g $o f) $== h $o g $o f intros [F ?] [G ?] [K ?] [L ?] [alpha ?] [gamma ?] [phi ?] a; cbn.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
K: A -> B
fun01_is0functor2: Is0Functor K
L: A -> B
fun01_is0functor3: Is0Functor L
alpha: F $=> G
is1natural_nattrans: Is1Natural F G alpha
gamma: G $=> K
is1natural_nattrans0: Is1Natural G K gamma
phi: K $=> L
is1natural_nattrans1: Is1Natural K L phi
a: A
trans_comp phi (trans_comp gamma alpha) a $==
trans_comp (trans_comp phi gamma) alpha a
    srapply cat_assoc_opp.
  -
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall (a b : Fun01 A B) 
(f : a $-> b), Id b $o f $== f intros [F ?] [G ?] [alpha ?] a; cbn.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
is1natural_nattrans: Is1Natural F G alpha
a: A
trans_comp (id_transformation G) alpha a $== alpha a
    srapply cat_idl.
  -
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
forall (a b : Fun01 A B) 
(f : a $-> b), f $o Id a $== f intros [F ?] [G ?] [alpha ?] a; cbn.
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
is1natural_nattrans: Is1Natural F G alpha
a: A
trans_comp alpha (id_transformation F) a $== alpha a
    srapply cat_idr.
Defined.

(** It also inherits a notion of equivalence, namely a natural transformation that is a pointwise equivalence.  Note that this is not a "fully coherent" notion of equivalence, since the functors and transformations are not themselves fully coherent. *)

Global Instance hasequivs_fun01 (A B : Type) `{Is01Cat A} `{HasEquivs B}
  : HasEquivs (Fun01 A B).
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
HasEquivs (Fun01 A B)
Proof.
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
HasEquivs (Fun01 A B)
  srapply Build_HasEquivs.
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
Fun01 A B -> Fun01 A B -> Type
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall a b : Fun01 A B, (a $-> b) -> Type
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall a b : Fun01 A B, ?CatEquiv' a b -> a $-> b
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B) 
(f : ?CatEquiv' a b),
?CatIsEquiv' a b (?cate_fun' a b f)
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B) 
(f : a $-> b), ?CatIsEquiv' a b f -> ?CatEquiv' a b
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B) 
(f : a $-> b) (fe : ?CatIsEquiv' a b f),
?cate_fun' a b (?cate_buildequiv' a b f fe) $== f
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall a b : Fun01 A B, ?CatEquiv' a b -> b $-> a
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B) 
(f : ?CatEquiv' a b),
?cate_inv' a b f $o ?cate_fun' a b f $== Id a
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B) 
(f : ?CatEquiv' a b),
?cate_fun' a b f $o ?cate_inv' a b f $== Id b
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B) 
(f : a $-> b) (g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a -> ?CatIsEquiv' a b f
  1:{
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
Fun01 A B -> Fun01 A B -> Type intros [F ?] [G ?].
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
Type exact (NatEquiv F G). }
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall a b : Fun01 A B, (a $-> b) -> Type
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall a b : Fun01 A B,
(fun X : Fun01 A B =>
 (fun (F : A -> B) (fun01_is0functor0 : Is0Functor F)
    (X0 : Fun01 A B) =>
  (fun (G : A -> B) (fun01_is0functor1 : Is0Functor G)
   => NatEquiv F G) X0 
    (fun01_is0functor A B X0)) X
   (fun01_is0functor A B X)) a b -> 
a $-> b
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B)
(f : (fun X : Fun01 A B =>
      (fun (F : A -> B)
         (fun01_is0functor0 : Is0Functor F)
         (X0 : Fun01 A B) =>
       (fun (G : A -> B)
          (fun01_is0functor1 : Is0Functor G) =>
        NatEquiv F G) X0 
         (fun01_is0functor A B X0)) X
        (fun01_is0functor A B X)) a b),
?CatIsEquiv' a b (?cate_fun' a b f)
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B) 
(f : a $-> b),
?CatIsEquiv' a b f ->
(fun X : Fun01 A B =>
 (fun (F : A -> B) (fun01_is0functor0 : Is0Functor F)
    (X0 : Fun01 A B) =>
  (fun (G : A -> B) (fun01_is0functor1 : Is0Functor G)
   => NatEquiv F G) X0 
    (fun01_is0functor A B X0)) X
   (fun01_is0functor A B X)) a b
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B) 
(f : a $-> b) (fe : ?CatIsEquiv' a b f),
?cate_fun' a b (?cate_buildequiv' a b f fe) $== f
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall a b : Fun01 A B,
(fun X : Fun01 A B =>
 (fun (F : A -> B) (fun01_is0functor0 : Is0Functor F)
    (X0 : Fun01 A B) =>
  (fun (G : A -> B) (fun01_is0functor1 : Is0Functor G)
   => NatEquiv F G) X0 
    (fun01_is0functor A B X0)) X
   (fun01_is0functor A B X)) a b -> 
b $-> a
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B)
(f : (fun X : Fun01 A B =>
      (fun (F : A -> B)
         (fun01_is0functor0 : Is0Functor F)
         (X0 : Fun01 A B) =>
       (fun (G : A -> B)
          (fun01_is0functor1 : Is0Functor G) =>
        NatEquiv F G) X0 
         (fun01_is0functor A B X0)) X
        (fun01_is0functor A B X)) a b),
?cate_inv' a b f $o ?cate_fun' a b f $== Id a
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B)
(f : (fun X : Fun01 A B =>
      (fun (F : A -> B)
         (fun01_is0functor0 : Is0Functor F)
         (X0 : Fun01 A B) =>
       (fun (G : A -> B)
          (fun01_is0functor1 : Is0Functor G) =>
        NatEquiv F G) X0 
         (fun01_is0functor A B X0)) X
        (fun01_is0functor A B X)) a b),
?cate_fun' a b f $o ?cate_inv' a b f $== Id b
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B) 
(f : a $-> b) (g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a -> ?CatIsEquiv' a b f
  1:{
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall a b : Fun01 A B, (a $-> b) -> Type intros [F ?] [G ?] [alpha ?]; cbn in *.
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
is1natural_nattrans: Is1Natural F G alpha
Type
      exact (forall a, CatIsEquiv (alpha a)). }
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall a b : Fun01 A B,
(fun X : Fun01 A B =>
 (fun (F : A -> B) (fun01_is0functor0 : Is0Functor F)
    (X0 : Fun01 A B) =>
  (fun (G : A -> B) (fun01_is0functor1 : Is0Functor G)
   => NatEquiv F G) X0 
    (fun01_is0functor A B X0)) X
   (fun01_is0functor A B X)) a b -> 
a $-> b
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B)
(f : (fun X : Fun01 A B =>
      (fun (F : A -> B)
         (fun01_is0functor0 : Is0Functor F)
         (X0 : Fun01 A B) =>
       (fun (G : A -> B)
          (fun01_is0functor1 : Is0Functor G) =>
        NatEquiv F G) X0 
         (fun01_is0functor A B X0)) X
        (fun01_is0functor A B X)) a b),
(fun a0 : Fun01 A B =>
 (fun (F : A -> B) (fun01_is0functor0 : Is0Functor F)
    (b0 : Fun01 A B) =>
  (fun (G : A -> B) (fun01_is0functor1 : Is0Functor G)
     (X : {|
            fun01_F := F;
            fun01_is0functor := fun01_is0functor0
          |} $->
          {|
            fun01_F := G;
            fun01_is0functor := fun01_is0functor1
          |}) =>
   (fun (alpha : F $=> G) (_ : Is1Natural F G alpha)
    => (forall a1 : A, CatIsEquiv (alpha a1)) : Type)
     X (is1natural_nattrans X)) b0
    (fun01_is0functor A B b0)) a0
   (fun01_is0functor A B a0)) a b 
  (?cate_fun' a b f)
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B) 
(f : a $-> b),
(fun a0 : Fun01 A B =>
 (fun (F : A -> B) (fun01_is0functor0 : Is0Functor F)
    (b0 : Fun01 A B) =>
  (fun (G : A -> B) (fun01_is0functor1 : Is0Functor G)
     (X : {|
            fun01_F := F;
            fun01_is0functor := fun01_is0functor0
          |} $->
          {|
            fun01_F := G;
            fun01_is0functor := fun01_is0functor1
          |}) =>
   (fun (alpha : F $=> G) (_ : Is1Natural F G alpha)
    => (forall a1 : A, CatIsEquiv (alpha a1)) : Type)
     X (is1natural_nattrans X)) b0
    (fun01_is0functor A B b0)) a0
   (fun01_is0functor A B a0)) a b f ->
(fun X : Fun01 A B =>
 (fun (F : A -> B) (fun01_is0functor0 : Is0Functor F)
    (X0 : Fun01 A B) =>
  (fun (G : A -> B) (fun01_is0functor1 : Is0Functor G)
   => NatEquiv F G) X0 
    (fun01_is0functor A B X0)) X
   (fun01_is0functor A B X)) a b
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B) 
(f : a $-> b)
(fe : (fun a0 : Fun01 A B =>
       (fun (F : A -> B)
          (fun01_is0functor0 : Is0Functor F)
          (b0 : Fun01 A B) =>
        (fun (G : A -> B)
           (fun01_is0functor1 : Is0Functor G)
           (X : {|
                  fun01_F := F;
                  fun01_is0functor :=
                    fun01_is0functor0
                |} $->
                {|
                  fun01_F := G;
                  fun01_is0functor :=
                    fun01_is0functor1
                |}) =>
         (fun (alpha : F $=> G)
            (_ : Is1Natural F G alpha) =>
          (forall a1 : A, CatIsEquiv (alpha a1))
          :
          Type) X (is1natural_nattrans X)) b0
          (fun01_is0functor A B b0)) a0
         (fun01_is0functor A B a0)) a b f),
?cate_fun' a b (?cate_buildequiv' a b f fe) $== f
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall a b : Fun01 A B,
(fun X : Fun01 A B =>
 (fun (F : A -> B) (fun01_is0functor0 : Is0Functor F)
    (X0 : Fun01 A B) =>
  (fun (G : A -> B) (fun01_is0functor1 : Is0Functor G)
   => NatEquiv F G) X0 
    (fun01_is0functor A B X0)) X
   (fun01_is0functor A B X)) a b -> 
b $-> a
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B)
(f : (fun X : Fun01 A B =>
      (fun (F : A -> B)
         (fun01_is0functor0 : Is0Functor F)
         (X0 : Fun01 A B) =>
       (fun (G : A -> B)
          (fun01_is0functor1 : Is0Functor G) =>
        NatEquiv F G) X0 
         (fun01_is0functor A B X0)) X
        (fun01_is0functor A B X)) a b),
?cate_inv' a b f $o ?cate_fun' a b f $== Id a
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B)
(f : (fun X : Fun01 A B =>
      (fun (F : A -> B)
         (fun01_is0functor0 : Is0Functor F)
         (X0 : Fun01 A B) =>
       (fun (G : A -> B)
          (fun01_is0functor1 : Is0Functor G) =>
        NatEquiv F G) X0 
         (fun01_is0functor A B X0)) X
        (fun01_is0functor A B X)) a b),
?cate_fun' a b f $o ?cate_inv' a b f $== Id b
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : Fun01 A B) 
(f : a $-> b) (g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a ->
(fun a0 : Fun01 A B =>
 (fun (F : A -> B) (fun01_is0functor0 : Is0Functor F)
    (b0 : Fun01 A B) =>
  (fun (G : A -> B) (fun01_is0functor1 : Is0Functor G)
     (X : {|
            fun01_F := F;
            fun01_is0functor := fun01_is0functor0
          |} $->
          {|
            fun01_F := G;
            fun01_is0functor := fun01_is0functor1
          |}) =>
   (fun (alpha : F $=> G) (_ : Is1Natural F G alpha)
    => (forall a1 : A, CatIsEquiv (alpha a1)) : Type)
     X (is1natural_nattrans X)) b0
    (fun01_is0functor A B b0)) a0
   (fun01_is0functor A B a0)) a b f
  all:intros [F ?] [G ?] [alpha alnat]; cbn in *.
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
NatTrans F G
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
forall a : A, CatIsEquiv (?Goal a)
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
alnat: Is1Natural F G alpha
(forall a : A, CatIsEquiv (alpha a)) -> NatEquiv F G
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
alnat: Is1Natural F G alpha
forall (fe : forall a : A, CatIsEquiv (alpha a))
(a : A),
?Goal@{alpha:=cat_equiv_natequiv (?Goal1 fe);
       alnat:=is1natural_natequiv (?Goal1 fe)} a $==
alpha a
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
NatTrans G F
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
forall a : A,
trans_comp ?Goal3 ?Goal a $== id_transformation F a
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
forall a : A,
trans_comp ?Goal ?Goal3 a $== id_transformation G a
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
alnat: Is1Natural F G alpha
forall g : NatTrans G F,
(forall a : A,
 trans_comp alpha g a $== id_transformation G a) ->
(forall a : A,
 trans_comp g alpha a $== id_transformation F a) ->
forall a : A, CatIsEquiv (alpha a)
  -
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
NatTrans F G exists (fun a => alpha a); assumption.
  -
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
forall a : A,
CatIsEquiv
  ({|
     trans_nattrans := fun a0 : A => alpha a0;
     is1natural_nattrans := alnat
   |} a) intros a; exact _.
  -
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
alnat: Is1Natural F G alpha
(forall a : A, CatIsEquiv (alpha a)) -> NatEquiv F G intros ?.
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
alnat: Is1Natural F G alpha
X: forall a : A, CatIsEquiv (alpha a)
NatEquiv F G
    snrapply Build_NatEquiv.
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
alnat: Is1Natural F G alpha
X: forall a : A, CatIsEquiv (alpha a)
forall a : A, F a $<~> G a
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
alnat: Is1Natural F G alpha
X: forall a : A, CatIsEquiv (alpha a)
Is1Natural F G (fun a : A => ?e a)
    +
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
alnat: Is1Natural F G alpha
X: forall a : A, CatIsEquiv (alpha a)
forall a : A, F a $<~> G a intros a; exact (Build_CatEquiv (alpha a)).
    +
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
alnat: Is1Natural F G alpha
X: forall a : A, CatIsEquiv (alpha a)
Is1Natural F G
  (fun a : A =>
   (fun a0 : A => Build_CatEquiv (alpha a0)) a) cbn.
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
alnat: Is1Natural F G alpha
X: forall a : A, CatIsEquiv (alpha a)
Is1Natural F G (fun a : A => Build_CatEquiv (alpha a)) refine (is1natural_homotopic alpha _).
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
alnat: Is1Natural F G alpha
X: forall a : A, CatIsEquiv (alpha a)
forall a : A, Build_CatEquiv (alpha a) $== alpha a
      intros a; apply cate_buildequiv_fun.
  -
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
alnat: Is1Natural F G alpha
forall (fe : forall a : A, CatIsEquiv (alpha a))
(a : A),
{|
  trans_nattrans :=
    fun a0 : A =>
    (fun X : forall a1 : A, CatIsEquiv (alpha a1) =>
     {|
       cat_equiv_natequiv :=
         fun a1 : A => Build_CatEquiv (alpha a1);
       is1natural_natequiv :=
         is1natural_homotopic alpha
           (fun a1 : A =>
            cate_buildequiv_fun (alpha a1))
         :
         Is1Natural F G
           (fun a1 : A =>
            (fun a2 : A => Build_CatEquiv (alpha a2))
              a1)
     |}) fe a0;
  is1natural_nattrans :=
    is1natural_natequiv
      ((fun X : forall a0 : A, CatIsEquiv (alpha a0)
        =>
        {|
          cat_equiv_natequiv :=
            fun a0 : A => Build_CatEquiv (alpha a0);
          is1natural_natequiv :=
            is1natural_homotopic alpha
              (fun a0 : A =>
               cate_buildequiv_fun (alpha a0))
            :
            Is1Natural F G
              (fun a0 : A =>
               (fun a1 : A =>
                Build_CatEquiv (alpha a1)) a0)
        |}) fe)
|} a $== alpha a cbn; intros; apply cate_buildequiv_fun.
  -
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
NatTrans G F exists (fun a => (alpha a)^-1$).
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
Is1Natural G F (fun a : A => (alpha a)^-1$)
    intros a b f.
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
a, b: A
f: a $-> b
(alpha b)^-1$ $o fmap G f $==
fmap F f $o (alpha a)^-1$
    refine ((cat_idr _)^$ $@ _).
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
a, b: A
f: a $-> b
(alpha b)^-1$ $o fmap G f $o Id (G a) $==
fmap F f $o (alpha a)^-1$
    refine ((_ $@L (cate_isretr (alpha a))^$) $@ _).
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
a, b: A
f: a $-> b
(alpha b)^-1$ $o fmap G f $o
(alpha a $o (alpha a)^-1$) $==
fmap F f $o (alpha a)^-1$
    refine (cat_assoc _ _ _ $@ _).
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
a, b: A
f: a $-> b
(alpha b)^-1$ $o
(fmap G f $o (alpha a $o (alpha a)^-1$)) $==
fmap F f $o (alpha a)^-1$
    refine ((_ $@L (cat_assoc_opp _ _ _)) $@ _).
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
a, b: A
f: a $-> b
(alpha b)^-1$ $o
(fmap G f $o alpha a $o (alpha a)^-1$) $==
fmap F f $o (alpha a)^-1$
    refine ((_ $@L ((isnat (fun a => alpha a) f)^$ $@R _)) $@ _).
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
a, b: A
f: a $-> b
(alpha b)^-1$ $o
(alpha b $o fmap F f $o (alpha a)^-1$) $==
fmap F f $o (alpha a)^-1$
    refine ((_ $@L (cat_assoc _ _ _)) $@ _).
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
a, b: A
f: a $-> b
(alpha b)^-1$ $o
(alpha b $o (fmap F f $o (alpha a)^-1$)) $==
fmap F f $o (alpha a)^-1$
    refine (cat_assoc_opp _ _ _ $@ _).
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
a, b: A
f: a $-> b
(alpha b)^-1$ $o alpha b $o
(fmap F f $o (alpha a)^-1$) $==
fmap F f $o (alpha a)^-1$
    refine ((cate_issect (alpha b) $@R _) $@ _).
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
a, b: A
f: a $-> b
Id (F b) $o (fmap F f $o (alpha a)^-1$) $==
fmap F f $o (alpha a)^-1$
    exact (cat_idl _).
  -
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
forall a : A,
trans_comp
  {|
    trans_nattrans := fun a0 : A => (alpha a0)^-1$;
    is1natural_nattrans :=
      (fun (a0 b : A) (f : a0 $-> b) =>
       (cat_idr ((alpha b)^-1$ $o fmap G f))^$ $@
       ((((alpha b)^-1$ $o fmap G f) $@L
         (cate_isretr (alpha a0))^$) $@
        (cat_assoc (alpha a0 $o (alpha a0)^-1$)
           (fmap G f) (alpha b)^-1$ $@
         (((alpha b)^-1$ $@L
           cat_assoc_opp 
             (alpha a0)^-1$ 
             (alpha a0) 
             (fmap G f)) $@
          (((alpha b)^-1$ $@L
            ((isnat (fun ... => alpha a1) f)^$ $@R
             (alpha a0)^-1$)) $@
           (((alpha b)^-1$ $@L
             cat_assoc 
               (alpha a0)^-1$ 
               (fmap F f) 
               (alpha b)) $@
            (cat_assoc_opp
               (fmap F f $o (alpha a0)^-1$) 
               (alpha b) 
               (alpha b)^-1$ $@
             ((cate_issect ... $@R (...)) $@
              cat_idl (... $o ...^-1$)))))))))
      :
      Is1Natural G F (fun a0 : A => (alpha a0)^-1$)
  |}
  {|
    trans_nattrans := fun a0 : A => alpha a0;
    is1natural_nattrans := alnat
  |} a $== id_transformation F a intros; apply cate_issect.
  -
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
alnat: Is1Natural F G (fun a : A => alpha a)
forall a : A,
trans_comp
  {|
    trans_nattrans := fun a0 : A => alpha a0;
    is1natural_nattrans := alnat
  |}
  {|
    trans_nattrans := fun a0 : A => (alpha a0)^-1$;
    is1natural_nattrans :=
      (fun (a0 b : A) (f : a0 $-> b) =>
       (cat_idr ((alpha b)^-1$ $o fmap G f))^$ $@
       ((((alpha b)^-1$ $o fmap G f) $@L
         (cate_isretr (alpha a0))^$) $@
        (cat_assoc (alpha a0 $o (alpha a0)^-1$)
           (fmap G f) (alpha b)^-1$ $@
         (((alpha b)^-1$ $@L
           cat_assoc_opp 
             (alpha a0)^-1$ 
             (alpha a0) 
             (fmap G f)) $@
          (((alpha b)^-1$ $@L
            ((isnat (fun ... => alpha a1) f)^$ $@R
             (alpha a0)^-1$)) $@
           (((alpha b)^-1$ $@L
             cat_assoc 
               (alpha a0)^-1$ 
               (fmap F f) 
               (alpha b)) $@
            (cat_assoc_opp
               (fmap F f $o (alpha a0)^-1$) 
               (alpha b) 
               (alpha b)^-1$ $@
             ((cate_issect ... $@R (...)) $@
              cat_idl (... $o ...^-1$)))))))))
      :
      Is1Natural G F (fun a0 : A => (alpha a0)^-1$)
  |} a $== id_transformation G a intros; apply cate_isretr.
  -
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
alnat: Is1Natural F G alpha
forall g : NatTrans G F,
(forall a : A,
 trans_comp alpha g a $== id_transformation G a) ->
(forall a : A,
 trans_comp g alpha a $== id_transformation F a) ->
forall a : A, CatIsEquiv (alpha a) intros [gamma ?] r s a; cbn in *.
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F: A -> B
fun01_is0functor0: Is0Functor F
G: A -> B
fun01_is0functor1: Is0Functor G
alpha: F $=> G
alnat: Is1Natural F G alpha
gamma: G $=> F
is1natural_nattrans: Is1Natural G F gamma
r: forall a : A,
trans_comp alpha gamma a $== id_transformation G a
s: forall a : A,
trans_comp gamma alpha a $== id_transformation F a
a: A
CatIsEquiv (alpha a)
    refine (catie_adjointify (alpha a) (gamma a) (r a) (s a)).
Defined.

(** Bundled opposite functors *)
Definition fun01_op (A B : Type) `{IsGraph A} `{IsGraph B}
  : Fun01 A B -> Fun01 A^op B^op.
A, B: Type
H: IsGraph A
H0: IsGraph B
Fun01 A B -> Fun01 A^op B^op
Proof.
A, B: Type
H: IsGraph A
H0: IsGraph B
Fun01 A B -> Fun01 A^op B^op
  intros F.
A, B: Type
H: IsGraph A
H0: IsGraph B
F: Fun01 A B
Fun01 A^op B^op
  rapply (Build_Fun01 A^op B^op F).
Defined.

(** ** Categories of 1-coherent 1-functors *)

Record Fun11 (A B : Type) `{Is1Cat A} `{Is1Cat B} :=
{
  fun11_fun : A -> B ;
  is0functor_fun11 : Is0Functor fun11_fun ;
  is1functor_fun11 : Is1Functor fun11_fun
}.

Coercion fun11_fun : Fun11 >-> Funclass.
Global Existing Instance is0functor_fun11.
Global Existing Instance is1functor_fun11.

Arguments Build_Fun11 A B
  {isgraph_A is2graph_A is01cat_A is1cat_A
   isgraph_B is2graph_B is01cat_B is1cat_B}
  F {is0functor_fun11 is1functor_fun11} : rename.

Coercion fun01_fun11 {A B : Type} `{Is1Cat A} `{Is1Cat B}
           (F : Fun11 A B)
  : Fun01 A B.
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
F: Fun11 A B
Fun01 A B
Proof.
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
F: Fun11 A B
Fun01 A B
  exists F; exact _.
Defined.

Global Instance isgraph_fun11 {A B : Type} `{Is1Cat A} `{Is1Cat B}
  : IsGraph (Fun11 A B)
  := isgraph_induced fun01_fun11.

Global Instance is01cat_fun11 {A B : Type} `{Is1Cat A} `{Is1Cat B}
  : Is01Cat (Fun11 A B)
  := is01cat_induced fun01_fun11.

Global Instance is2graph_fun11 {A B : Type} `{Is1Cat A, Is1Cat B}
  : Is2Graph (Fun11 A B)
  := is2graph_induced fun01_fun11.

Global Instance is1cat_fun11 {A B :Type} `{Is1Cat A} `{Is1Cat B}
  : Is1Cat (Fun11 A B)
  := is1cat_induced fun01_fun11.

Global Instance hasequivs_fun11 {A B : Type} `{Is1Cat A} `{HasEquivs B}
  : HasEquivs (Fun11 A B)
  := hasequivs_induced fun01_fun11.

(** * Identity functors *)

Definition fun01_id {A} `{IsGraph A} : Fun01 A A
  := Build_Fun01 A A idmap.

Definition fun11_id {A} `{Is1Cat A} : Fun11 A A
  := Build_Fun11 _ _ idmap.

(** * Composition of functors *)

Definition fun01_compose {A B C} `{IsGraph A, IsGraph B, IsGraph C}
  : Fun01 B C -> Fun01 A B -> Fun01 A C
  := fun G F => Build_Fun01 _ _ (G o F).

Definition fun01_postcomp {A B C}
  `{IsGraph A, Is1Cat B, Is1Cat C} (F : Fun11 B C)
  : Fun01 A B -> Fun01 A C
  := fun01_compose (A:=A) F.

(** Warning: [F] needs to be a 1-functor for this to be a 0-functor. *)
Global Instance is0functor_fun01_postcomp {A B C}
  `{IsGraph A, Is1Cat B, Is1Cat C} (F : Fun11 B C)
  : Is0Functor (fun01_postcomp (A:=A) F).
A, B, C: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
Is0Functor (fun01_postcomp F)
Proof.
A, B, C: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
Is0Functor (fun01_postcomp F)
  apply Build_Is0Functor.
A, B, C: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
forall a b : Fun01 A B,
(a $-> b) -> fun01_postcomp F a $-> fun01_postcomp F b
  intros a b f.
A, B, C: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
a, b: Fun01 A B
f: a $-> b
fun01_postcomp F a $-> fun01_postcomp F b
  rapply nattrans_postwhisker.
A, B, C: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
a, b: Fun01 A B
f: a $-> b
NatTrans a b
  exact f.
Defined.

Global Instance is1functor_fun01_postcomp {A B C}
  `{IsGraph A, Is1Cat B, Is1Cat C} (F : Fun11 B C)
  : Is1Functor (fun01_postcomp (A:=A) F).
A, B, C: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
Is1Functor (fun01_postcomp F)
Proof.
A, B, C: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
Is1Functor (fun01_postcomp F)
  apply Build_Is1Functor.
A, B, C: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
forall (a b : Fun01 A B) 
(f g : a $-> b),
f $== g ->
fmap (fun01_postcomp F) f $==
fmap (fun01_postcomp F) g
A, B, C: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
forall a : Fun01 A B,
fmap (fun01_postcomp F) (Id a) $==
Id (fun01_postcomp F a)
A, B, C: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
forall (a b c : Fun01 A B) 
(f : a $-> b) (g : b $-> c),
fmap (fun01_postcomp F) (g $o f) $==
fmap (fun01_postcomp F) g $o fmap (fun01_postcomp F) f
  -
A, B, C: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
forall (a b : Fun01 A B) 
(f g : a $-> b),
f $== g ->
fmap (fun01_postcomp F) f $==
fmap (fun01_postcomp F) g intros a b f g p x.
A, B, C: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
a, b: Fun01 A B
f, g: a $-> b
p: f $== g
x: A
fmap (fun01_postcomp F) f x $==
fmap (fun01_postcomp F) g x
    rapply fmap2.
A, B, C: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
a, b: Fun01 A B
f, g: a $-> b
p: f $== g
x: A
f x $== g x
    rapply p.
  -
A, B, C: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
forall a : Fun01 A B,
fmap (fun01_postcomp F) (Id a) $==
Id (fun01_postcomp F a) intros f x.
A, B, C: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
f: Fun01 A B
x: A
fmap (fun01_postcomp F) (Id f) x $==
Id (fun01_postcomp F f) x
    rapply fmap_id.
  -
A, B, C: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
forall (a b c : Fun01 A B) 
(f : a $-> b) (g : b $-> c),
fmap (fun01_postcomp F) (g $o f) $==
fmap (fun01_postcomp F) g $o fmap (fun01_postcomp F) f intros a b c f g x.
A, B, C: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
a, b, c: Fun01 A B
f: a $-> b
g: b $-> c
x: A
fmap (fun01_postcomp F) (g $o f) x $==
(fmap (fun01_postcomp F) g $o
 fmap (fun01_postcomp F) f) x
    rapply fmap_comp.
Defined.

Definition fun11_fun01_postcomp {A B C}
  `{IsGraph A, Is1Cat B, Is1Cat C} (F : Fun11 B C)
  : Fun11 (Fun01 A B) (Fun01 A C)
  := Build_Fun11 _ _ (fun01_postcomp F).

Definition fun11_compose {A B C} `{Is1Cat A, Is1Cat B, Is1Cat C}
  : Fun11 B C -> Fun11 A B -> Fun11 A C.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Fun11 B C -> Fun11 A B -> Fun11 A C
Proof.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Fun11 B C -> Fun11 A B -> Fun11 A C
  intros F G.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
G: Fun11 A B
Fun11 A C
  nrapply Build_Fun11.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: Fun11 B C
G: Fun11 A B
Is1Functor ?Goal
  rapply (is1functor_compose G F).
Defined.