ZeroGroupoid.v

Require Import Basics.Overture Basics.Tactics
               Basics.PathGroupoids.[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. *)

Record ZeroGpd := {
  carrier :> Type;
  isgraph_carrier : IsGraph carrier;
  is01cat_carrier : Is01Cat carrier;
  is0gpd_carrier : Is0Gpd carrier;
}.

Global Existing Instance isgraph_carrier.
Global Existing Instance is01cat_carrier.
Global Existing Instance is0gpd_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. *)
Record Morphism_0Gpd (G H : ZeroGpd) := {
  fun_0gpd :> carrier G -> carrier H;
  is0functor_fun_0gpd : Is0Functor fun_0gpd;
}.

Global Existing Instance is0functor_fun_0gpd.

(** Now we show that the type [ZeroGpd] of 0-groupoids is itself a 1-category, with morphisms the 0-functors. *)
Global Instance isgraph_0gpd : IsGraph ZeroGpd.IsGraph ZeroGpd
Proof.IsGraph ZeroGpd
  apply Build_IsGraph.ZeroGpd -> ZeroGpd -> Type
  exact Morphism_0Gpd.
Defined.

Global Instance is01cat_0gpd : Is01Cat ZeroGpd.Is01Cat ZeroGpd
Proof.Is01Cat ZeroGpd
  srapply Build_Is01Cat.forall a : ZeroGpd, a $-> a
forall a b c : ZeroGpd,
(b $-> c) -> (a $-> b) -> a $-> c
  -forall a : ZeroGpd, a $-> a intro G.G: ZeroGpd
G $-> G
    exact (Build_Morphism_0Gpd G G idmap _).
  -forall a b c : ZeroGpd,
(b $-> c) -> (a $-> b) -> a $-> c intros G H K f g.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. *)
Global Instance is2graph_0gpd : Is2Graph ZeroGpd.Is2Graph ZeroGpd
Proof.Is2Graph ZeroGpd
  intros G H.G, H: ZeroGpd
IsGraph (G $-> H)
  snrapply Build_IsGraph.G, H: ZeroGpd
(G $-> H) -> (G $-> H) -> Type
  intros f g.G, H: ZeroGpd
f, g: G $-> H
Type
  exact (forall x : G, f x $== g x).
Defined.

Global Instance is1cat_0gpd : Is1Cat ZeroGpd.Is1Cat ZeroGpd
Proof.Is1Cat ZeroGpd
  snrapply Build_Is1Cat.forall a b : ZeroGpd, Is01Cat (a $-> b)
forall a b : ZeroGpd, Is0Gpd (a $-> b)
forall (a b c : ZeroGpd) (g : b $-> c),
Is0Functor (cat_postcomp a g)
forall (a b c : ZeroGpd) (f : a $-> b),
Is0Functor (cat_precomp c f)
forall (a b c d : ZeroGpd) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o g $o f $== h $o (g $o f)
forall (a b c d : ZeroGpd) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o (g $o f) $== h $o g $o f
forall (a b : ZeroGpd) (f : a $-> b), Id b $o f $== f
forall (a b : ZeroGpd) (f : a $-> b), f $o Id a $== f
  -forall a b : ZeroGpd, Is01Cat (a $-> b) intros G H.G, H: ZeroGpd
Is01Cat (G $-> H)
    srapply Build_Is01Cat.G, H: ZeroGpd
forall a : G $-> H, a $-> a
G, H: ZeroGpd
forall a b c : G $-> H,
(b $-> c) -> (a $-> b) -> a $-> c
    +G, H: ZeroGpd
forall a : G $-> H, a $-> a intro f.G, H: ZeroGpd
f: G $-> H
f $-> f exact (fun x => Id (f x)).
    +G, H: ZeroGpd
forall a b c : G $-> H,
(b $-> c) -> (a $-> b) -> a $-> c intros f g h p q.G, H: ZeroGpd
f, g, h: G $-> H
p: g $-> h
q: f $-> g
f $-> h exact (fun x => q x $@ p x).
  -forall a b : ZeroGpd, Is0Gpd (a $-> b) intros G H.G, H: ZeroGpd
Is0Gpd (G $-> H)
    srapply Build_Is0Gpd.G, H: ZeroGpd
forall a b : G $-> H, (a $-> b) -> b $-> a
    intros f g p.G, H: ZeroGpd
f, g: G $-> H
p: f $-> g
g $-> f exact (fun x => (p x)^$).
  -forall (a b c : ZeroGpd) (g : b $-> c),
Is0Functor (cat_postcomp a g) intros G H K f.G, H, K: ZeroGpd
f: H $-> K
Is0Functor (cat_postcomp G f)
    srapply Build_Is0Functor.G, H, K: ZeroGpd
f: H $-> K
forall a b : G $-> H,
(a $-> b) -> cat_postcomp G f a $-> cat_postcomp G f b
    intros g h p x.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
    cbn.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 (a b c : ZeroGpd) (f : a $-> b),
Is0Functor (cat_precomp c f) intros G H K f.G, H, K: ZeroGpd
f: G $-> H
Is0Functor (cat_precomp K f)
    srapply Build_Is0Functor.G, H, K: ZeroGpd
f: G $-> H
forall a b : H $-> K,
(a $-> b) -> cat_precomp K f a $-> cat_precomp K f b
    intros g h p x.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
    cbn.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 (a b c d : ZeroGpd) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o g $o f $== h $o (g $o f) reflexivity. (* Associativity. *)
  -forall (a b c d : 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 (a b : ZeroGpd) (f : a $-> b), Id b $o f $== f reflexivity. (* Left identity. *)
  -forall (a b : 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 Instance hasequivs_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. *)

Definition equiv_fun_0gpd {G H : 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. *)
Definition isinj_equiv_0gpd {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
Proof.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. *)
Definition moveR_equiv_V_0gpd {G H : 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.

Definition moveL_equiv_V_0gpd {G H : 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. *)
Global Instance issurjinj_equiv_0gpd {G H : ZeroGpd} (f : G $<~> H)
  : IsSurjInj (equiv_fun_0gpd f).G, H: ZeroGpd
f: G $<~> H
IsSurjInj (equiv_fun_0gpd f)
Proof.G, H: ZeroGpd
f: G $<~> H
IsSurjInj (equiv_fun_0gpd f)
  econstructor.G, H: ZeroGpd
f: G $<~> H
SplEssSurj (equiv_fun_0gpd f)
G, H: ZeroGpd
f: G $<~> H
forall x y : G,
equiv_fun_0gpd f x $== equiv_fun_0gpd f y -> x $== y
  -G, H: ZeroGpd
f: G $<~> H
SplEssSurj (equiv_fun_0gpd f) intro y.G, H: ZeroGpd
f: G $<~> H
y: H
{a : G & equiv_fun_0gpd f a $== y}
    exists (equiv_fun_0gpd f^-1$ 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
forall x y : 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. *)
Definition isequiv_0gpd_issurjinj {G H : ZeroGpd} (F : G $-> H)
  {e : IsSurjInj F}
  : Cat_IsBiInv F.G, H: ZeroGpd
F: G $-> H
e: IsSurjInj F
Cat_IsBiInv F
Proof.G, H: ZeroGpd
F: G $-> H
e: IsSurjInj F
Cat_IsBiInv F
  destruct e as [e0 e1]; unfold SplEssSurj in e0.G, H: ZeroGpd
F: G $-> H
e0: forall b : H, {a : G & F a $== b}
e1: forall x y : G, F x $== F y -> x $== y
Cat_IsBiInv F
  srapply catie_adjointify.G, H: ZeroGpd
F: G $-> H
e0: forall b : H, {a : G & F a $== b}
e1: forall x y : G, F x $== F y -> x $== y
H $-> G
G, H: ZeroGpd
F: G $-> H
e0: forall b : H, {a : G & F a $== b}
e1: forall x y : G, F x $== F y -> x $== y
F $o ?g $== Id H
G, H: ZeroGpd
F: G $-> H
e0: forall b : H, {a : G & F a $== b}
e1: forall x y : G, F x $== F y -> x $== y
?g $o F $== Id G
  -G, H: ZeroGpd
F: G $-> H
e0: forall b : H, {a : G & F a $== b}
e1: forall x y : G, F x $== F y -> x $== y
H $-> G snrapply Build_Morphism_0Gpd.G, H: ZeroGpd
F: G $-> H
e0: forall b : H, {a : G & F a $== b}
e1: forall x y : G, F x $== F y -> x $== y
H -> G
G, H: ZeroGpd
F: G $-> H
e0: forall b : H, {a : G & F a $== b}
e1: forall x y : G, F x $== F y -> x $== y
Is0Functor ?fun_0gpd
    1: exact (fun y => (e0 y).1).G, H: ZeroGpd
F: G $-> H
e0: forall b : H, {a : G & F a $== b}
e1: forall x y : G, F x $== F y -> x $== y
Is0Functor (fun y : H => (e0 y).1)
    snrapply Build_Is0Functor; cbn beta.G, H: ZeroGpd
F: G $-> H
e0: forall b : H, {a : G & F a $== b}
e1: forall x y : G, F x $== F y -> x $== y
forall a b : H, (a $-> b) -> (e0 a).1 $-> (e0 b).1
    intros y1 y2 m.G, H: ZeroGpd
F: G $-> H
e0: forall b : H, {a : G & F a $== b}
e1: forall x y : G, F x $== F y -> x $== y
y1, y2: H
m: y1 $-> y2
(e0 y1).1 $-> (e0 y2).1
    apply e1.G, H: ZeroGpd
F: G $-> H
e0: forall b : H, {a : G & F a $== b}
e1: forall x y : 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: forall b : H, {a : G & F a $== b}
e1: forall x y : G, F x $== F y -> x $== y
F $o
{|
  fun_0gpd := fun y : H => (e0 y).1;
  is0functor_fun_0gpd :=
    {|
      fmap :=
        (fun (y1 y2 : H) (m : y1 $-> y2) =>
         e1 (e0 y1).1 (e0 y2).1
           (((e0 y1).2 $@ m) $@ ((e0 y2).2)^$))
        :
        forall a b : H,
        (a $-> b) ->
        (fun y : H => (e0 y).1) a $->
        (fun y : H => (e0 y).1) b
    |}
|} $== Id H cbn.G, H: ZeroGpd
F: G $-> H
e0: forall b : H, {a : G & F a $== b}
e1: forall x y : G, F x $== F y -> x $== y
forall x : H, F (e0 x).1 $== x  apply e0.
  -G, H: ZeroGpd
F: G $-> H
e0: forall b : H, {a : G & F a $== b}
e1: forall x y : G, F x $== F y -> x $== y
{|
  fun_0gpd := fun y : H => (e0 y).1;
  is0functor_fun_0gpd :=
    {|
      fmap :=
        (fun (y1 y2 : H) (m : y1 $-> y2) =>
         e1 (e0 y1).1 (e0 y2).1
           (((e0 y1).2 $@ m) $@ ((e0 y2).2)^$))
        :
        forall a b : H,
        (a $-> b) ->
        (fun y : H => (e0 y).1) a $->
        (fun y : H => (e0 y).1) b
    |}
|} $o F $== Id G cbn.G, H: ZeroGpd
F: G $-> H
e0: forall b : H, {a : G & F a $== b}
e1: forall x y : G, F x $== F y -> x $== y
forall x : G, (e0 (F x)).1 $== x  intro x.G, H: ZeroGpd
F: G $-> H
e0: forall b : H, {a : G & F a $== b}
e1: forall x y : G, F x $== F y -> x $== y
x: G
(e0 (F x)).1 $== x
    apply e1.G, H: ZeroGpd
F: G $-> H
e0: forall b : H, {a : G & F a $== b}
e1: forall x y : 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. *)
Definition prod_0gpd (I : Type) (G : I -> ZeroGpd) : ZeroGpd.I: Type
G: I -> ZeroGpd
ZeroGpd
Proof.I: Type
G: I -> ZeroGpd
ZeroGpd
  rapply (Build_ZeroGpd (forall i, G i)).
Defined.

(** The [i]-th projection from the [I]-indexed product of 0-groupoids. *)
Definition prod_0gpd_pr {I : Type} {G : I -> ZeroGpd}
  : forall i, prod_0gpd I G $-> G i.I: Type
G: I -> ZeroGpd
forall i : I, prod_0gpd I G $-> G i
Proof.I: Type
G: I -> ZeroGpd
forall i : I, prod_0gpd I G $-> G i
  intros i.I: Type
G: I -> ZeroGpd
i: I
prod_0gpd I G $-> G i
  snrapply Build_Morphism_0Gpd.I: Type
G: I -> ZeroGpd
i: I
prod_0gpd I G -> G i
I: Type
G: I -> ZeroGpd
i: I
Is0Functor ?fun_0gpd
  1: exact (fun f => f i).I: Type
G: I -> ZeroGpd
i: I
Is0Functor (fun f : prod_0gpd I G => f i)
  snrapply Build_Is0Functor; cbn beta.I: Type
G: I -> ZeroGpd
i: I
forall a b : prod_0gpd I G, (a $-> b) -> a i $-> b i
  intros f g p.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. *)
Definition equiv_prod_0gpd_corec {I : Type} {G : ZeroGpd} {H : I -> ZeroGpd}
  : (forall i, G $-> H i) <~> (G $-> prod_0gpd I H).I: Type
G: ZeroGpd
H: I -> ZeroGpd
(forall i : I, G $-> H i) <~> (G $-> prod_0gpd I H)
Proof.I: Type
G: ZeroGpd
H: I -> ZeroGpd
(forall i : I, G $-> H i) <~> (G $-> prod_0gpd I H)
  snrapply Build_Equiv.I: Type
G: ZeroGpd
H: I -> ZeroGpd
(forall i : 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
(forall i : I, G $-> H i) -> G $-> prod_0gpd I H intro f.I: Type
G: ZeroGpd
H: I -> ZeroGpd
f: forall i : I, G $-> H i
G $-> prod_0gpd I H
    snrapply Build_Morphism_0Gpd.I: Type
G: ZeroGpd
H: I -> ZeroGpd
f: forall i : I, G $-> H i
G -> prod_0gpd I H
I: Type
G: ZeroGpd
H: I -> ZeroGpd
f: forall i : I, G $-> H i
Is0Functor ?fun_0gpd
    1: exact (fun x i => f i x).I: Type
G: ZeroGpd
H: I -> ZeroGpd
f: forall i : I, G $-> H i
Is0Functor (fun (x : G) (i : I) => f i x)
    snrapply Build_Is0Functor; cbn beta.I: Type
G: ZeroGpd
H: I -> ZeroGpd
f: forall i : I, G $-> H i
forall a b : G,
(a $-> b) ->
(fun i : I => f i a) $-> (fun i : I => f i b)
    intros x y p i; simpl.I: Type
G: ZeroGpd
H: I -> ZeroGpd
f: forall i : 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
  (fun f : forall i : I, G $-> H i =>
   {|
     fun_0gpd := fun (x : G) (i : I) => f i x;
     is0functor_fun_0gpd :=
       {|
         fmap :=
           (fun (x y : G) (p : x $-> y) =>
            (fun i : I =>
             fmap (f i) p : f i x $-> f i y)
            :
            (fun i : I => f i x) $->
            (fun i : I => f i y))
           :
           forall a b : G,
           (a $-> b) ->
           (fun (x : G) (i : I) => f i x) a $->
           (fun (x : G) (i : I) => f i x) b
       |}
   |})
  snrapply Build_IsEquiv.I: Type
G: ZeroGpd
H: I -> ZeroGpd
(G $-> prod_0gpd I H) -> forall i : I, G $-> H i
I: Type
G: ZeroGpd
H: I -> ZeroGpd
(fun f : forall i : I, G $-> H i =>
 {|
   fun_0gpd := fun (x : G) (i : I) => f i x;
   is0functor_fun_0gpd :=
     {|
       fmap :=
         (fun (x y : G) (p : x $-> y) =>
          (fun i : I => fmap (f i) p : f i x $-> f i y)
          :
          (fun i : I => f i x) $->
          (fun i : I => f i y))
         :
         forall a b : 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 (fun f : forall i : I, G $-> H i =>
   {|
     fun_0gpd := fun (x : G) (i : I) => f i x;
     is0functor_fun_0gpd :=
       {|
         fmap :=
           (fun (x y : G) (p : x $-> y) =>
            (fun i : I =>
             fmap (f i) p : f i x $-> f i y)
            :
            (fun i : I => f i x) $->
            (fun i : I => f i y))
           :
           forall a b : 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
forall x : forall i : I, G $-> H i,
?eisretr
  ((fun f : forall i : I, G $-> H i =>
    {|
      fun_0gpd := fun (x0 : G) (i : I) => f i x0;
      is0functor_fun_0gpd :=
        {|
          fmap :=
            (fun (x0 y : G) (p : x0 $-> y) =>
             (fun i : I =>
              fmap (f i) p : f i x0 $-> f i y)
             :
             (fun i : I => f i x0) $->
             (fun i : I => f i y))
            :
            forall a b : G,
            (a $-> b) ->
            (fun (x0 : G) (i : I) => f i x0) a $->
            (fun (x0 : G) (i : I) => f i x0) b
        |}
    |}) x) =
ap
  (fun f : forall i : I, G $-> H i =>
   {|
     fun_0gpd := fun (x0 : G) (i : I) => f i x0;
     is0functor_fun_0gpd :=
       {|
         fmap :=
           (fun (x0 y : G) (p : x0 $-> y) =>
            (fun i : I =>
             fmap (f i) p : f i x0 $-> f i y)
            :
            (fun i : I => f i x0) $->
            (fun i : I => f i y))
           :
           forall a b : 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) -> forall i : I, G $-> H i intro f.I: Type
G: ZeroGpd
H: I -> ZeroGpd
f: G $-> prod_0gpd I H
forall i : I, G $-> H i
    intros 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
(fun f : forall i : I, G $-> H i =>
 {|
   fun_0gpd := fun (x : G) (i : I) => f i x;
   is0functor_fun_0gpd :=
     {|
       fmap :=
         (fun (x y : G) (p : x $-> y) =>
          (fun i : I => fmap (f i) p : f i x $-> f i y)
          :
          (fun i : I => f i x) $->
          (fun i : I => f i y))
         :
         forall a b : 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 intro f.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 (x y : 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 (fun f : forall i : I, G $-> H i =>
   {|
     fun_0gpd := fun (x : G) (i : I) => f i x;
     is0functor_fun_0gpd :=
       {|
         fmap :=
           (fun (x y : G) (p : x $-> y) =>
            (fun i : I =>
             fmap (f i) p : f i x $-> f i y)
            :
            (fun i : I => f i x) $->
            (fun i : I => f i y))
           :
           forall a b : G,
           (a $-> b) ->
           (fun (x : G) (i : I) => f i x) a $->
           (fun (x : G) (i : I) => f i x) b
       |}
   |}) == idmap intro f.I: Type
G: ZeroGpd
H: I -> ZeroGpd
f: forall i : I, G $-> H i
(fun i : I =>
 prod_0gpd_pr i $o
 {|
   fun_0gpd := fun (x : G) (i0 : I) => f i0 x;
   is0functor_fun_0gpd :=
     {|
       fmap :=
         fun (x y : G) (p : x $-> y) (i0 : I) =>
         fmap (f i0) p
     |}
 |}) = f
    reflexivity.
  -I: Type
G: ZeroGpd
H: I -> ZeroGpd
forall x : forall i : I, G $-> H i,
((fun f : G $-> prod_0gpd I H => 1)
 :
 (fun f : forall i : I, G $-> H i =>
  {|
    fun_0gpd := fun (x0 : G) (i : I) => f i x0;
    is0functor_fun_0gpd :=
      {|
        fmap :=
          (fun (x0 y : G) (p : x0 $-> y) =>
           (fun i : I =>
            fmap (f i) p : f i x0 $-> f i y)
           :
           (fun i : I => f i x0) $->
           (fun i : I => f i y))
          :
          forall a b : 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)
  ((fun f : forall i : I, G $-> H i =>
    {|
      fun_0gpd := fun (x0 : G) (i : I) => f i x0;
      is0functor_fun_0gpd :=
        {|
          fmap :=
            (fun (x0 y : G) (p : x0 $-> y) =>
             (fun i : I =>
              fmap (f i) p : f i x0 $-> f i y)
             :
             (fun i : I => f i x0) $->
             (fun i : I => f i y))
            :
            forall a b : G,
            (a $-> b) ->
            (fun (x0 : G) (i : I) => f i x0) a $->
            (fun (x0 : G) (i : I) => f i x0) b
        |}
    |}) x) =
ap
  (fun f : forall i : I, G $-> H i =>
   {|
     fun_0gpd := fun (x0 : G) (i : I) => f i x0;
     is0functor_fun_0gpd :=
       {|
         fmap :=
           (fun (x0 y : G) (p : x0 $-> y) =>
            (fun i : I =>
             fmap (f i) p : f i x0 $-> f i y)
            :
            (fun i : I => f i x0) $->
            (fun i : I => f i y))
           :
           forall a b : G,
           (a $-> b) ->
           (fun (x0 : G) (i : I) => f i x0) a $->
           (fun (x0 : G) (i : I) => f i x0) b
       |}
   |})
  (((fun f : forall i : I, G $-> H i => 1)
    :
    (fun (f : G $-> prod_0gpd I H) (i : I) =>
     prod_0gpd_pr i $o f)
    o (fun f : forall i : I, G $-> H i =>
       {|
         fun_0gpd := fun (x0 : G) (i : I) => f i x0;
         is0functor_fun_0gpd :=
           {|
             fmap :=
               (fun (x0 y : G) (p : x0 $-> y) =>
                (fun i : I =>
                 fmap (f i) p : f i x0 $-> f i y)
                :
                (fun i : I => f i x0) $->
                (fun i : I => f i y))
               :
               forall a b : 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. *)
Definition cate_prod_0gpd {I J : Type} (ie : I <~> J)
  (G : I -> ZeroGpd) (H : J -> ZeroGpd)
  (f : forall (i : 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: forall i : I, G i $<~> H (ie i)
prod_0gpd I G $<~> prod_0gpd J H
Proof.I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
prod_0gpd I G $<~> prod_0gpd J H
  snrapply cate_adjointify.I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : 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: forall i : 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: forall i : 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: forall i : 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: forall i : I, G i $<~> H (ie i)
prod_0gpd I G $-> prod_0gpd J H snrapply Build_Morphism_0Gpd.I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : 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: forall i : I, G i $<~> H (ie i)
Is0Functor ?fun_0gpd
    +I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
prod_0gpd I G -> prod_0gpd J H intros h j.I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
h: prod_0gpd I G
j: J
H j
      exact (transport H (eisretr ie j) (cate_fun (f (ie^-1 j)) (h _))).
    +I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
Is0Functor
  (fun h : prod_0gpd I G =>
   (fun j : J =>
    transport (fun x : J => H x) (eisretr ie j)
      (f (ie^-1 j) (h (ie^-1 j))))
   :
   prod_0gpd J H) nrapply Build_Is0Functor.I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
forall a b : prod_0gpd I G,
(a $-> b) ->
(fun j : J =>
 transport (fun x : J => H x) (eisretr ie j)
   (f (ie^-1 j) (a (ie^-1 j)))) $->
(fun j : J =>
 transport (fun x : J => H x) (eisretr ie j)
   (f (ie^-1 j) (b (ie^-1 j))))
      intros g h p j.I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
g, h: prod_0gpd I G
p: g $-> h
j: J
transport (fun x : J => H x) (eisretr ie j)
  (f (ie^-1 j) (g (ie^-1 j))) $->
transport (fun x : J => H x) (eisretr ie j)
  (f (ie^-1 j) (h (ie^-1 j)))
      destruct (eisretr ie j).I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
g, h: prod_0gpd I G
p: g $-> h
j: J
transport (fun x : J => H x) 1
  (f (ie^-1 j) (g (ie^-1 j))) $->
transport (fun x : J => H x) 1
  (f (ie^-1 j) (h (ie^-1 j)))
      refine (_ $o Hom_path (transport_1 _ _)).I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
g, h: prod_0gpd I G
p: g $-> h
j: J
f (ie^-1 j) (g (ie^-1 j)) $->
transport (fun x : J => H x) 1
  (f (ie^-1 j) (h (ie^-1 j)))
      apply Build_Morphism_0Gpd.I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
g, h: prod_0gpd I G
p: g $-> h
j: J
g (ie^-1 j) $-> h (ie^-1 j)
      exact (p _).
  -I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
prod_0gpd J H $-> prod_0gpd I G exact (equiv_prod_0gpd_corec (fun i => (f i)^-1$ $o prod_0gpd_pr (ie i))).
  -I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
{|
  fun_0gpd :=
    fun h : prod_0gpd I G =>
    (fun j : J =>
     transport (fun x : J => H x) (eisretr ie j)
       (f (ie^-1 j) (h (ie^-1 j))))
    :
    prod_0gpd J H;
  is0functor_fun_0gpd :=
    {|
      fmap :=
        fun (g h : prod_0gpd I G) (p : g $-> h) =>
        (fun j : J =>
         let p0 := eisretr ie j in
         match
           p0 as p1 in (_ = j0)
           return
             (transport (fun x : J => H x) p1
                (f (ie^-1 j) (g (ie^-1 j))) $->
              transport (fun x : J => H x) p1
                (f (ie^-1 j) (h (ie^-1 j))))
         with
         | 1 =>
             (let X :=
                fun (G H : ZeroGpd)
                  (fun_0gpd : G -> H)
                  (is0functor_fun_0gpd : Is0Functor
                                           fun_0gpd)
                =>
                ZeroGroupoid.is0functor_fun_0gpd G H
                  {|
                    fun_0gpd := fun_0gpd;
                    is0functor_fun_0gpd :=
                      is0functor_fun_0gpd
                  |} in
              let X0 :=
                fun (G H : ZeroGpd)
                  (fun_0gpd : G -> H)
                  (is0functor_fun_0gpd : Is0Functor
                                           fun_0gpd)
                =>
                @fmap G H (isgraph_carrier G)
                  (isgraph_carrier H)
                  {|
                    fun_0gpd := fun_0gpd;
                    is0functor_fun_0gpd :=
                      is0functor_fun_0gpd
                  |}
                  (X G H fun_0gpd is0functor_fun_0gpd)
                in
              X0 (G (ie^-1 j)) (H (ie (ie^-1 j)))
                (f (ie^-1 j))
                (is0functor_fun_0gpd (G (ie^-1 j))
                   (H (ie (...))) (f (ie^-1 j)))
                (g (ie^-1 j)) (h (ie^-1 j))
                (p (ie^-1 j))) $o
             Hom_path
               (transport_1 carrier
                  (f (ie^-1 j) (g (ie^-1 j))))
         end)
        :
        (fun j : J =>
         transport (fun x : J => H x) (eisretr ie j)
           (f (ie^-1 j) (g (ie^-1 j)))) $->
        (fun j : J =>
         transport (fun x : J => H x) (eisretr ie j)
           (f (ie^-1 j) (h (ie^-1 j))))
    |}
|} $o
equiv_prod_0gpd_corec
  (fun i : I => (f i)^-1$ $o prod_0gpd_pr (ie i)) $==
Id (prod_0gpd J H) intros h j.I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
h: prod_0gpd J H
j: J
({|
   fun_0gpd :=
     fun (h : prod_0gpd I G) (j : J) =>
     transport (fun x : J => H x) (eisretr ie j)
       (f (ie^-1 j) (h (ie^-1 j)));
   is0functor_fun_0gpd :=
     {|
       fmap :=
         fun (g h : prod_0gpd I G) (p : g $-> h)
           (j : J) =>
         let p0 := eisretr ie j in
         match
           p0 as p1 in (_ = j0)
           return
             (transport (fun x : J => H x) p1
                (f (ie^-1 j) (g (ie^-1 j))) $->
              transport (fun x : J => H x) p1
                (f (ie^-1 j) (h (ie^-1 j))))
         with
         | 1 =>
             (let X :=
                fun (G H : ZeroGpd)
                  (fun_0gpd : G -> H)
                  (is0functor_fun_0gpd : Is0Functor
                                           fun_0gpd)
                =>
                ZeroGroupoid.is0functor_fun_0gpd G H
                  {|
                    fun_0gpd := fun_0gpd;
                    is0functor_fun_0gpd :=
                      is0functor_fun_0gpd
                  |} in
              let X0 :=
                fun (G H : ZeroGpd)
                  (fun_0gpd : G -> H)
                  (is0functor_fun_0gpd : Is0Functor
                                           fun_0gpd)
                =>
                @fmap G H (isgraph_carrier G)
                  (isgraph_carrier H)
                  {|
                    fun_0gpd := fun_0gpd;
                    is0functor_fun_0gpd :=
                      is0functor_fun_0gpd
                  |}
                  (X G H fun_0gpd is0functor_fun_0gpd)
                in
              X0 (G (ie^-1 j)) (H (ie (ie^-1 j)))
                (f (ie^-1 j))
                (is0functor_fun_0gpd (G (ie^-1 j))
                   (H (ie (ie^-1 j))) (f (ie^-1 j)))
                (g (ie^-1 j)) (h (ie^-1 j))
                (p (ie^-1 j))) $o
             Hom_path
               (transport_1 carrier
                  (f (ie^-1 j) (g (ie^-1 j))))
         end
     |}
 |} $o
 equiv_prod_0gpd_corec
   (fun i : I => (f i)^-1$ $o prod_0gpd_pr (ie i))) h
  j $-> Id (prod_0gpd J H) h j
    cbn.I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
h: prod_0gpd J H
j: J
transport (fun x : J => H x) (eisretr ie j)
  (f (ie^-1 j)
     (cat_equiv_inv (f (ie^-1 j)) (h (ie (ie^-1 j))))) $->
h j
    destruct (eisretr ie j).I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
h: prod_0gpd J H
j: J
transport (fun x : J => H x) 1
  (f (ie^-1 j)
     (cat_equiv_inv (f (ie^-1 j)) (h (ie (ie^-1 j))))) $->
h (ie (ie^-1 j))
    exact (cate_isretr (f _) _).
  -I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
equiv_prod_0gpd_corec
  (fun i : I => (f i)^-1$ $o prod_0gpd_pr (ie i)) $o
{|
  fun_0gpd :=
    fun h : prod_0gpd I G =>
    (fun j : J =>
     transport (fun x : J => H x) (eisretr ie j)
       (f (ie^-1 j) (h (ie^-1 j))))
    :
    prod_0gpd J H;
  is0functor_fun_0gpd :=
    {|
      fmap :=
        fun (g h : prod_0gpd I G) (p : g $-> h) =>
        (fun j : J =>
         let p0 := eisretr ie j in
         match
           p0 as p1 in (_ = j0)
           return
             (transport (fun x : J => H x) p1
                (f (ie^-1 j) (g (ie^-1 j))) $->
              transport (fun x : J => H x) p1
                (f (ie^-1 j) (h (ie^-1 j))))
         with
         | 1 =>
             (let X :=
                fun (G H : ZeroGpd)
                  (fun_0gpd : G -> H)
                  (is0functor_fun_0gpd : Is0Functor
                                           fun_0gpd)
                =>
                ZeroGroupoid.is0functor_fun_0gpd G H
                  {|
                    fun_0gpd := fun_0gpd;
                    is0functor_fun_0gpd :=
                      is0functor_fun_0gpd
                  |} in
              let X0 :=
                fun (G H : ZeroGpd)
                  (fun_0gpd : G -> H)
                  (is0functor_fun_0gpd : Is0Functor
                                           fun_0gpd)
                =>
                @fmap G H (isgraph_carrier G)
                  (isgraph_carrier H)
                  {|
                    fun_0gpd := fun_0gpd;
                    is0functor_fun_0gpd :=
                      is0functor_fun_0gpd
                  |}
                  (X G H fun_0gpd is0functor_fun_0gpd)
                in
              X0 (G (ie^-1 j)) (H (ie (ie^-1 j)))
                (f (ie^-1 j))
                (is0functor_fun_0gpd (G (ie^-1 j))
                   (H (ie (...))) (f (ie^-1 j)))
                (g (ie^-1 j)) (h (ie^-1 j))
                (p (ie^-1 j))) $o
             Hom_path
               (transport_1 carrier
                  (f (ie^-1 j) (g (ie^-1 j))))
         end)
        :
        (fun j : J =>
         transport (fun x : J => H x) (eisretr ie j)
           (f (ie^-1 j) (g (ie^-1 j)))) $->
        (fun j : J =>
         transport (fun x : J => H x) (eisretr ie j)
           (f (ie^-1 j) (h (ie^-1 j))))
    |}
|} $== Id (prod_0gpd I G) intros g i.I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
g: prod_0gpd I G
i: I
(equiv_prod_0gpd_corec
   (fun i : I => (f i)^-1$ $o prod_0gpd_pr (ie i)) $o
 {|
   fun_0gpd :=
     fun (h : prod_0gpd I G) (j : J) =>
     transport (fun x : J => H x) (eisretr ie j)
       (f (ie^-1 j) (h (ie^-1 j)));
   is0functor_fun_0gpd :=
     {|
       fmap :=
         fun (g h : prod_0gpd I G) (p : g $-> h)
           (j : J) =>
         let p0 := eisretr ie j in
         match
           p0 as p1 in (_ = j0)
           return
             (transport (fun x : J => H x) p1
                (f (ie^-1 j) (g (ie^-1 j))) $->
              transport (fun x : J => H x) p1
                (f (ie^-1 j) (h (ie^-1 j))))
         with
         | 1 =>
             (let X :=
                fun (G H : ZeroGpd)
                  (fun_0gpd : G -> H)
                  (is0functor_fun_0gpd : Is0Functor
                                           fun_0gpd)
                =>
                ZeroGroupoid.is0functor_fun_0gpd G H
                  {|
                    fun_0gpd := fun_0gpd;
                    is0functor_fun_0gpd :=
                      is0functor_fun_0gpd
                  |} in
              let X0 :=
                fun (G H : ZeroGpd)
                  (fun_0gpd : G -> H)
                  (is0functor_fun_0gpd : Is0Functor
                                           fun_0gpd)
                =>
                @fmap G H (isgraph_carrier G)
                  (isgraph_carrier H)
                  {|
                    fun_0gpd := fun_0gpd;
                    is0functor_fun_0gpd :=
                      is0functor_fun_0gpd
                  |}
                  (X G H fun_0gpd is0functor_fun_0gpd)
                in
              X0 (G (ie^-1 j)) (H (ie (ie^-1 j)))
                (f (ie^-1 j))
                (is0functor_fun_0gpd (G (ie^-1 j))
                   (H (ie (ie^-1 j))) (f (ie^-1 j)))
                (g (ie^-1 j)) (h (ie^-1 j))
                (p (ie^-1 j))) $o
             Hom_path
               (transport_1 carrier
                  (f (ie^-1 j) (g (ie^-1 j))))
         end
     |}
 |}) g i $-> Id (prod_0gpd I G) g i
    cbn.I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
g: prod_0gpd I G
i: I
cat_equiv_inv (f i)
  (transport (fun x : J => H x) (eisretr ie (ie i))
     (f (ie^-1 (ie i)) (g (ie^-1 (ie i))))) $-> g i
    refine (_ $o Hom_path
            (ap (cate_fun (f i)^-1$) (transport2 _ (eisadj ie i) _))).I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
g: prod_0gpd I G
i: I
(f i)^-1$
  (transport (fun x : J => H x) (ap ie (eissect ie i))
     (f (ie^-1 (ie i)) (g (ie^-1 (ie i))))) $-> g i
    destruct (eissect ie i).I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
g: prod_0gpd I G
i: I
(f (ie^-1 (ie i)))^-1$
  (transport (fun x : J => H x) (ap ie 1)
     (f (ie^-1 (ie i)) (g (ie^-1 (ie i))))) $->
g (ie^-1 (ie i))
    exact (cate_issect (f _) _).
Defined.