Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
(* -*- mode: coq; mode: visual-line -*- *)
[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 *)RecordFun01 (AB : Type) `{IsGraph A} `{IsGraph B} := {
fun01_F : A -> B;
fun01_is0functor : Is0Functor fun01_F;
}.Coercionfun01_F : Fun01 >-> Funclass.Global Existing Instancefun01_is0functor.Arguments Build_Fun01 A B {isgraph_A isgraph_B} F {fun01_is0functor} : rename.Definitionissig_Fun01 (AB : 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. *)
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: 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)
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
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.
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: 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)
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B
foralla : Fun01 A B, a $-> a
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B
forallabc : 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
foralla : Fun01 A B, 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
NatTrans F F
exists (id_transformationF); exact _.
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B
forallabc : 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 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_compgammaalpha); exact _.Defined.
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: 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)
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
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 (foralla, 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. *)
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: 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)
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B
forallab : Fun01 A B, Is01Cat (a $-> b)
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B
forallab : 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 (abc : 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 (abc : 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 (abcd : 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 (abcd : 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 (ab : 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 (ab : 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
forallab : Fun01 A B, Is01Cat (a $-> b)
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
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
forallabc : {|
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
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
forallabc : {|
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 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
forallab : Fun01 A B, Is0Gpd (a $-> b)
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
forallab : {|
fun01_F := F;
fun01_is0functor := fun01_is0functor0
|} $->
{|
fun01_F := G;
fun01_is0functor := fun01_is0functor1
|}, (a $-> b) -> b $-> 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 (abc : 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 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
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
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
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B
forall (abc : 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 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
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
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
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B
forall (abcd : 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 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 (abcd : 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 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 (ab : 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 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 (ab : 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 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. *)
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)
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)
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
forallab : 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
forallab : 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 (ab : 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 (ab : 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 (ab : 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
forallab : 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 (ab : 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 (ab : 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 (ab : Fun01 A B)
(f : a $-> b) (g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a -> ?CatIsEquiv' 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
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 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
forallab : 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
forallab : Fun01 A B,
(funX : 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 (ab : Fun01 A B)
(f : (funX : 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 (ab : Fun01 A B)
(f : a $-> b),
?CatIsEquiv' a b f ->
(funX : 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 (ab : 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
forallab : Fun01 A B,
(funX : 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 (ab : Fun01 A B)
(f : (funX : 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 (ab : Fun01 A B)
(f : (funX : 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 (ab : Fun01 A B)
(f : a $-> b) (g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a -> ?CatIsEquiv' 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
forallab : 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 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 (foralla, 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
forallab : Fun01 A B,
(funX : 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 (ab : Fun01 A B)
(f : (funX : 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),
(funa0 : 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)
=> (foralla1 : 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 (ab : Fun01 A B)
(f : a $-> b),
(funa0 : 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)
=> (foralla1 : A, CatIsEquiv (alpha a1)) : Type)
X (is1natural_nattrans X)) b0
(fun01_is0functor A B b0)) a0
(fun01_is0functor A B a0)) a b f ->
(funX : 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 (ab : Fun01 A B)
(f : a $-> b)
(fe : (funa0 : 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) =>
(foralla1 : 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
forallab : Fun01 A B,
(funX : 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 (ab : Fun01 A B)
(f : (funX : 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 (ab : Fun01 A B)
(f : (funX : 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 (ab : Fun01 A B)
(f : a $-> b) (g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a ->
(funa0 : 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)
=> (foralla1 : A, CatIsEquiv (alpha a1)) : Type)
X (is1natural_nattrans X)) b0
(fun01_is0functor A B b0)) a0
(fun01_is0functor A B a0)) 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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : 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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : A => alpha a)
foralla : 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
(foralla : 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 : foralla : 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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : 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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : A => alpha a)
foralla : 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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : A => alpha a)
foralla : 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
forallg : NatTrans G F,
(foralla : A,
trans_comp alpha g a $== id_transformation G a) ->
(foralla : A,
trans_comp g alpha a $== id_transformation F a) ->
foralla : 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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : A => alpha a)
NatTrans F G
exists (funa => 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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : A => alpha a)
foralla : A,
CatIsEquiv
({|
trans_nattrans := funa0 : 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
(foralla : 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 X: foralla : 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 X: foralla : A, CatIsEquiv (alpha a)
foralla : 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: foralla : A, CatIsEquiv (alpha a)
Is1Natural F G (funa : 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: foralla : A, CatIsEquiv (alpha a)
foralla : 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: foralla : A, CatIsEquiv (alpha a)
Is1Natural F G
(funa : A =>
(funa0 : A => Build_CatEquiv (alpha a0)) 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: foralla : A, CatIsEquiv (alpha a)
Is1Natural F G (funa : A => 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: foralla : A, CatIsEquiv (alpha a)
foralla : 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 : foralla : A, CatIsEquiv (alpha a))
(a : A),
{|
trans_nattrans :=
funa0 : A =>
(funX : foralla1 : A, CatIsEquiv (alpha a1) =>
{|
cat_equiv_natequiv :=
funa1 : A => Build_CatEquiv (alpha a1);
is1natural_natequiv :=
is1natural_homotopic alpha
(funa1 : A =>
cate_buildequiv_fun (alpha a1))
:
Is1Natural F G
(funa1 : A =>
(funa2 : A => Build_CatEquiv (alpha a2))
a1)
|}) fe a0;
is1natural_nattrans :=
is1natural_natequiv
((funX : foralla0 : A, CatIsEquiv (alpha a0)
=>
{|
cat_equiv_natequiv :=
funa0 : A => Build_CatEquiv (alpha a0);
is1natural_natequiv :=
is1natural_homotopic alpha
(funa0 : A =>
cate_buildequiv_fun (alpha a0))
:
Is1Natural F G
(funa0 : A =>
(funa1 : 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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : 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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : A => alpha a)
Is1Natural G F (funa : 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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : A => alpha a) a, b: A f: a $-> b
(alpha b)^-1$ $o fmap G f $==
fmap F f $o (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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : 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$
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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : 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$
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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : 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$
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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : 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$
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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : 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$
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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : 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$
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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : 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$
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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : 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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : A => alpha a)
foralla : A,
trans_comp
{|
trans_nattrans := funa0 : A => (alpha a0)^-1$;
is1natural_nattrans :=
(fun (a0b : 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 (funa0 : A => (alpha a0)^-1$)
|}
{|
trans_nattrans := funa0 : 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: foralla : A, F a $<~> G a alnat: Is1Natural F G (funa : A => alpha a)
foralla : A,
trans_comp
{|
trans_nattrans := funa0 : A => alpha a0;
is1natural_nattrans := alnat
|}
{|
trans_nattrans := funa0 : A => (alpha a0)^-1$;
is1natural_nattrans :=
(fun (a0b : 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 (funa0 : 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
forallg : NatTrans G F,
(foralla : A,
trans_comp alpha g a $== id_transformation G a) ->
(foralla : A,
trans_comp g alpha a $== id_transformation F a) ->
foralla : 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: F $=> G alnat: Is1Natural F G alpha gamma: G $=> F is1natural_nattrans: Is1Natural G F gamma r: foralla : A,
trans_comp alpha gamma a $== id_transformation G a s: foralla : 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 *)
A, B: Type H: IsGraph A H0: 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
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 *)RecordFun11 (AB : Type) `{Is1Cat A} `{Is1Cat B} :=
{
fun11_fun : A -> B ;
is0functor_fun11 : Is0Functor fun11_fun ;
is1functor_fun11 : Is1Functor fun11_fun
}.Coercionfun11_fun : Fun11 >-> Funclass.Global Existing Instanceis0functor_fun11.Global Existing Instanceis1functor_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.
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
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
existsF; exact _.Defined.Global Instanceisgraph_fun11 {AB : Type} `{Is1Cat A} `{Is1Cat B}
: IsGraph (Fun11 A B)
:= isgraph_induced fun01_fun11.Global Instanceis01cat_fun11 {AB : Type} `{Is1Cat A} `{Is1Cat B}
: Is01Cat (Fun11 A B)
:= is01cat_induced fun01_fun11.Global Instanceis2graph_fun11 {AB : Type} `{Is1Cat A, Is1Cat B}
: Is2Graph (Fun11 A B)
:= is2graph_induced fun01_fun11.Global Instanceis1cat_fun11 {AB :Type} `{Is1Cat A} `{Is1Cat B}
: Is1Cat (Fun11 A B)
:= is1cat_induced fun01_fun11.Global Instancehasequivs_fun11 {AB : Type} `{Is1Cat A} `{HasEquivs B}
: HasEquivs (Fun11 A B)
:= hasequivs_induced fun01_fun11.(** * Identity functors *)Definitionfun01_id {A} `{IsGraph A} : Fun01 A A
:= Build_Fun01 A A idmap.Definitionfun11_id {A} `{Is1Cat A} : Fun11 A A
:= Build_Fun11 _ _ idmap.(** * Composition of functors *)Definitionfun01_compose {ABC} `{IsGraph A, IsGraph B, IsGraph C}
: Fun01 B C -> Fun01 A B -> Fun01 A C
:= funGF => Build_Fun01 _ _ (G o F).Definitionfun01_postcomp {ABC}
`{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. *)
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)
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)
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
forallab : Fun01 A B,
(a $-> b) -> fun01_postcomp F a $-> fun01_postcomp F b
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
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.
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)
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)
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 (ab : Fun01 A B)
(fg : 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
foralla : 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 (abc : 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 (ab : Fun01 A B)
(fg : 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 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
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
foralla : 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 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 (abc : 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 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.Definitionfun11_fun01_postcomp {ABC}
`{IsGraph A, Is1Cat B, Is1Cat C} (F : Fun11 B C)
: Fun11 (Fun01 A B) (Fun01 A C)
:= Build_Fun11 _ _ (fun01_postcomp F).
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
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
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
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