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.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.Core.Require Import WildCat.Equiv.Require Import WildCat.Square.Require Import WildCat.Opposite.(** ** Natural transformations *)DefinitionTransformation {A : Type} {B : A -> Type} `{forallx, IsGraph (B x)}
(F G : forall (x : A), B x)
:= forall (a : A), F a $-> G a.(** This lets us apply transformations to things. Identity Coercion tells coq that this coercion is in fact definitionally the identity map so it doesn't need to insert it, but merely rewrite definitionally when typechecking. *)Identity Coercionfun_trans : Transformation >-> Funclass.Notation"F $=> G" := (Transformation F G).(** A 1-natural transformation is natural up to a 2-cell, so its codomain must be a 1-category. *)ClassIs1Natural {AB : Type} `{IsGraph A} `{Is1Cat B}
(F : A -> B) `{!Is0Functor F} (G : A -> B) `{!Is0Functor G}
(alpha : F $=> G) :=
isnat : forallaa' (f : a $-> a'),
(alpha a') $o (fmap F f) $== (fmap G f) $o (alpha a).Arguments Is1Natural {A B} {isgraph_A}
{isgraph_B} {is2graph_B} {is01cat_B} {is1cat_B}
F {is0functor_F} G {is0functor_G} alpha : rename.Arguments isnat {_ _ _ _ _ _ _ _ _ _ _} alpha {alnat _ _} f : rename.RecordNatTrans {AB : Type} `{IsGraph A} `{Is1Cat B} {F G : A -> B}
{ff : Is0Functor F} {fg : Is0Functor G} :=
{
trans_nattrans : F $=> G ;
is1natural_nattrans : Is1Natural F G trans_nattrans ;
}.Arguments NatTrans {A B} {isgraph_A}
{isgraph_B} {is2graph_B} {is01cat_B} {is1cat_B}
F G {is0functor_F} {is0functor_G} : rename.Arguments Build_NatTrans {A B} {isgraph_A}
{isgraph_B} {is2graph_B} {is01cat_B} {is1cat_B}
F G {is0functor_F} {is0functor_G} alpha isnat_alpha: rename.Global Existing Instanceis1natural_nattrans.Coerciontrans_nattrans : NatTrans >-> Transformation.Definitionissig_NatTrans {AB : Type} `{IsGraph A} `{Is1Cat B} (F G : A -> B)
{ff : Is0Functor F} {fg : Is0Functor G}
: _ <~> NatTrans F G := ltac:(issig).(** The transposed natural square *)Definitionisnat_tr {AB : Type} `{IsGraph A} `{Is1Cat B}
{F : A -> B} `{!Is0Functor F} {G : A -> B} `{!Is0Functor G}
(alpha : F $=> G) `{!Is1Natural F G alpha}
{a a' : A} (f : a $-> a')
: (fmap G f) $o (alpha a) $== (alpha a') $o (fmap F f)
:= (isnat alpha f)^$.Definitionid_transformation {AB : Type} `{Is01Cat B} (F : A -> B)
: F $=> F
:= funa => Id (F a).
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B F: A -> B Is0Functor0: Is0Functor F
Is1Natural F F (id_transformation F)
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B F: A -> B Is0Functor0: Is0Functor F
Is1Natural F F (id_transformation F)
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B F: A -> B Is0Functor0: Is0Functor F a, b: A f: a $-> b
id_transformation F b $o fmap F f $==
fmap F f $o id_transformation F a
refine (cat_idl _ $@ (cat_idr _)^$).Defined.
A, B: Type F: A -> B H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B Is0Functor0: Is0Functor F
NatTrans F F
A, B: Type F: A -> B H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B Is0Functor0: Is0Functor F
NatTrans F F
A, B: Type F: A -> B H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B Is0Functor0: Is0Functor F
Is1Natural F F ?Goal
rapply is1natural_id.Defined.Definitiontrans_comp {AB : Type} `{Is01Cat B}
{F G K : A -> B} (gamma : G $=> K) (alpha : F $=> G)
: F $=> K
:= funa => gamma a $o alpha a.Definitiontrans_prewhisker {AB : Type} {C : B -> Type} {FG : forallx, C x}
`{Is01Cat B} `{!forallx, IsGraph (C x)}
`{!forallx, Is01Cat (C x)} (gamma : F $=> G) (K : A -> B)
: F o K $=> G o K
:= gamma o K.Definitiontrans_postwhisker {ABC : Type} {FG : A -> B}
(K : B -> C) `{Is01Cat B, Is01Cat C, !Is0Functor K} (gamma : F $=> G)
: K o F $=> K o G
:= funa => fmap K (gamma a).
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B F, G, K: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K gamma: G $=> K Is1Natural0: Is1Natural G K gamma alpha: F $=> G Is1Natural1: Is1Natural F G alpha
Is1Natural F K (trans_comp gamma alpha)
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B F, G, K: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K gamma: G $=> K Is1Natural0: Is1Natural G K gamma alpha: F $=> G Is1Natural1: Is1Natural F G alpha
Is1Natural F K (trans_comp gamma alpha)
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B F, G, K: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K gamma: G $=> K Is1Natural0: Is1Natural G K gamma alpha: F $=> G Is1Natural1: Is1Natural F G alpha a, b: A f: a $-> b
gamma b $o alpha b $o fmap F f $==
fmap K f $o (gamma a $o alpha a)
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B F, G, K: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K gamma: G $=> K Is1Natural0: Is1Natural G K gamma alpha: F $=> G Is1Natural1: Is1Natural F G alpha a, b: A f: a $-> b
gamma b $o (fmap G f $o alpha a) $==
fmap K f $o (gamma a $o alpha a)
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B F, G, K: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K gamma: G $=> K Is1Natural0: Is1Natural G K gamma alpha: F $=> G Is1Natural1: Is1Natural F G alpha a, b: A f: a $-> b
fmap K f $o gamma a $o alpha a $==
fmap K f $o (gamma a $o alpha a)
apply cat_assoc.Defined.
A, B, C: Type F, G: B -> C K: A -> B H: IsGraph A H0: IsGraph B H1: Is01Cat B IsGraph0: IsGraph C Is2Graph0: Is2Graph C Is01Cat0: Is01Cat C H2: Is1Cat C Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K gamma: F $=> G L: Is1Natural F G gamma
Is1Natural (F o K) (G o K) (trans_prewhisker gamma K)
A, B, C: Type F, G: B -> C K: A -> B H: IsGraph A H0: IsGraph B H1: Is01Cat B IsGraph0: IsGraph C Is2Graph0: Is2Graph C Is01Cat0: Is01Cat C H2: Is1Cat C Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K gamma: F $=> G L: Is1Natural F G gamma
Is1Natural (F o K) (G o K) (trans_prewhisker gamma K)
A, B, C: Type F, G: B -> C K: A -> B H: IsGraph A H0: IsGraph B H1: Is01Cat B IsGraph0: IsGraph C Is2Graph0: Is2Graph C Is01Cat0: Is01Cat C H2: Is1Cat C Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K gamma: F $=> G L: Is1Natural F G gamma x, y: A f: x $-> y
gamma (K y) $o fmap F (fmap K f) $==
fmap G (fmap K f) $o gamma (K x)
exact (L _ _ _).Defined.
A, B, C: Type F, G: A -> B K: B -> C 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 Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K gamma: F $=> G L: Is1Natural F G gamma
Is1Natural (K o F) (K o G) (trans_postwhisker K gamma)
A, B, C: Type F, G: A -> B K: B -> C 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 Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K gamma: F $=> G L: Is1Natural F G gamma
Is1Natural (K o F) (K o G) (trans_postwhisker K gamma)
A, B, C: Type F, G: A -> B K: B -> C 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 Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K gamma: F $=> G L: Is1Natural F G gamma x, y: A f: x $-> y
fmap K (gamma y) $o fmap K (fmap F f) $==
fmap K (fmap G f) $o fmap K (gamma x)
A, B, C: Type F, G: A -> B K: B -> C 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 Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K gamma: F $=> G L: Is1Natural F G gamma x, y: A f: x $-> y
?Goal0 $-> fmap K (gamma y) $o fmap K (fmap F f)
A, B, C: Type F, G: A -> B K: B -> C 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 Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K gamma: F $=> G L: Is1Natural F G gamma x, y: A f: x $-> y
?Goal0 $== ?Goal
A, B, C: Type F, G: A -> B K: B -> C 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 Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K gamma: F $=> G L: Is1Natural F G gamma x, y: A f: x $-> y
?Goal $== fmap K (fmap G f) $o fmap K (gamma x)
A, B, C: Type F, G: A -> B K: B -> C 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 Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K gamma: F $=> G L: Is1Natural F G gamma x, y: A f: x $-> y
fmap K (gamma y $o fmap F f) $==
fmap K (fmap G f $o gamma x)
A, B, C: Type F, G: A -> B K: B -> C 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 Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K gamma: F $=> G L: Is1Natural F G gamma x, y: A f: x $-> y
gamma y $o fmap F f $== fmap G f $o gamma x
exact (L _ _ _).Defined.
A, B: Type F, G, K: A -> B H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K
NatTrans G K -> NatTrans F G -> NatTrans F K
A, B: Type F, G, K: A -> B H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K
NatTrans G K -> NatTrans F G -> NatTrans F K
A, B: Type F, G, K: A -> B H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K alpha: NatTrans G K beta: NatTrans F G
NatTrans F K
A, B: Type F, G, K: A -> B H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K alpha: NatTrans G K beta: NatTrans F G
Is1Natural F K ?Goal
rapply (is1natural_comp alpha beta).Defined.
A, B, C: Type F, G: B -> C 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 Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: NatTrans F G K: A -> B Is0Functor2: Is0Functor K
NatTrans (F o K) (G o K)
A, B, C: Type F, G: B -> C 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 Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: NatTrans F G K: A -> B Is0Functor2: Is0Functor K
NatTrans (F o K) (G o K)
A, B, C: Type F, G: B -> C 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 Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: NatTrans F G K: A -> B Is0Functor2: Is0Functor K
Is1Natural (funx : A => F (K x))
(funx : A => G (K x)) ?Goal
rapply (is1natural_prewhisker K alpha).Defined.
A, B, C: Type F, G: A -> B K: B -> C 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 Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K
NatTrans F G -> NatTrans (K o F) (K o G)
A, B, C: Type F, G: A -> B K: B -> C 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 Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K
NatTrans F G -> NatTrans (K o F) (K o G)
A, B, C: Type F, G: A -> B K: B -> C 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 Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K alpha: NatTrans F G
NatTrans (K o F) (K o G)
A, B, C: Type F, G: A -> B K: B -> C 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 Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K alpha: NatTrans F G
Is1Natural (funx : A => K (F x))
(funx : A => K (G x)) ?Goal
rapply (is1natural_postwhisker K alpha).Defined.(** Modifying a transformation to something pointwise equal preserves naturality. *)
A, B: Type H: IsGraph A H0: Is01Cat A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H1: Is1Cat B F: A -> B Is0Functor0: Is0Functor F G: A -> B Is0Functor1: Is0Functor G alpha, gamma: F $=> G Is1Natural0: Is1Natural F G gamma p: foralla : A, alpha a $== gamma a
Is1Natural F G alpha
A, B: Type H: IsGraph A H0: Is01Cat A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H1: Is1Cat B F: A -> B Is0Functor0: Is0Functor F G: A -> B Is0Functor1: Is0Functor G alpha, gamma: F $=> G Is1Natural0: Is1Natural F G gamma p: foralla : A, alpha a $== gamma a
Is1Natural F G alpha
A, B: Type H: IsGraph A H0: Is01Cat A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H1: Is1Cat B F: A -> B Is0Functor0: Is0Functor F G: A -> B Is0Functor1: Is0Functor G alpha, gamma: F $=> G Is1Natural0: Is1Natural F G gamma p: foralla : A, alpha a $== gamma a a, b: A f: a $-> b
alpha b $o fmap F f $== fmap G f $o alpha a
exact ((p b $@R _) $@ isnat gamma f $@ (_ $@L (p a)^$)).Defined.(** Opposite natural transformations *)
A, B: Type H: IsGraph B H0: Is01Cat B F, G: A -> B alpha: F $=> G
(G : A^op -> B^op) $=> (F : A^op -> B^op)
A, B: Type H: IsGraph B H0: Is01Cat B F, G: A -> B alpha: F $=> G
(G : A^op -> B^op) $=> (F : A^op -> B^op)
A, B: Type H: IsGraph B H0: Is01Cat B F, G: A -> B alpha: F $=> G
G $=> F
A, B: Type H: IsGraph B H0: Is01Cat B F, G: A -> B alpha: F $=> G
G $=> F
A, B: Type H: IsGraph B H0: Is01Cat B F, G: A -> B alpha: F $=> G a: A
G a $-> F a
apply (alpha a).Defined.
A, B: Type H: IsGraph A H0: Is01Cat A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H1: Is1Cat B F: A -> B Is0Functor0: Is0Functor F G: A -> B Is0Functor1: Is0Functor G alpha: F $=> G Is1Natural0: Is1Natural F G alpha
Is1Natural (G : A^op -> B^op) (F : A^op -> B^op)
(transformation_op F G alpha)
A, B: Type H: IsGraph A H0: Is01Cat A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H1: Is1Cat B F: A -> B Is0Functor0: Is0Functor F G: A -> B Is0Functor1: Is0Functor G alpha: F $=> G Is1Natural0: Is1Natural F G alpha
Is1Natural (G : A^op -> B^op) (F : A^op -> B^op)
(transformation_op F G alpha)
A, B: Type H: IsGraph A H0: Is01Cat A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H1: Is1Cat B F: A -> B Is0Functor0: Is0Functor F G: A -> B Is0Functor1: Is0Functor G alpha: F $=> G Is1Natural0: Is1Natural F G alpha
Is1Natural G F (transformation_op F G alpha)
A, B: Type H: IsGraph A H0: Is01Cat A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H1: Is1Cat B F: A -> B Is0Functor0: Is0Functor F G: A -> B Is0Functor1: Is0Functor G alpha: F $=> G Is1Natural0: Is1Natural F G alpha
Is1Natural G F (funa : A => alpha a)
A, B: Type H: IsGraph A H0: Is01Cat A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H1: Is1Cat B F: A -> B Is0Functor0: Is0Functor F G: A -> B Is0Functor1: Is0Functor G alpha: F $=> G Is1Natural0: Is1Natural F G alpha a, b: A f: a $-> b
alpha b $o fmap (G : A^op -> B^op) f $==
fmap (F : A^op -> B^op) f $o alpha a
srapply isnat_tr.Defined.(** Natural equivalences *)RecordNatEquiv {AB : Type} `{IsGraph A} `{HasEquivs B}
{F G : A -> B} `{!Is0Functor F, !Is0Functor G} :=
{
cat_equiv_natequiv : foralla, F a $<~> G a ;
is1natural_natequiv : Is1Natural F G (funa => cat_equiv_natequiv a) ;
}.Arguments NatEquiv {A B} {isgraph_A}
{isgraph_B} {is2graph_B} {is01cat_B} {is1cat_B} {hasequivs_B}
F G {is0functor_F} {is0functor_G} : rename.Arguments Build_NatEquiv {A B} {isgraph_A}
{isgraph_B} {is2graph_B} {is01cat_B} {is1cat_B} {hasequivs_B}
F G {is0functor_F} {is0functor_G} e isnat_e: rename.Definitionissig_NatEquiv {AB : Type} `{IsGraph A} `{HasEquivs B}
(F G : A -> B) `{!Is0Functor F, !Is0Functor G}
: _ <~> NatEquiv F G := ltac:(issig).Global Existing Instanceis1natural_natequiv.Coercioncat_equiv_natequiv : NatEquiv >-> Funclass.
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G
NatEquiv F G -> NatTrans F G
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G
NatEquiv F G -> NatTrans F G
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: NatEquiv F G
NatTrans F G
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: NatEquiv F G
Is1Natural F G ?Goal
rapply (is1natural_natequiv alpha).Defined.(** Throws a warning, but can probably be ignored. *)Global Set Warnings"-ambiguous-paths".Coercionnattrans_natequiv : NatEquiv >-> NatTrans.(** The above coercion doesn't trigger when it should, so we add the following. *)Definitionisnat_natequiv {AB : Type} `{IsGraph A} `{HasEquivs B}
{F G : A -> B} `{!Is0Functor F, !Is0Functor G} (alpha : NatEquiv F G)
{a a' : A} (f : a $-> a')
:= isnat (nattrans_natequiv alpha) f.
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: NatTrans F G H2: foralla : A, CatIsEquiv (alpha a)
NatEquiv F G
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: NatTrans F G H2: foralla : A, CatIsEquiv (alpha a)
NatEquiv F G
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: NatTrans F G H2: foralla : A, CatIsEquiv (alpha a)
foralla : A, F a $<~> G a
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: NatTrans F G H2: foralla : A, CatIsEquiv (alpha a)
Is1Natural F G (funa : A => ?e a)
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: NatTrans F G H2: foralla : A, CatIsEquiv (alpha a)
foralla : A, F a $<~> G a
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: NatTrans F G H2: foralla : A, CatIsEquiv (alpha a) a: A
F a $<~> G a
refine (Build_CatEquiv (alpha a)).
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: NatTrans F G H2: foralla : A, CatIsEquiv (alpha a)
Is1Natural F G
(funa : A =>
(funa0 : A => Build_CatEquiv (alpha a0)) a)
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: NatTrans F G H2: foralla : A, CatIsEquiv (alpha a) a, a': A f: a $-> a'
Build_CatEquiv (alpha a') $o fmap F f $==
fmap G f $o Build_CatEquiv (alpha a)
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: NatTrans F G H2: foralla : A, CatIsEquiv (alpha a) a, a': A f: a $-> a'
alpha a' $o fmap F f $== fmap G f $o alpha a
apply (isnat alpha).Defined.Definitionnatequiv_compose {AB} {FGH : A -> B} `{IsGraph A} `{HasEquivs B}
`{!Is0Functor F, !Is0Functor G, !Is0Functor H}
(alpha : NatEquiv G H) (beta : NatEquiv F G)
: NatEquiv F H
:= Build_NatEquiv' (nattrans_comp alpha beta).Definitionnatequiv_prewhisker {ABC} {HK : B -> C}
`{IsGraph A, HasEquivs B, HasEquivs C, !Is0Functor H, !Is0Functor K}
(alpha : NatEquiv H K) (F : A -> B) `{!Is0Functor F}
: NatEquiv (H o F) (K o F)
:= Build_NatEquiv' (nattrans_prewhisker alpha F).
A, B, C: Type F, G: A -> B H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H2: Is1Cat C H3: HasEquivs C Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G K: B -> C alpha: NatEquiv F G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K
NatEquiv (K o F) (K o G)
A, B, C: Type F, G: A -> B H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H2: Is1Cat C H3: HasEquivs C Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G K: B -> C alpha: NatEquiv F G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K
NatEquiv (K o F) (K o G)
A, B, C: Type F, G: A -> B H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H2: Is1Cat C H3: HasEquivs C Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G K: B -> C alpha: NatEquiv F G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K
Is1Functor K
A, B, C: Type F, G: A -> B H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H2: Is1Cat C H3: HasEquivs C Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G K: B -> C alpha: NatEquiv F G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K
foralla : A,
CatIsEquiv (nattrans_postwhisker K alpha a)
A, B, C: Type F, G: A -> B H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H2: Is1Cat C H3: HasEquivs C Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G K: B -> C alpha: NatEquiv F G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K
Is1Functor K
A, B, C: Type F, G: A -> B H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H2: Is1Cat C H3: HasEquivs C Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G K: B -> C alpha: NatEquiv F G Is0Functor2: Is0Functor K Is1Functor0: Is1Functor K
foralla : A, CatIsEquiv (fmap K (alpha a))
all: exact _.Defined.
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G
NatEquiv F G -> NatEquiv G F
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G
NatEquiv F G -> NatEquiv G F
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: foralla : A, F a $<~> G a I: Is1Natural F G (funa : A => alpha a)
NatEquiv G F
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: foralla : A, F a $<~> G a I: Is1Natural F G (funa : A => alpha a)
foralla : A, G a $<~> F a
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: foralla : A, F a $<~> G a I: Is1Natural F G (funa : A => alpha a)
Is1Natural G F (funa : A => ?e a)
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: foralla : A, F a $<~> G a I: Is1Natural F G (funa : A => alpha a)
Is1Natural G F
(funa : A =>
(funa0 : A =>
symmetric_cate (F a0) (G a0) (alpha a0)) a)
A, B: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B F, G: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G alpha: foralla : A, F a $<~> G a I: Is1Natural F G (funa : A => alpha a) X, Y: A f: X $-> Y
symmetric_cate (F Y) (G Y) (alpha Y) $o fmap G f $==
fmap F f $o symmetric_cate (F X) (G X) (alpha X)
apply vinverse, I.Defined.(** This lemma might seem unnecessery since as functions ((F o G) o K) and (F o (G o K)) are definitionally equal. But the functor instances of both sides are different. This can be a nasty trap since you cannot see this difference clearly. *)
A, B, C, D: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H2: Is1Cat C H3: HasEquivs C IsGraph2: IsGraph D Is2Graph2: Is2Graph D Is01Cat2: Is01Cat D H4: Is1Cat D H5: HasEquivs D F: C -> D G: B -> C K: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K
NatEquiv (F o G o K) (F o (G o K))
A, B, C, D: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H2: Is1Cat C H3: HasEquivs C IsGraph2: IsGraph D Is2Graph2: Is2Graph D Is01Cat2: Is01Cat D H4: Is1Cat D H5: HasEquivs D F: C -> D G: B -> C K: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K
NatEquiv (F o G o K) (F o (G o K))
A, B, C, D: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H2: Is1Cat C H3: HasEquivs C IsGraph2: IsGraph D Is2Graph2: Is2Graph D Is01Cat2: Is01Cat D H4: Is1Cat D H5: HasEquivs D F: C -> D G: B -> C K: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K
foralla : A,
(funx : A => (F o G) (K x)) a $<~>
(funx : A => F ((G o K) x)) a
A, B, C, D: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H2: Is1Cat C H3: HasEquivs C IsGraph2: IsGraph D Is2Graph2: Is2Graph D Is01Cat2: Is01Cat D H4: Is1Cat D H5: HasEquivs D F: C -> D G: B -> C K: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K
Is1Natural (funx : A => (F o G) (K x))
(funx : A => F ((G o K) x))
(funa : A => ?e a)
A, B, C, D: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H2: Is1Cat C H3: HasEquivs C IsGraph2: IsGraph D Is2Graph2: Is2Graph D Is01Cat2: Is01Cat D H4: Is1Cat D H5: HasEquivs D F: C -> D G: B -> C K: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K
Is1Natural (funx : A => (F o G) (K x))
(funx : A => F ((G o K) x))
(funa : A =>
(funa0 : A => reflexive_cate (F (G (K a0)))) a)
A, B, C, D: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H2: Is1Cat C H3: HasEquivs C IsGraph2: IsGraph D Is2Graph2: Is2Graph D Is01Cat2: Is01Cat D H4: Is1Cat D H5: HasEquivs D F: C -> D G: B -> C K: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K X, Y: A f: X $-> Y
reflexive_cate (F (G (K Y))) $o
fmap ((funx : B => F (G x)) o K) f $==
fmap (F o (funx : A => G (K x))) f $o
reflexive_cate (F (G (K X)))
A, B, C, D: Type H: IsGraph A IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H0: Is1Cat B H1: HasEquivs B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H2: Is1Cat C H3: HasEquivs C IsGraph2: IsGraph D Is2Graph2: Is2Graph D Is01Cat2: Is01Cat D H4: Is1Cat D H5: HasEquivs D F: C -> D G: B -> C K: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G Is0Functor2: Is0Functor K X, Y: A f: X $-> Y
fmap (F o (funx : A => G (K x))) f $o
reflexive_cate (F (G (K X))) $->
fmap ((funx : B => F (G x)) o K) 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: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G
NatEquiv F G -> NatEquiv (G : A^op -> B^op) 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: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G
NatEquiv F G -> NatEquiv (G : A^op -> B^op) 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: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G a: foralla : A, F a $<~> G a n: Is1Natural F G (funa0 : A => a a0)
NatEquiv 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: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G a: foralla : A, F a $<~> G a n: Is1Natural F G (funa0 : A => a a0)
foralla : A^op, G a $<~> 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: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G a: foralla : A, F a $<~> G a n: Is1Natural F G (funa0 : A => a a0)
Is1Natural G F (funa0 : A^op => ?e a0)
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: A -> B Is0Functor0: Is0Functor F Is0Functor1: Is0Functor G a: foralla : A, F a $<~> G a n: Is1Natural F G (funa0 : A => a a0)
Is1Natural G F (funa0 : A^op => a a0)
rapply is1nat_op.Defined.(** *** Pointed natural transformations *)DefinitionPointedTransformation {BC : Type} `{Is1Cat B, Is1Gpd C}
`{IsPointed B, IsPointed C} (F G : B -->* C)
:= {eta : F $=> G & eta (point _) $== bp_pointed F $@ (bp_pointed G)^$}.Notation"F $=>* G" := (PointedTransformation F G) (at level70).
B, C: Type IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H0: Is1Cat C Is0Gpd0: Is0Gpd C H1: Is1Gpd C H2: IsPointed B H3: IsPointed C F, G: B -->* C
F $=>* G -> G $=>* F
B, C: Type IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H0: Is1Cat C Is0Gpd0: Is0Gpd C H1: Is1Gpd C H2: IsPointed B H3: IsPointed C F, G: B -->* C
F $=>* G -> G $=>* F
B, C: Type IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H0: Is1Cat C Is0Gpd0: Is0Gpd C H1: Is1Gpd C H2: IsPointed B H3: IsPointed C F, G: B -->* C h: F $=> G p: h (point B) $== bp_pointed F $@ (bp_pointed G)^$
G $=>* F
B, C: Type IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H0: Is1Cat C Is0Gpd0: Is0Gpd C H1: Is1Gpd C H2: IsPointed B H3: IsPointed C F, G: B -->* C h: F $=> G p: h (point B) $== bp_pointed F $@ (bp_pointed G)^$
(h (point B))^$ $== bp_pointed G $@ (bp_pointed F)^$
B, C: Type IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H0: Is1Cat C Is0Gpd0: Is0Gpd C H1: Is1Gpd C H2: IsPointed B H3: IsPointed C F, G: B -->* C h: F $=> G p: h (point B) $== bp_pointed F $@ (bp_pointed G)^$
(bp_pointed F $@ (bp_pointed G)^$)^$ $==
bp_pointed G $@ (bp_pointed F)^$
B, C: Type IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H0: Is1Cat C Is0Gpd0: Is0Gpd C H1: Is1Gpd C H2: IsPointed B H3: IsPointed C F, G: B -->* C h: F $=> G p: h (point B) $== bp_pointed F $@ (bp_pointed G)^$
B, C: Type IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H0: Is1Cat C Is0Gpd0: Is0Gpd C H1: Is1Gpd C H2: IsPointed B H3: IsPointed C F, G: B -->* C h: F $=> G p: h (point B) $== bp_pointed F $@ (bp_pointed G)^$
B, C: Type IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H0: Is1Cat C Is0Gpd0: Is0Gpd C H1: Is1Gpd C H2: IsPointed B H3: IsPointed C F0, F1, F2: B -->* C
F0 $=>* F1 -> F1 $=>* F2 -> F0 $=>* F2
B, C: Type IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H0: Is1Cat C Is0Gpd0: Is0Gpd C H1: Is1Gpd C H2: IsPointed B H3: IsPointed C F0, F1, F2: B -->* C
F0 $=>* F1 -> F1 $=>* F2 -> F0 $=>* F2
B, C: Type IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H0: Is1Cat C Is0Gpd0: Is0Gpd C H1: Is1Gpd C H2: IsPointed B H3: IsPointed C F0, F1, F2: B -->* C h0: F0 $=> F1 p0: h0 (point B) $==
bp_pointed F0 $@ (bp_pointed F1)^$ h1: F1 $=> F2 p1: h1 (point B) $==
bp_pointed F1 $@ (bp_pointed F2)^$
F0 $=>* F2
B, C: Type IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H0: Is1Cat C Is0Gpd0: Is0Gpd C H1: Is1Gpd C H2: IsPointed B H3: IsPointed C F0, F1, F2: B -->* C h0: F0 $=> F1 p0: h0 (point B) $==
bp_pointed F0 $@ (bp_pointed F1)^$ h1: F1 $=> F2 p1: h1 (point B) $==
bp_pointed F1 $@ (bp_pointed F2)^$
B, C: Type IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H0: Is1Cat C Is0Gpd0: Is0Gpd C H1: Is1Gpd C H2: IsPointed B H3: IsPointed C F0, F1, F2: B -->* C h0: F0 $=> F1 p0: h0 (point B) $==
bp_pointed F0 $@ (bp_pointed F1)^$ h1: F1 $=> F2 p1: h1 (point B) $==
bp_pointed F1 $@ (bp_pointed F2)^$
B, C: Type IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H0: Is1Cat C Is0Gpd0: Is0Gpd C H1: Is1Gpd C H2: IsPointed B H3: IsPointed C F0, F1, F2: B -->* C h0: F0 $=> F1 p0: h0 (point B) $==
bp_pointed F0 $@ (bp_pointed F1)^$ h1: F1 $=> F2 p1: h1 (point B) $==
bp_pointed F1 $@ (bp_pointed F2)^$
B, C: Type IsGraph0: IsGraph B Is2Graph0: Is2Graph B Is01Cat0: Is01Cat B H: Is1Cat B IsGraph1: IsGraph C Is2Graph1: Is2Graph C Is01Cat1: Is01Cat C H0: Is1Cat C Is0Gpd0: Is0Gpd C H1: Is1Gpd C H2: IsPointed B H3: IsPointed C F0, F1, F2: B -->* C h0: F0 $=> F1 p0: h0 (point B) $==
bp_pointed F0 $@ (bp_pointed F1)^$ h1: F1 $=> F2 p1: h1 (point B) $==
bp_pointed F1 $@ (bp_pointed F2)^$
apply gpd_h_Vh.Defined.Notation"h $@* k" := (ptransformation_compose h k) (at level40).(* TODO: *)(* Morphisms of natural transformations - Modifications *)(* Since [Transformation] is dependent, we can define a modification to be a transformation together with a cylinder condition. This doesn't seem to be too useful as of yet however. We would also need better ways to write down cylinders. *)