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 WildCat.Equiv WildCat.EquivGpd
WildCat.Forall.(** * The wild 1-category of 0-groupoids. *)(** Here we define a wild 1-category structure on the type of 0-groupoids. We think of the 1-cells [g $== h] in a 0-groupoid [G] as a substitute for the paths [g = h], and so we closely follow the definitions used for the 1-category of types with [=] replaced by [$==]. In fact, the 1-category structure on types should be the pullback of the 1-category structure on 0-groupoids along a natural map [Type -> ZeroGpd] which sends [A] to [A] equipped with its path types. A second motivating example is the 0-groupoid with underlying type [A -> B] and homotopies as the 1-cells. The definitions chosen here exactly make the Yoneda lemma [opyon_equiv_0gpd] go through. *)RecordZeroGpd := {
carrier :> Type;
isgraph_carrier : IsGraph carrier;
is01cat_carrier : Is01Cat carrier;
is0gpd_carrier : Is0Gpd carrier;
}.Global Existing Instanceisgraph_carrier.Global Existing Instanceis01cat_carrier.Global Existing Instanceis0gpd_carrier.(* The morphisms of 0-groupoids are the 0-functors. This is the same as [Fun01], but we put a different graph and 01-category structure on it, so we give this a custom name. *)RecordMorphism_0Gpd (GH : ZeroGpd) := {
fun_0gpd :> carrier G -> carrier H;
is0functor_fun_0gpd : Is0Functor fun_0gpd;
}.Global Existing Instanceis0functor_fun_0gpd.(** Now we show that the type [ZeroGpd] of 0-groupoids is itself a 1-category, with morphisms the 0-functors. *)
IsGraph ZeroGpd
IsGraph ZeroGpd
ZeroGpd -> ZeroGpd -> Type
exact Morphism_0Gpd.Defined.
Is01Cat ZeroGpd
Is01Cat ZeroGpd
foralla : ZeroGpd, a $-> a
forallabc : ZeroGpd,
(b $-> c) -> (a $-> b) -> a $-> c
foralla : ZeroGpd, a $-> a
G: ZeroGpd
G $-> G
exact (Build_Morphism_0Gpd G G idmap _).
forallabc : ZeroGpd,
(b $-> c) -> (a $-> b) -> a $-> c
G, H, K: ZeroGpd f: H $-> K g: G $-> H
G $-> K
exact (Build_Morphism_0Gpd _ _ (f o g) _).Defined.(* The 2-cells are unnatural transformations, and are analogous to homotopies. *)
Is2Graph ZeroGpd
Is2Graph ZeroGpd
G, H: ZeroGpd
IsGraph (G $-> H)
G, H: ZeroGpd
(G $-> H) -> (G $-> H) -> Type
G, H: ZeroGpd f, g: G $-> H
Type
exact (forallx : G, f x $== g x).Defined.
Is1Cat ZeroGpd
Is1Cat ZeroGpd
forallab : ZeroGpd, Is01Cat (a $-> b)
forallab : ZeroGpd, Is0Gpd (a $-> b)
forall (abc : ZeroGpd) (g : b $-> c),
Is0Functor (cat_postcomp a g)
forall (abc : ZeroGpd) (f : a $-> b),
Is0Functor (cat_precomp c f)
forall (abcd : ZeroGpd) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o g $o f $== h $o (g $o f)
forall (abcd : ZeroGpd) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o (g $o f) $== h $o g $o f
forall (ab : ZeroGpd) (f : a $-> b), Id b $o f $== f
forall (ab : ZeroGpd) (f : a $-> b), f $o Id a $== f
forallab : ZeroGpd, Is01Cat (a $-> b)
G, H: ZeroGpd
Is01Cat (G $-> H)
G, H: ZeroGpd
foralla : G $-> H, a $-> a
G, H: ZeroGpd
forallabc : G $-> H,
(b $-> c) -> (a $-> b) -> a $-> c
G, H: ZeroGpd
foralla : G $-> H, a $-> a
G, H: ZeroGpd f: G $-> H
f $-> f
exact (funx => Id (f x)).
G, H: ZeroGpd
forallabc : G $-> H,
(b $-> c) -> (a $-> b) -> a $-> c
G, H: ZeroGpd f, g, h: G $-> H p: g $-> h q: f $-> g
f $-> h
exact (funx => q x $@ p x).
forallab : ZeroGpd, Is0Gpd (a $-> b)
G, H: ZeroGpd
Is0Gpd (G $-> H)
G, H: ZeroGpd
forallab : G $-> H, (a $-> b) -> b $-> a
G, H: ZeroGpd f, g: G $-> H p: f $-> g
g $-> f
exact (funx => (p x)^$).
forall (abc : ZeroGpd) (g : b $-> c),
Is0Functor (cat_postcomp a g)
G, H, K: ZeroGpd f: H $-> K
Is0Functor (cat_postcomp G f)
G, H, K: ZeroGpd f: H $-> K
forallab : G $-> H,
(a $-> b) -> cat_postcomp G f a $-> cat_postcomp G f b
G, H, K: ZeroGpd f: H $-> K g, h: G $-> H p: g $-> h x: G
cat_postcomp G f g x $== cat_postcomp G f h x
G, H, K: ZeroGpd f: H $-> K g, h: G $-> H p: g $-> h x: G
f (g x) $== f (h x)
exact (fmap f (p x)).
forall (abc : ZeroGpd) (f : a $-> b),
Is0Functor (cat_precomp c f)
G, H, K: ZeroGpd f: G $-> H
Is0Functor (cat_precomp K f)
G, H, K: ZeroGpd f: G $-> H
forallab : H $-> K,
(a $-> b) -> cat_precomp K f a $-> cat_precomp K f b
G, H, K: ZeroGpd f: G $-> H g, h: H $-> K p: g $-> h x: G
cat_precomp K f g x $== cat_precomp K f h x
G, H, K: ZeroGpd f: G $-> H g, h: H $-> K p: g $-> h x: G
g (f x) $== h (f x)
exact (p (f x)).
forall (abcd : ZeroGpd) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o g $o f $== h $o (g $o f)
reflexivity. (* Associativity. *)
forall (abcd : ZeroGpd) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o (g $o f) $== h $o g $o f
reflexivity. (* Associativity in opposite direction. *)
forall (ab : ZeroGpd) (f : a $-> b), Id b $o f $== f
reflexivity. (* Left identity. *)
forall (ab : ZeroGpd) (f : a $-> b), f $o Id a $== f
reflexivity. (* Right identity. *)Defined.(** We define equivalences of 0-groupoids as the bi-invertible maps, using [Cat_BiInv] and [Cat_IsBiInv]. This definition is chosen to provide what is needed for the Yoneda lemma, and because it specializes to one of the correct definitions for types. *)Global Instancehasequivs_0gpd : HasEquivs ZeroGpd
:= cat_hasequivs ZeroGpd.(** Coq can't find the composite of the coercions [cate_fun : G $<~> H >-> G $-> H] and [fun_0gpd : Morphism_0Gpd G H >-> G -> H], probably because it passes through the definitional equality of [G $-> H] and [Morphism_0Gpd G H]. I couldn't find a solution, so instead here is a helper function to manually do the coercion when needed. *)Definitionequiv_fun_0gpd {GH : ZeroGpd} (f : G $<~> H) : G -> H
:= fun_0gpd _ _ (cat_equiv_fun _ _ _ f).(** ** Tools for manipulating equivalences of 0-groupoids Even though the proofs are easy, in certain contexts Coq gets confused about [$==] vs [$->], which makes it hard to prove this inline. So we record them here. *)(** Every equivalence is injective. *)
G, H: ZeroGpd f: G $<~> H x, y: G h: equiv_fun_0gpd f x $== equiv_fun_0gpd f y
x $== y
G, H: ZeroGpd f: G $<~> H x, y: G h: equiv_fun_0gpd f x $== equiv_fun_0gpd f y
x $== y
exact ((cat_eissect f x)^$ $@ fmap (equiv_fun_0gpd f^-1$) h $@ cat_eissect f y).Defined.(** This is one example of many things that could be ported from Basics/Equivalences.v. *)DefinitionmoveR_equiv_V_0gpd {GH : ZeroGpd} (f : G $<~> H) (x : H) (y : G) (p : x $== equiv_fun_0gpd f y)
: equiv_fun_0gpd f^-1$ x $== y
:= fmap (equiv_fun_0gpd f^-1$) p $@ cat_eissect f y.DefinitionmoveL_equiv_V_0gpd {GH : ZeroGpd} (f : G $<~> H) (x : H) (y : G) (p : equiv_fun_0gpd f y $== x)
: y $== equiv_fun_0gpd f^-1$ x
:= (cat_eissect f y)^$ $@ fmap (equiv_fun_0gpd f^-1$) p.(** ** [f] is an equivalence of 0-groupoids iff [IsSurjInj f] We now give a different characterization of the equivalences of 0-groupoids, as the injective split essentially surjective 0-functors, which are defined in EquivGpd. Advantages of this logically equivalent formulation are that it tends to be easier to prove in examples and that in some cases it is definitionally equal to [ExtensionAlong], which is convenient. See Homotopy/Suspension.v and Algebra/AbGroups/Abelianization for examples. Advantages of the bi-invertible definition are that it reproduces a definition that is equivalent to [IsEquiv] when applied to types, assuming [Funext]. It also works in any 1-category. *)(** Every equivalence is injective and split essentially surjective. *)
G, H: ZeroGpd f: G $<~> H
IsSurjInj (equiv_fun_0gpd f)
G, H: ZeroGpd f: G $<~> H
IsSurjInj (equiv_fun_0gpd f)
G, H: ZeroGpd f: G $<~> H
SplEssSurj (equiv_fun_0gpd f)
G, H: ZeroGpd f: G $<~> H
forallxy : G,
equiv_fun_0gpd f x $== equiv_fun_0gpd f y -> x $== y
G, H: ZeroGpd f: G $<~> H
SplEssSurj (equiv_fun_0gpd f)
G, H: ZeroGpd f: G $<~> H y: H
{a : G & equiv_fun_0gpd f a $== y}
G, H: ZeroGpd f: G $<~> H y: H
equiv_fun_0gpd f (equiv_fun_0gpd f^-1$ y) $== y
rapply cat_eisretr.
G, H: ZeroGpd f: G $<~> H
forallxy : G,
equiv_fun_0gpd f x $== equiv_fun_0gpd f y -> x $== y
apply isinj_equiv_0gpd.Defined.(** Conversely, every injective split essentially surjective 0-functor is an equivalence. In practice, this is often the easiest way to prove that a functor is an equivalence. *)
G, H: ZeroGpd F: G $-> H e: IsSurjInj F
Cat_IsBiInv F
G, H: ZeroGpd F: G $-> H e: IsSurjInj F
Cat_IsBiInv F
G, H: ZeroGpd F: G $-> H e0: forallb : H, {a : G & F a $== b} e1: forallxy : G, F x $== F y -> x $== y
Cat_IsBiInv F
G, H: ZeroGpd F: G $-> H e0: forallb : H, {a : G & F a $== b} e1: forallxy : G, F x $== F y -> x $== y
H $-> G
G, H: ZeroGpd F: G $-> H e0: forallb : H, {a : G & F a $== b} e1: forallxy : G, F x $== F y -> x $== y
F $o ?g $== Id H
G, H: ZeroGpd F: G $-> H e0: forallb : H, {a : G & F a $== b} e1: forallxy : G, F x $== F y -> x $== y
?g $o F $== Id G
G, H: ZeroGpd F: G $-> H e0: forallb : H, {a : G & F a $== b} e1: forallxy : G, F x $== F y -> x $== y
H $-> G
G, H: ZeroGpd F: G $-> H e0: forallb : H, {a : G & F a $== b} e1: forallxy : G, F x $== F y -> x $== y
H -> G
G, H: ZeroGpd F: G $-> H e0: forallb : H, {a : G & F a $== b} e1: forallxy : G, F x $== F y -> x $== y
Is0Functor ?fun_0gpd
G, H: ZeroGpd F: G $-> H e0: forallb : H, {a : G & F a $== b} e1: forallxy : G, F x $== F y -> x $== y
Is0Functor (funy : H => (e0 y).1)
G, H: ZeroGpd F: G $-> H e0: forallb : H, {a : G & F a $== b} e1: forallxy : G, F x $== F y -> x $== y
forallab : H, (a $-> b) -> (e0 a).1 $-> (e0 b).1
G, H: ZeroGpd F: G $-> H e0: forallb : H, {a : G & F a $== b} e1: forallxy : G, F x $== F y -> x $== y y1, y2: H m: y1 $-> y2
(e0 y1).1 $-> (e0 y2).1
G, H: ZeroGpd F: G $-> H e0: forallb : H, {a : G & F a $== b} e1: forallxy : G, F x $== F y -> x $== y y1, y2: H m: y1 $-> y2
F (e0 y1).1 $== F (e0 y2).1
exact ((e0 y1).2 $@ m $@ ((e0 y2).2)^$).
G, H: ZeroGpd F: G $-> H e0: forallb : H, {a : G & F a $== b} e1: forallxy : G, F x $== F y -> x $== y
F $o
{|
fun_0gpd := funy : H => (e0 y).1;
is0functor_fun_0gpd :=
{|
fmap :=
(fun (y1y2 : H) (m : y1 $-> y2) =>
e1 (e0 y1).1 (e0 y2).1
(((e0 y1).2 $@ m) $@ ((e0 y2).2)^$))
:
forallab : H,
(a $-> b) ->
(funy : H => (e0 y).1) a $->
(funy : H => (e0 y).1) b
|}
|} $== Id H
G, H: ZeroGpd F: G $-> H e0: forallb : H, {a : G & F a $== b} e1: forallxy : G, F x $== F y -> x $== y
forallx : H, F (e0 x).1 $== x
apply e0.
G, H: ZeroGpd F: G $-> H e0: forallb : H, {a : G & F a $== b} e1: forallxy : G, F x $== F y -> x $== y
{|
fun_0gpd := funy : H => (e0 y).1;
is0functor_fun_0gpd :=
{|
fmap :=
(fun (y1y2 : H) (m : y1 $-> y2) =>
e1 (e0 y1).1 (e0 y2).1
(((e0 y1).2 $@ m) $@ ((e0 y2).2)^$))
:
forallab : H,
(a $-> b) ->
(funy : H => (e0 y).1) a $->
(funy : H => (e0 y).1) b
|}
|} $o F $== Id G
G, H: ZeroGpd F: G $-> H e0: forallb : H, {a : G & F a $== b} e1: forallxy : G, F x $== F y -> x $== y
forallx : G, (e0 (F x)).1 $== x
G, H: ZeroGpd F: G $-> H e0: forallb : H, {a : G & F a $== b} e1: forallxy : G, F x $== F y -> x $== y x: G
(e0 (F x)).1 $== x
G, H: ZeroGpd F: G $-> H e0: forallb : H, {a : G & F a $== b} e1: forallxy : G, F x $== F y -> x $== y x: G
F (e0 (F x)).1 $== F x
apply e0.Defined.(** [I]-indexed products for an [I]-indexed family of 0-groupoids. *)
I: Type G: I -> ZeroGpd
ZeroGpd
I: Type G: I -> ZeroGpd
ZeroGpd
rapply (Build_ZeroGpd (foralli, G i)).Defined.(** The [i]-th projection from the [I]-indexed product of 0-groupoids. *)
I: Type G: I -> ZeroGpd
foralli : I, prod_0gpd I G $-> G i
I: Type G: I -> ZeroGpd
foralli : I, prod_0gpd I G $-> G i
I: Type G: I -> ZeroGpd i: I
prod_0gpd I G $-> G i
I: Type G: I -> ZeroGpd i: I
prod_0gpd I G -> G i
I: Type G: I -> ZeroGpd i: I
Is0Functor ?fun_0gpd
I: Type G: I -> ZeroGpd i: I
Is0Functor (funf : prod_0gpd I G => f i)
I: Type G: I -> ZeroGpd i: I
forallab : prod_0gpd I G, (a $-> b) -> a i $-> b i
I: Type G: I -> ZeroGpd i: I f, g: prod_0gpd I G p: f $-> g
f i $-> g i
exact (p i).Defined.(** The universal property of the product of 0-groupoids holds almost definitionally. *)
I: Type G: ZeroGpd H: I -> ZeroGpd
(foralli : I, G $-> H i) <~> (G $-> prod_0gpd I H)
I: Type G: ZeroGpd H: I -> ZeroGpd
(foralli : I, G $-> H i) <~> (G $-> prod_0gpd I H)
I: Type G: ZeroGpd H: I -> ZeroGpd
(foralli : I, G $-> H i) -> G $-> prod_0gpd I H
I: Type G: ZeroGpd H: I -> ZeroGpd
IsEquiv ?equiv_fun
I: Type G: ZeroGpd H: I -> ZeroGpd
(foralli : I, G $-> H i) -> G $-> prod_0gpd I H
I: Type G: ZeroGpd H: I -> ZeroGpd f: foralli : I, G $-> H i
G $-> prod_0gpd I H
I: Type G: ZeroGpd H: I -> ZeroGpd f: foralli : I, G $-> H i
G -> prod_0gpd I H
I: Type G: ZeroGpd H: I -> ZeroGpd f: foralli : I, G $-> H i
Is0Functor ?fun_0gpd
I: Type G: ZeroGpd H: I -> ZeroGpd f: foralli : I, G $-> H i
Is0Functor (fun (x : G) (i : I) => f i x)
I: Type G: ZeroGpd H: I -> ZeroGpd f: foralli : I, G $-> H i
forallab : G,
(a $-> b) ->
(funi : I => f i a) $-> (funi : I => f i b)
I: Type G: ZeroGpd H: I -> ZeroGpd f: foralli : I, G $-> H i x, y: G p: x $-> y i: I
f i x $-> f i y
exact (fmap (f i) p).
I: Type G: ZeroGpd H: I -> ZeroGpd
IsEquiv
(funf : foralli : I, G $-> H i =>
{|
fun_0gpd := fun (x : G) (i : I) => f i x;
is0functor_fun_0gpd :=
{|
fmap :=
(fun (xy : G) (p : x $-> y) =>
(funi : I =>
fmap (f i) p : f i x $-> f i y)
:
(funi : I => f i x) $->
(funi : I => f i y))
:
forallab : G,
(a $-> b) ->
(fun (x : G) (i : I) => f i x) a $->
(fun (x : G) (i : I) => f i x) b
|}
|})
I: Type G: ZeroGpd H: I -> ZeroGpd
(G $-> prod_0gpd I H) -> foralli : I, G $-> H i
I: Type G: ZeroGpd H: I -> ZeroGpd
(funf : foralli : I, G $-> H i =>
{|
fun_0gpd := fun (x : G) (i : I) => f i x;
is0functor_fun_0gpd :=
{|
fmap :=
(fun (xy : G) (p : x $-> y) =>
(funi : I => fmap (f i) p : f i x $-> f i y)
:
(funi : I => f i x) $->
(funi : I => f i y))
:
forallab : G,
(a $-> b) ->
(fun (x : G) (i : I) => f i x) a $->
(fun (x : G) (i : I) => f i x) b
|}
|}) o ?equiv_inv == idmap
I: Type G: ZeroGpd H: I -> ZeroGpd
?equiv_inv
o (funf : foralli : I, G $-> H i =>
{|
fun_0gpd := fun (x : G) (i : I) => f i x;
is0functor_fun_0gpd :=
{|
fmap :=
(fun (xy : G) (p : x $-> y) =>
(funi : I =>
fmap (f i) p : f i x $-> f i y)
:
(funi : I => f i x) $->
(funi : I => f i y))
:
forallab : G,
(a $-> b) ->
(fun (x : G) (i : I) => f i x) a $->
(fun (x : G) (i : I) => f i x) b
|}
|}) == idmap
I: Type G: ZeroGpd H: I -> ZeroGpd
forallx : foralli : I, G $-> H i,
?eisretr
((funf : foralli : I, G $-> H i =>
{|
fun_0gpd := fun (x0 : G) (i : I) => f i x0;
is0functor_fun_0gpd :=
{|
fmap :=
(fun (x0y : G) (p : x0 $-> y) =>
(funi : I =>
fmap (f i) p : f i x0 $-> f i y)
:
(funi : I => f i x0) $->
(funi : I => f i y))
:
forallab : G,
(a $-> b) ->
(fun (x0 : G) (i : I) => f i x0) a $->
(fun (x0 : G) (i : I) => f i x0) b
|}
|}) x) =
ap
(funf : foralli : I, G $-> H i =>
{|
fun_0gpd := fun (x0 : G) (i : I) => f i x0;
is0functor_fun_0gpd :=
{|
fmap :=
(fun (x0y : G) (p : x0 $-> y) =>
(funi : I =>
fmap (f i) p : f i x0 $-> f i y)
:
(funi : I => f i x0) $->
(funi : I => f i y))
:
forallab : G,
(a $-> b) ->
(fun (x0 : G) (i : I) => f i x0) a $->
(fun (x0 : G) (i : I) => f i x0) b
|}
|}) (?eissect x)
I: Type G: ZeroGpd H: I -> ZeroGpd
(G $-> prod_0gpd I H) -> foralli : I, G $-> H i
I: Type G: ZeroGpd H: I -> ZeroGpd f: G $-> prod_0gpd I H
foralli : I, G $-> H i
I: Type G: ZeroGpd H: I -> ZeroGpd f: G $-> prod_0gpd I H i: I
G $-> H i
exact (prod_0gpd_pr i $o f).
I: Type G: ZeroGpd H: I -> ZeroGpd
(funf : foralli : I, G $-> H i =>
{|
fun_0gpd := fun (x : G) (i : I) => f i x;
is0functor_fun_0gpd :=
{|
fmap :=
(fun (xy : G) (p : x $-> y) =>
(funi : I => fmap (f i) p : f i x $-> f i y)
:
(funi : I => f i x) $->
(funi : I => f i y))
:
forallab : G,
(a $-> b) ->
(fun (x : G) (i : I) => f i x) a $->
(fun (x : G) (i : I) => f i x) b
|}
|})
o (fun (f : G $-> prod_0gpd I H) (i : I) =>
prod_0gpd_pr i $o f) == idmap
I: Type G: ZeroGpd H: I -> ZeroGpd f: G $-> prod_0gpd I H
{|
fun_0gpd :=
fun (x : G) (i : I) => (prod_0gpd_pr i $o f) x;
is0functor_fun_0gpd :=
{|
fmap :=
fun (xy : G) (p : x $-> y) (i : I) =>
fmap (prod_0gpd_pr i $o f) p
|}
|} = f
reflexivity.
I: Type G: ZeroGpd H: I -> ZeroGpd
(fun (f : G $-> prod_0gpd I H) (i : I) =>
prod_0gpd_pr i $o f)
o (funf : foralli : I, G $-> H i =>
{|
fun_0gpd := fun (x : G) (i : I) => f i x;
is0functor_fun_0gpd :=
{|
fmap :=
(fun (xy : G) (p : x $-> y) =>
(funi : I =>
fmap (f i) p : f i x $-> f i y)
:
(funi : I => f i x) $->
(funi : I => f i y))
:
forallab : G,
(a $-> b) ->
(fun (x : G) (i : I) => f i x) a $->
(fun (x : G) (i : I) => f i x) b
|}
|}) == idmap
I: Type G: ZeroGpd H: I -> ZeroGpd f: foralli : I, G $-> H i
(funi : I =>
prod_0gpd_pr i $o
{|
fun_0gpd := fun (x : G) (i0 : I) => f i0 x;
is0functor_fun_0gpd :=
{|
fmap :=
fun (xy : G) (p : x $-> y) (i0 : I) =>
fmap (f i0) p
|}
|}) = f
reflexivity.
I: Type G: ZeroGpd H: I -> ZeroGpd
forallx : foralli : I, G $-> H i,
((funf : G $-> prod_0gpd I H => 1)
:
(funf : foralli : I, G $-> H i =>
{|
fun_0gpd := fun (x0 : G) (i : I) => f i x0;
is0functor_fun_0gpd :=
{|
fmap :=
(fun (x0y : G) (p : x0 $-> y) =>
(funi : I =>
fmap (f i) p : f i x0 $-> f i y)
:
(funi : I => f i x0) $->
(funi : I => f i y))
:
forallab : G,
(a $-> b) ->
(fun (x0 : G) (i : I) => f i x0) a $->
(fun (x0 : G) (i : I) => f i x0) b
|}
|})
o (fun (f : G $-> prod_0gpd I H) (i : I) =>
prod_0gpd_pr i $o f) == idmap)
((funf : foralli : I, G $-> H i =>
{|
fun_0gpd := fun (x0 : G) (i : I) => f i x0;
is0functor_fun_0gpd :=
{|
fmap :=
(fun (x0y : G) (p : x0 $-> y) =>
(funi : I =>
fmap (f i) p : f i x0 $-> f i y)
:
(funi : I => f i x0) $->
(funi : I => f i y))
:
forallab : G,
(a $-> b) ->
(fun (x0 : G) (i : I) => f i x0) a $->
(fun (x0 : G) (i : I) => f i x0) b
|}
|}) x) =
ap
(funf : foralli : I, G $-> H i =>
{|
fun_0gpd := fun (x0 : G) (i : I) => f i x0;
is0functor_fun_0gpd :=
{|
fmap :=
(fun (x0y : G) (p : x0 $-> y) =>
(funi : I =>
fmap (f i) p : f i x0 $-> f i y)
:
(funi : I => f i x0) $->
(funi : I => f i y))
:
forallab : G,
(a $-> b) ->
(fun (x0 : G) (i : I) => f i x0) a $->
(fun (x0 : G) (i : I) => f i x0) b
|}
|})
(((funf : foralli : I, G $-> H i => 1)
:
(fun (f : G $-> prod_0gpd I H) (i : I) =>
prod_0gpd_pr i $o f)
o (funf : foralli : I, G $-> H i =>
{|
fun_0gpd := fun (x0 : G) (i : I) => f i x0;
is0functor_fun_0gpd :=
{|
fmap :=
(fun (x0y : G) (p : x0 $-> y) =>
(funi : I =>
fmap (f i) p : f i x0 $-> f i y)
:
(funi : I => f i x0) $->
(funi : I => f i y))
:
forallab : G,
(a $-> b) ->
(fun (x0 : G) (i : I) => f i x0) a $->
(fun (x0 : G) (i : I) => f i x0) b
|}
|}) == idmap) x)
reflexivity.Defined.(** Indexed products of groupoids with equivalent indices and fiberwise equivalent factors are equivalent. *)
I, J: Type ie: I <~> J G: I -> ZeroGpd H: J -> ZeroGpd f: foralli : I, G i $<~> H (ie i)
prod_0gpd I G $<~> prod_0gpd J H
I, J: Type ie: I <~> J G: I -> ZeroGpd H: J -> ZeroGpd f: foralli : I, G i $<~> H (ie i)
prod_0gpd I G $<~> prod_0gpd J H
I, J: Type ie: I <~> J G: I -> ZeroGpd H: J -> ZeroGpd f: foralli : I, G i $<~> H (ie i)
prod_0gpd I G $-> prod_0gpd J H
I, J: Type ie: I <~> J G: I -> ZeroGpd H: J -> ZeroGpd f: foralli : I, G i $<~> H (ie i)
prod_0gpd J H $-> prod_0gpd I G
I, J: Type ie: I <~> J G: I -> ZeroGpd H: J -> ZeroGpd f: foralli : I, G i $<~> H (ie i)
?f $o ?g $== Id (prod_0gpd J H)
I, J: Type ie: I <~> J G: I -> ZeroGpd H: J -> ZeroGpd f: foralli : I, G i $<~> H (ie i)
?g $o ?f $== Id (prod_0gpd I G)
I, J: Type ie: I <~> J G: I -> ZeroGpd H: J -> ZeroGpd f: foralli : I, G i $<~> H (ie i)
prod_0gpd I G $-> prod_0gpd J H
I, J: Type ie: I <~> J G: I -> ZeroGpd H: J -> ZeroGpd f: foralli : I, G i $<~> H (ie i)
prod_0gpd I G -> prod_0gpd J H
I, J: Type ie: I <~> J G: I -> ZeroGpd H: J -> ZeroGpd f: foralli : I, G i $<~> H (ie i)
Is0Functor ?fun_0gpd
I, J: Type ie: I <~> J G: I -> ZeroGpd H: J -> ZeroGpd f: foralli : I, G i $<~> H (ie i)
prod_0gpd I G -> prod_0gpd J H
I, J: Type ie: I <~> J G: I -> ZeroGpd H: J -> ZeroGpd f: foralli : I, G i $<~> H (ie i) h: prod_0gpd I G j: J