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.

Arguments Build_Fun01 A B {isgraph_A isgraph_B} F {fun01_is0functor} : rename.
Arguments fun01_F {A B isgraph_A isgraph_B} : 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. *)

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.

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
    exact (nattrans_id F).
  -
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, G, K: Fun01 A B
gamma: NatTrans G K
alpha: NatTrans F G
NatTrans F K
    exact (nattrans_comp gamma alpha).
Defined.

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

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 (trans_id 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 (trans_id 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. *)

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: intros F G; 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 F G : Fun01 A B => NatEquiv F G) 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 F G : Fun01 A B => NatEquiv F G) 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 F G : Fun01 A B => NatEquiv F G) 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 F G : Fun01 A B => NatEquiv F G) 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 F G : Fun01 A B => NatEquiv F G) 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 F G : Fun01 A B => NatEquiv F G) 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
  all: 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, G: Fun01 A B
alpha: NatTrans F G
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
F, G: Fun01 A B
alpha: NatEquiv F G
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, G: Fun01 A B
alpha: NatEquiv F G
?Goal@{alpha:=?Goal0}
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, G: Fun01 A B
alpha: NatTrans F G
?Goal -> 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, G: Fun01 A B
alpha: NatTrans F G
forall (fe : ?Goal) (a : A),
?Goal0@{alpha:=?Goal2 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, G: Fun01 A B
alpha: NatEquiv F G
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, G: Fun01 A B
alpha: NatEquiv F G
forall a : A,
trans_comp ?Goal4 ?Goal0 a $== trans_id 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, G: Fun01 A B
alpha: NatEquiv F G
forall a : A,
trans_comp ?Goal0 ?Goal4 a $== trans_id 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, G: Fun01 A B
alpha: NatTrans F G
forall g : NatTrans G F,
(forall a : A, trans_comp alpha g a $== trans_id G a) ->
(forall a : A, trans_comp g alpha a $== trans_id F a) ->
?Goal
  -
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, G: Fun01 A B
alpha: NatTrans F G
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
F, G: Fun01 A B
alpha: NatEquiv F G
NatTrans F G exact 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, G: Fun01 A B
alpha: NatEquiv F G
forall a : A, CatIsEquiv (alpha 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, G: Fun01 A B
alpha: NatTrans F G
(forall a : A, CatIsEquiv (alpha a)) -> NatEquiv F G apply 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, G: Fun01 A B
alpha: NatTrans F G
forall (fe : forall a : A, CatIsEquiv (alpha a))
(a : A), Build_NatEquiv' alpha 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, G: Fun01 A B
alpha: NatEquiv F G
NatTrans G F exact (natequiv_inverse 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, G: Fun01 A B
alpha: NatEquiv F G
forall a : A,
trans_comp (natequiv_inverse alpha) alpha a $==
trans_id 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, G: Fun01 A B
alpha: NatEquiv F G
forall a : A,
trans_comp alpha (natequiv_inverse alpha) a $==
trans_id 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, G: Fun01 A B
alpha: NatTrans F G
forall g : NatTrans G F,
(forall a : A, trans_comp alpha g a $== trans_id G a) ->
(forall a : A, trans_comp g alpha a $== trans_id 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, G: Fun01 A B
alpha: NatTrans F G
gamma: G $=> F
is1natural_nattrans: Is1Natural G F gamma
r: forall a : A,
trans_comp alpha gamma a $== trans_id G a
s: forall a : A,
trans_comp gamma alpha a $== trans_id F a
a: A
CatIsEquiv (alpha a)
    exact (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
  exact (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.

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.

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

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

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

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

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. *)
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
  napply 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
Is1Functor 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
NatTrans a b
  1: exact _.
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.

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
  napply 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
  exact (is1functor_compose G F).
Defined.