Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
From HoTT.WildCat Require Import Core Equiv EquivGpd Prod UnitCat
  Forall Graph Induced FunctorCat.

(** * 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;
}.

Definition zerogpd_graph (C : ZeroGpd) : Graph := {|
    graph_carrier := carrier C;
    isgraph_graph_carrier := isgraph_carrier C
  |}.

Instance isgraph_0gpd : IsGraph ZeroGpd := isgraph_induced zerogpd_graph.

Instance is01cat_0gpd : Is01Cat ZeroGpd := is01cat_induced zerogpd_graph.

Instance is2graph_0gpd : Is2Graph ZeroGpd := is2graph_induced zerogpd_graph.

Instance is1cat_0gpd : Is1Cat ZeroGpd.
Is1Cat ZeroGpd
Proof.
Is1Cat ZeroGpd
  snapply 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: zerogpd_graph 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: zerogpd_graph 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: zerogpd_graph 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: zerogpd_graph 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. *)

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
  := fun01_F (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.

Definition isinj_isequiv_0gpd {G H : ZeroGpd} (f : G $-> H) `{!Cat_IsBiInv f}
  {x y : G} (h : f x $== f y)
  : x $== y
  := isinj_equiv_0gpd (Build_Cat_BiInv _ _ _ _ _ _ _ f _) h.

(** These are some examples of 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.

Definition moveR_equiv_M_0gpd {G H : ZeroGpd} (f : G $<~> H) {x : G} {y : H} (p : x $== equiv_fun_0gpd f^-1$ y)
  : equiv_fun_0gpd f x $== y
  := fmap (equiv_fun_0gpd f) p $@ cat_eisretr f y.

Definition moveL_equiv_M_0gpd {G H : ZeroGpd} (f : G $<~> H) {x : G} {y : H} (p : equiv_fun_0gpd f^-1$ y $== x)
  : y $== equiv_fun_0gpd f x
  := (cat_eisretr f y)^$ $@ fmap (equiv_fun_0gpd f) 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. *)
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
    tapply 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 : zerogpd_graph H,
{a : zerogpd_graph G & F a $== b}
e1: forall x y : zerogpd_graph G,
F x $== F y -> x $== y
Cat_IsBiInv F
  stapply catie_adjointify.
G, H: ZeroGpd
F: G $-> H
e0: forall b : zerogpd_graph H,
{a : zerogpd_graph G & F a $== b}
e1: forall x y : zerogpd_graph G,
F x $== F y -> x $== y
H $-> G
G, H: ZeroGpd
F: G $-> H
e0: forall b : zerogpd_graph H,
{a : zerogpd_graph G & F a $== b}
e1: forall x y : zerogpd_graph G,
F x $== F y -> x $== y
F $o ?g $== Id H
G, H: ZeroGpd
F: G $-> H
e0: forall b : zerogpd_graph H,
{a : zerogpd_graph G & F a $== b}
e1: forall x y : zerogpd_graph G,
F x $== F y -> x $== y
?g $o F $== Id G
  -
G, H: ZeroGpd
F: G $-> H
e0: forall b : zerogpd_graph H,
{a : zerogpd_graph G & F a $== b}
e1: forall x y : zerogpd_graph G,
F x $== F y -> x $== y
H $-> G snapply Build_Fun01'.
G, H: ZeroGpd
F: G $-> H
e0: forall b : zerogpd_graph H,
{a : zerogpd_graph G & F a $== b}
e1: forall x y : zerogpd_graph G,
F x $== F y -> x $== y
zerogpd_graph H -> zerogpd_graph G
G, H: ZeroGpd
F: G $-> H
e0: forall b : zerogpd_graph H,
{a : zerogpd_graph G & F a $== b}
e1: forall x y : zerogpd_graph G,
F x $== F y -> x $== y
forall a b : zerogpd_graph H,
(a $-> b) -> ?F a $-> ?F b
    1: exact (fun y => (e0 y).1).
G, H: ZeroGpd
F: G $-> H
e0: forall b : zerogpd_graph H,
{a : zerogpd_graph G & F a $== b}
e1: forall x y : zerogpd_graph G,
F x $== F y -> x $== y
forall a b : zerogpd_graph H,
(a $-> b) ->
(fun y : zerogpd_graph H => (e0 y).1) a $->
(fun y : zerogpd_graph H => (e0 y).1) b
    cbn beta.
G, H: ZeroGpd
F: G $-> H
e0: forall b : zerogpd_graph H,
{a : zerogpd_graph G & F a $== b}
e1: forall x y : zerogpd_graph G,
F x $== F y -> x $== y
forall a b : zerogpd_graph H,
(a $-> b) -> (e0 a).1 $-> (e0 b).1
    intros y1 y2 m.
G, H: ZeroGpd
F: G $-> H
e0: forall b : zerogpd_graph H,
{a : zerogpd_graph G & F a $== b}
e1: forall x y : zerogpd_graph G,
F x $== F y -> x $== y
y1, y2: zerogpd_graph H
m: y1 $-> y2
(e0 y1).1 $-> (e0 y2).1
    apply e1.
G, H: ZeroGpd
F: G $-> H
e0: forall b : zerogpd_graph H,
{a : zerogpd_graph G & F a $== b}
e1: forall x y : zerogpd_graph G,
F x $== F y -> x $== y
y1, y2: zerogpd_graph 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 : zerogpd_graph H,
{a : zerogpd_graph G & F a $== b}
e1: forall x y : zerogpd_graph G,
F x $== F y -> x $== y
F $o
Build_Fun01' (fun y : zerogpd_graph H => (e0 y).1)
  ((fun (y1 y2 : zerogpd_graph H) (m : y1 $-> y2) =>
    e1 (e0 y1).1 (e0 y2).1
      (((e0 y1).2 $@ m) $@ ((e0 y2).2)^$))
   :
   forall a b : zerogpd_graph H,
   (a $-> b) ->
   (fun y : zerogpd_graph H => (e0 y).1) a $->
   (fun y : zerogpd_graph H => (e0 y).1) b) $== Id H cbn.
G, H: ZeroGpd
F: G $-> H
e0: forall b : zerogpd_graph H,
{a : zerogpd_graph G & F a $== b}
e1: forall x y : zerogpd_graph G,
F x $== F y -> x $== y
NatTrans.Transformation (fun x : H => F (e0 x).1)
  idmap exact (fun a => (e0 a).2).
  -
G, H: ZeroGpd
F: G $-> H
e0: forall b : zerogpd_graph H,
{a : zerogpd_graph G & F a $== b}
e1: forall x y : zerogpd_graph G,
F x $== F y -> x $== y
Build_Fun01' (fun y : zerogpd_graph H => (e0 y).1)
  ((fun (y1 y2 : zerogpd_graph H) (m : y1 $-> y2) =>
    e1 (e0 y1).1 (e0 y2).1
      (((e0 y1).2 $@ m) $@ ((e0 y2).2)^$))
   :
   forall a b : zerogpd_graph H,
   (a $-> b) ->
   (fun y : zerogpd_graph H => (e0 y).1) a $->
   (fun y : zerogpd_graph H => (e0 y).1) b) $o F $==
Id G cbn.
G, H: ZeroGpd
F: G $-> H
e0: forall b : zerogpd_graph H,
{a : zerogpd_graph G & F a $== b}
e1: forall x y : zerogpd_graph G,
F x $== F y -> x $== y
NatTrans.Transformation (fun x : G => (e0 (F x)).1)
  idmap  intro x.
G, H: ZeroGpd
F: G $-> H
e0: forall b : zerogpd_graph H,
{a : zerogpd_graph G & F a $== b}
e1: forall x y : zerogpd_graph 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 : zerogpd_graph H,
{a : zerogpd_graph G & F a $== b}
e1: forall x y : zerogpd_graph G,
F x $== F y -> x $== y
x: G
F (e0 (F x)).1 $== F x
    apply e0.
Defined.

(** ** Induced 0-groupoid structures *)

Definition zerogpd_induced {A : Type} {G : ZeroGpd} (f : A -> G)
  : ZeroGpd
  := Build_ZeroGpd A (isgraph_induced f) (is01cat_induced f) (is0gpd_induced f).

Definition zerogpd_induced_map {A : Type} {G : ZeroGpd} (f : A -> G)
  : zerogpd_induced f $-> G.
A: Type
G: ZeroGpd
f: A -> G
zerogpd_induced f $-> G
Proof.
A: Type
G: ZeroGpd
f: A -> G
zerogpd_induced f $-> G
  napply (Build_Fun01' f).
A: Type
G: ZeroGpd
f: A -> G
forall a b : A, (a $-> b) -> f a $-> f b
  intros a b; exact idmap.
Defined.

(** ** Products of families of 0-groupoids *)

(** Here we define products of families of 0-groupoids. *)

(** [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
  apply (Build_Fun01' (fun f => f i)); cbn beta.
I: Type
G: I -> ZeroGpd
i: I
forall a b : forall x : I, G x,
(a $-> b) -> a i $-> b i
  intros f g p.
I: Type
G: I -> ZeroGpd
i: I
f, g: forall x : I, G x
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)
  snapply 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
    apply (Build_Fun01' (fun x i => f i x)).
I: Type
G: ZeroGpd
H: I -> ZeroGpd
f: forall i : I, G $-> H i
forall a b : zerogpd_graph G,
(a $-> b) ->
(fun i : I => f i a) $-> (fun i : I => f i b)
    intros x y p i.
I: Type
G: ZeroGpd
H: I -> ZeroGpd
f: forall i : I, G $-> H i
x, y: zerogpd_graph 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 =>
   Build_Fun01'
     (fun (x : zerogpd_graph G) (i : I) => f i x)
     (fun (x y : zerogpd_graph G) (p : x $-> y) =>
      (fun i : I => fmap (f i) p)
      :
      (fun i : I => f i x) $-> (fun i : I => f i y)))
  snapply 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 =>
 Build_Fun01'
   (fun (x : zerogpd_graph G) (i : I) => f i x)
   (fun (x y : zerogpd_graph G) (p : x $-> y) =>
    (fun i : I => fmap (f i) p)
    :
    (fun i : I => f i x) $-> (fun i : I => f i y)))
o ?equiv_inv == idmap
I: Type
G: ZeroGpd
H: I -> ZeroGpd
?equiv_inv
o (fun f : forall i : I, G $-> H i =>
   Build_Fun01'
     (fun (x : zerogpd_graph G) (i : I) => f i x)
     (fun (x y : zerogpd_graph G) (p : x $-> y) =>
      (fun i : I => fmap (f i) p)
      :
      (fun i : I => f i x) $-> (fun i : I => f i y))) ==
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 =>
    Build_Fun01'
      (fun (x0 : zerogpd_graph G) (i : I) => f i x0)
      (fun (x0 y : zerogpd_graph G) (p : x0 $-> y) =>
       (fun i : I => fmap (f i) p)
       :
       (fun i : I => f i x0) $-> (fun i : I => f i y)))
     x) =
ap
  (fun f : forall i : I, G $-> H i =>
   Build_Fun01'
     (fun (x0 : zerogpd_graph G) (i : I) => f i x0)
     (fun (x0 y : zerogpd_graph G) (p : x0 $-> y) =>
      (fun i : I => fmap (f i) p)
      :
      (fun i : I => f i x0) $-> (fun i : I => f i y)))
  (?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 =>
 Build_Fun01'
   (fun (x : zerogpd_graph G) (i : I) => f i x)
   (fun (x y : zerogpd_graph G) (p : x $-> y) =>
    (fun i : I => fmap (f i) p)
    :
    (fun i : I => f i x) $-> (fun i : I => f i y)))
o (fun (f : G $-> prod_0gpd I H) (i : I) =>
   prod_0gpd_pr i $o f) == idmap
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 =>
   Build_Fun01'
     (fun (x : zerogpd_graph G) (i : I) => f i x)
     (fun (x y : zerogpd_graph G) (p : x $-> y) =>
      (fun i : I => fmap (f i) p)
      :
      (fun i : I => f i x) $-> (fun i : I => f i y))) ==
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 =>
    Build_Fun01'
      (fun (x0 : zerogpd_graph G) (i : I) => f i x0)
      (fun (x0 y : zerogpd_graph G) (p : x0 $-> y) =>
       (fun i : I => fmap (f i) p)
       :
       (fun i : I => f i x0) $-> (fun i : I => f i y)))
     x) =
ap
  (fun f : forall i : I, G $-> H i =>
   Build_Fun01'
     (fun (x0 : zerogpd_graph G) (i : I) => f i x0)
     (fun (x0 y : zerogpd_graph G) (p : x0 $-> y) =>
      (fun i : I => fmap (f i) p)
      :
      (fun i : I => f i x0) $-> (fun i : I => f i y)))
  (?eissect x)
  all: 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
  snapply 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 snapply Build_Fun01'.
I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
zerogpd_graph (prod_0gpd I G) ->
zerogpd_graph (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)
forall a b : zerogpd_graph (prod_0gpd I G),
(a $-> b) -> ?F a $-> ?F b
    +
I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
zerogpd_graph (prod_0gpd I G) ->
zerogpd_graph (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: zerogpd_graph (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)
forall a b : zerogpd_graph (prod_0gpd I G),
(a $-> b) ->
(fun h : zerogpd_graph (prod_0gpd I G) =>
 (fun j : J =>
  transport (fun x : J => H x) (eisretr ie j)
    (f (ie^-1 j) (h (ie^-1 j))))
 :
 zerogpd_graph (prod_0gpd J H)) a $->
(fun h : zerogpd_graph (prod_0gpd I G) =>
 (fun j : J =>
  transport (fun x : J => H x) (eisretr ie j)
    (f (ie^-1 j) (h (ie^-1 j))))
 :
 zerogpd_graph (prod_0gpd J H)) b cbn.
I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
forall a b : forall i : I, G i,
(forall a0 : I, a a0 $-> b a0) ->
forall a0 : J,
transport (fun x : J => H x) (eisretr ie a0)
  (f (ie^-1 a0) (a (ie^-1 a0))) $->
transport (fun x : J => H x) (eisretr ie a0)
  (f (ie^-1 a0) (b (ie^-1 a0))) 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: forall i : I, G i
p: forall a : I, g a $-> h a
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); simpl.
I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
g, h: forall i : I, G i
p: forall a : I, g a $-> h a
j: J
f (ie^-1 j) (g (ie^-1 j)) $->
f (ie^-1 j) (h (ie^-1 j))
      exact (fmap _ (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)
Build_Fun01'
  (fun h : zerogpd_graph (prod_0gpd I G) =>
   (fun j : J =>
    transport (fun x : J => H x) (eisretr ie j)
      (f (ie^-1 j) (h (ie^-1 j))))
   :
   zerogpd_graph (prod_0gpd J H))
  ((fun (g h : forall i : I, G i)
      (p : forall a : I, g a $-> h a) (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 =>
        fmap (f (ie^-1 j)) (p (ie^-1 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)))
    end)
   :
   forall a b : zerogpd_graph (prod_0gpd I G),
   (a $-> b) ->
   (fun h : zerogpd_graph (prod_0gpd I G) =>
    (fun j : J =>
     transport (fun x : J => H x) (eisretr ie j)
       (f (ie^-1 j) (h (ie^-1 j))))
    :
    zerogpd_graph (prod_0gpd J H)) a $->
   (fun h : zerogpd_graph (prod_0gpd I G) =>
    (fun j : J =>
     transport (fun x : J => H x) (eisretr ie j)
       (f (ie^-1 j) (h (ie^-1 j))))
    :
    zerogpd_graph (prod_0gpd J H)) b) $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; cbn.
I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
h: zerogpd_graph (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); simpl.
I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
h: zerogpd_graph (prod_0gpd J H)
j: J
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
Build_Fun01'
  (fun h : zerogpd_graph (prod_0gpd I G) =>
   (fun j : J =>
    transport (fun x : J => H x) (eisretr ie j)
      (f (ie^-1 j) (h (ie^-1 j))))
   :
   zerogpd_graph (prod_0gpd J H))
  ((fun (g h : forall i : I, G i)
      (p : forall a : I, g a $-> h a) (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 =>
        fmap (f (ie^-1 j)) (p (ie^-1 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)))
    end)
   :
   forall a b : zerogpd_graph (prod_0gpd I G),
   (a $-> b) ->
   (fun h : zerogpd_graph (prod_0gpd I G) =>
    (fun j : J =>
     transport (fun x : J => H x) (eisretr ie j)
       (f (ie^-1 j) (h (ie^-1 j))))
    :
    zerogpd_graph (prod_0gpd J H)) a $->
   (fun h : zerogpd_graph (prod_0gpd I G) =>
    (fun j : J =>
     transport (fun x : J => H x) (eisretr ie j)
       (f (ie^-1 j) (h (ie^-1 j))))
    :
    zerogpd_graph (prod_0gpd J H)) b) $==
Id (prod_0gpd I G) intros 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: zerogpd_graph (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: zerogpd_graph (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); simpl.
I, J: Type
ie: I <~> J
G: I -> ZeroGpd
H: J -> ZeroGpd
f: forall i : I, G i $<~> H (ie i)
g: zerogpd_graph (prod_0gpd I G)
i: I
cat_equiv_inv (f (ie^-1 (ie i)))
  (f (ie^-1 (ie i)) (g (ie^-1 (ie i)))) $->
g (ie^-1 (ie i))
    exact (cate_issect (f _) _).
Defined.

(** ** Binary products of 0-groupoids *)

(** Binary products can be obtained from indexed products by indexing over [Bool], and indeed this follows from [hasbinaryproducts_hasproductsbool] in WildCat.Products.  However, we can avoid [Funext] in [equiv_binprod_0gpd_corec] if we separately define binary products of 0-groupoids using the product of types. *)

Section BinProd.

  Context (G H : ZeroGpd).

  (** This uses instances from WildCat.Prod. *)
  Definition binprod_0gpd : ZeroGpd
    := Build_ZeroGpd (G * H) _ _ _.

  (* Helper function to produce a term of binprod_0gpd. *)
  Definition binprod_0gpd_pair (g : G) (h : H) : binprod_0gpd
    := (g, h).

  (** The projections. *)
  Definition binprod_0gpd_pr1 : binprod_0gpd $-> G.
G, H: ZeroGpd
binprod_0gpd $-> G
  Proof.
G, H: ZeroGpd
binprod_0gpd $-> G
    snapply (Build_Fun01' fst).
G, H: ZeroGpd
forall a b : G * H, (a $-> b) -> fst a $-> fst b
    intros f g.
G, H: ZeroGpd
f, g: G * H
(f $-> g) -> fst f $-> fst g  exact fst.
  Defined.

  Definition binprod_0gpd_pr2 : binprod_0gpd $-> H.
G, H: ZeroGpd
binprod_0gpd $-> H
  Proof.
G, H: ZeroGpd
binprod_0gpd $-> H
    snapply (Build_Fun01' snd).
G, H: ZeroGpd
forall a b : G * H, (a $-> b) -> snd a $-> snd b
    intros f g.
G, H: ZeroGpd
f, g: G * H
(f $-> g) -> snd f $-> snd g  exact snd.
  Defined.

  (** The universal property of the product of 0-groupoids holds almost definitionally. *)
  Definition equiv_binprod_0gpd_corec (K : ZeroGpd)
    : (K $-> G) * (K $-> H) <~> (K $-> binprod_0gpd).
G, H, K: ZeroGpd
(K $-> G) * (K $-> H) <~> (K $-> binprod_0gpd)
  Proof.
G, H, K: ZeroGpd
(K $-> G) * (K $-> H) <~> (K $-> binprod_0gpd)
    snapply Build_Equiv.
G, H, K: ZeroGpd
(K $-> G) * (K $-> H) -> K $-> binprod_0gpd
G, H, K: ZeroGpd
IsEquiv ?equiv_fun
    {
G, H, K: ZeroGpd
(K $-> G) * (K $-> H) -> K $-> binprod_0gpd intros [f g].
G, H, K: ZeroGpd
f: K $-> G
g: K $-> H
K $-> binprod_0gpd
      snapply (Build_Fun01' (fun k => (f k, g k))); cbn.
G, H, K: ZeroGpd
f: K $-> G
g: K $-> H
forall a b : K,
(a $-> b) -> (f a $-> f b) * (g a $-> g b)
      intros x y p.
G, H, K: ZeroGpd
f: K $-> G
g: K $-> H
x, y: K
p: x $-> y
(f x $-> f y) * (g x $-> g y)  exact (fmap f p, fmap g p). }
G, H, K: ZeroGpd
IsEquiv
  (fun X : (K $-> G) * (K $-> H) =>
   (fun (f : K $-> G) (g : K $-> H) =>
    Build_Fun01'
      (fun k : zerogpd_graph K => (f k, g k))
      ((fun (x y : K) (p : x $-> y) =>
        (fmap f p, fmap g p))
       :
       forall a b : zerogpd_graph K,
       (a $-> b) ->
       (fun k : zerogpd_graph K => (f k, g k)) a $->
       (fun k : zerogpd_graph K => (f k, g k)) b))
     (fst X) (snd X))
    snapply Build_IsEquiv.
G, H, K: ZeroGpd
(K $-> binprod_0gpd) -> (K $-> G) * (K $-> H)
G, H, K: ZeroGpd
(fun X : (K $-> G) * (K $-> H) =>
 (fun (f : K $-> G) (g : K $-> H) =>
  Build_Fun01' (fun k : zerogpd_graph K => (f k, g k))
    ((fun (x y : K) (p : x $-> y) =>
      (fmap f p, fmap g p))
     :
     forall a b : zerogpd_graph K,
     (a $-> b) ->
     (fun k : zerogpd_graph K => (f k, g k)) a $->
     (fun k : zerogpd_graph K => (f k, g k)) b))
   (fst X) (snd X)) o ?equiv_inv == idmap
G, H, K: ZeroGpd
?equiv_inv
o (fun X : (K $-> G) * (K $-> H) =>
   (fun (f : K $-> G) (g : K $-> H) =>
    Build_Fun01'
      (fun k : zerogpd_graph K => (f k, g k))
      ((fun (x y : K) (p : x $-> y) =>
        (fmap f p, fmap g p))
       :
       forall a b : zerogpd_graph K,
       (a $-> b) ->
       (fun k : zerogpd_graph K => (f k, g k)) a $->
       (fun k : zerogpd_graph K => (f k, g k)) b))
     (fst X) (snd X)) == idmap
G, H, K: ZeroGpd
forall x : (K $-> G) * (K $-> H),
?eisretr
  ((fun X : (K $-> G) * (K $-> H) =>
    (fun (f : K $-> G) (g : K $-> H) =>
     Build_Fun01'
       (fun k : zerogpd_graph K => (f k, g k))
       ((fun (x0 y : K) (p : x0 $-> y) =>
         (fmap f p, fmap g p))
        :
        forall a b : zerogpd_graph K,
        (a $-> b) ->
        (fun k : zerogpd_graph K => (f k, g k)) a $->
        (fun k : zerogpd_graph K => (f k, g k)) b))
      (fst X) (snd X)) x) =
ap
  (fun X : (K $-> G) * (K $-> H) =>
   (fun (f : K $-> G) (g : K $-> H) =>
    Build_Fun01'
      (fun k : zerogpd_graph K => (f k, g k))
      ((fun (x0 y : K) (p : x0 $-> y) =>
        (fmap f p, fmap g p))
       :
       forall a b : zerogpd_graph K,
       (a $-> b) ->
       (fun k : zerogpd_graph K => (f k, g k)) a $->
       (fun k : zerogpd_graph K => (f k, g k)) b))
     (fst X) (snd X)) (?eissect x)
    1: exact (fun f => (binprod_0gpd_pr1 $o f, binprod_0gpd_pr2 $o f)).
G, H, K: ZeroGpd
(fun X : (K $-> G) * (K $-> H) =>
 (fun (f : K $-> G) (g : K $-> H) =>
  Build_Fun01' (fun k : zerogpd_graph K => (f k, g k))
    ((fun (x y : K) (p : x $-> y) =>
      (fmap f p, fmap g p))
     :
     forall a b : zerogpd_graph K,
     (a $-> b) ->
     (fun k : zerogpd_graph K => (f k, g k)) a $->
     (fun k : zerogpd_graph K => (f k, g k)) b))
   (fst X) (snd X))
o (fun f : K $-> binprod_0gpd =>
   (binprod_0gpd_pr1 $o f, binprod_0gpd_pr2 $o f)) ==
idmap
G, H, K: ZeroGpd
(fun f : K $-> binprod_0gpd =>
 (binprod_0gpd_pr1 $o f, binprod_0gpd_pr2 $o f))
o (fun X : (K $-> G) * (K $-> H) =>
   (fun (f : K $-> G) (g : K $-> H) =>
    Build_Fun01'
      (fun k : zerogpd_graph K => (f k, g k))
      ((fun (x y : K) (p : x $-> y) =>
        (fmap f p, fmap g p))
       :
       forall a b : zerogpd_graph K,
       (a $-> b) ->
       (fun k : zerogpd_graph K => (f k, g k)) a $->
       (fun k : zerogpd_graph K => (f k, g k)) b))
     (fst X) (snd X)) == idmap
G, H, K: ZeroGpd
forall x : (K $-> G) * (K $-> H),
?eisretr
  ((fun X : (K $-> G) * (K $-> H) =>
    (fun (f : K $-> G) (g : K $-> H) =>
     Build_Fun01'
       (fun k : zerogpd_graph K => (f k, g k))
       ((fun (x0 y : K) (p : x0 $-> y) =>
         (fmap f p, fmap g p))
        :
        forall a b : zerogpd_graph K,
        (a $-> b) ->
        (fun k : zerogpd_graph K => (f k, g k)) a $->
        (fun k : zerogpd_graph K => (f k, g k)) b))
      (fst X) (snd X)) x) =
ap
  (fun X : (K $-> G) * (K $-> H) =>
   (fun (f : K $-> G) (g : K $-> H) =>
    Build_Fun01'
      (fun k : zerogpd_graph K => (f k, g k))
      ((fun (x0 y : K) (p : x0 $-> y) =>
        (fmap f p, fmap g p))
       :
       forall a b : zerogpd_graph K,
       (a $-> b) ->
       (fun k : zerogpd_graph K => (f k, g k)) a $->
       (fun k : zerogpd_graph K => (f k, g k)) b))
     (fst X) (snd X)) (?eissect x)
    all: reflexivity.
  Defined.

End BinProd.

(** ** The terminal 0-groupoid *)

Definition Unit_0gpd : ZeroGpd := Build_ZeroGpd Unit _ _ _.

Instance is_terminal_unit_0gpd : IsTerminal Unit_0gpd.
IsTerminal Unit_0gpd
Proof.
IsTerminal Unit_0gpd
  intro A.
A: ZeroGpd
{f : A $-> Unit_0gpd &
forall g : A $-> Unit_0gpd, f $== g}
  pose proof (f:=Build_Fun01 (fun _ : A => tt)).
A: ZeroGpd
f: Fun01 A Unit
{f : A $-> Unit_0gpd &
forall g : A $-> Unit_0gpd, f $== g}
  exists f.
A: ZeroGpd
f: Fun01 A Unit
forall g : A $-> Unit_0gpd, f $== g
  intros g a; simpl.
A: ZeroGpd
f: Fun01 A Unit
g: A $-> Unit_0gpd
a: zerogpd_graph A
Unit
  exact tt.
Defined.

(** ** Pullbacks of 0-groupoids *)

Section ZeroGpdPullback.

  Context {G H K : ZeroGpd} (g : G $-> K) (h : H $-> K).

  (* The underlying type for the pullback of 0-groupoids is [{x : G & { y : H & g x $== h y }}].

  The pullbacks we define here do not assume any 2-cells, so the 1-cells in the pullback only involve the corners [G] and [H] and can therefore be induced from the product of these 0-groupoids.  (Because of this, this definition would not give the correct notion of pullback of types when we regard types as 0-groupoids.) *)

  Definition pullback_0gpd : ZeroGpd
    := @zerogpd_induced {x : G & { y : H & g x $== h y }} (binprod_0gpd G H)
        (fun '(x; (y; p)) => (x, y)).

  Definition pullback_0gpd_pr1 : pullback_0gpd $-> G
    := binprod_0gpd_pr1 G H $o zerogpd_induced_map _.

  Definition pullback_0gpd_pr2 : pullback_0gpd $-> H
    := binprod_0gpd_pr2 G H $o zerogpd_induced_map _.

  Definition pullback_0gpd_glue : g $o pullback_0gpd_pr1 $== h $o pullback_0gpd_pr2
    := fun '(x; (y; p)) => p.

  (** The universal property of the product of 0-groupoids holds almost definitionally. *)
  Definition equiv_pullback_0gpd_corec {Z : ZeroGpd}
    : { f1 : Z $-> G & { f2 : Z $-> H & g $o f1 $== h $o f2 }}
        <~> (Z $-> pullback_0gpd).
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
{f1 : Z $-> G & {f2 : Z $-> H & g $o f1 $== h $o f2}} <~>
(Z $-> pullback_0gpd)
  Proof.
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
{f1 : Z $-> G & {f2 : Z $-> H & g $o f1 $== h $o f2}} <~>
(Z $-> pullback_0gpd)
    snapply Build_Equiv.
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
{f1 : Z $-> G & {f2 : Z $-> H & g $o f1 $== h $o f2}} ->
Z $-> pullback_0gpd
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
IsEquiv ?equiv_fun
    {
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
{f1 : Z $-> G & {f2 : Z $-> H & g $o f1 $== h $o f2}} ->
Z $-> pullback_0gpd intros [f1 [f2 q]].
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
f1: Z $-> G
f2: Z $-> H
q: g $o f1 $== h $o f2
Z $-> pullback_0gpd
      snapply Build_Fun01'.
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
f1: Z $-> G
f2: Z $-> H
q: g $o f1 $== h $o f2
zerogpd_graph Z -> zerogpd_graph pullback_0gpd
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
f1: Z $-> G
f2: Z $-> H
q: g $o f1 $== h $o f2
forall a b : zerogpd_graph Z,
(a $-> b) -> ?F a $-> ?F b
      +
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
f1: Z $-> G
f2: Z $-> H
q: g $o f1 $== h $o f2
zerogpd_graph Z -> zerogpd_graph pullback_0gpd exact (fun z => (f1 z; (f2 z; q z))).
      +
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
f1: Z $-> G
f2: Z $-> H
q: g $o f1 $== h $o f2
forall a b : zerogpd_graph Z,
(a $-> b) ->
(fun z : zerogpd_graph Z => (f1 z; f2 z; q z)) a $->
(fun z : zerogpd_graph Z => (f1 z; f2 z; q z)) b intros z z' p; cbn beta.
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
f1: Z $-> G
f2: Z $-> H
q: g $o f1 $== h $o f2
z, z': zerogpd_graph Z
p: z $-> z'
(f1 z; f2 z; q z) $-> (f1 z'; f2 z'; q z')
        exact (fmap f1 p, fmap f2 p). }
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
IsEquiv
  (fun
     X : {f1 : Z $-> G &
         {f2 : Z $-> H & g $o f1 $== h $o f2}} =>
   (fun (f1 : Z $-> G)
      (proj2 : {f2 : Z $-> H & g $o f1 $== h $o f2})
    =>
    (fun (f2 : Z $-> H) (q : g $o f1 $== h $o f2) =>
     Build_Fun01'
       (fun z : zerogpd_graph Z => (f1 z; f2 z; q z))
       (fun (z z' : zerogpd_graph Z) (p : z $-> z') =>
        (fmap f1 p, fmap f2 p)
        :
        (fun z0 : zerogpd_graph Z =>
         (f1 z0; f2 z0; q z0)) z $->
        (fun z0 : zerogpd_graph Z =>
         (f1 z0; f2 z0; q z0)) z')) proj2.1 proj2.2)
     X.1 X.2)
    snapply Build_IsEquiv.
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
(Z $-> pullback_0gpd) ->
{f1 : Z $-> G & {f2 : Z $-> H & g $o f1 $== h $o f2}}
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
(fun
   X : {f1 : Z $-> G &
       {f2 : Z $-> H & g $o f1 $== h $o f2}} =>
 (fun (f1 : Z $-> G)
    (proj2 : {f2 : Z $-> H & g $o f1 $== h $o f2}) =>
  (fun (f2 : Z $-> H) (q : g $o f1 $== h $o f2) =>
   Build_Fun01'
     (fun z : zerogpd_graph Z => (f1 z; f2 z; q z))
     (fun (z z' : zerogpd_graph Z) (p : z $-> z') =>
      (fmap f1 p, fmap f2 p)
      :
      (fun z0 : zerogpd_graph Z =>
       (f1 z0; f2 z0; q z0)) z $->
      (fun z0 : zerogpd_graph Z =>
       (f1 z0; f2 z0; q z0)) z')) proj2.1 proj2.2) X.1
   X.2) o ?equiv_inv == idmap
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
?equiv_inv
o (fun
     X : {f1 : Z $-> G &
         {f2 : Z $-> H & g $o f1 $== h $o f2}} =>
   (fun (f1 : Z $-> G)
      (proj2 : {f2 : Z $-> H & g $o f1 $== h $o f2})
    =>
    (fun (f2 : Z $-> H) (q : g $o f1 $== h $o f2) =>
     Build_Fun01'
       (fun z : zerogpd_graph Z => (f1 z; f2 z; q z))
       (fun (z z' : zerogpd_graph Z) (p : z $-> z') =>
        (fmap f1 p, fmap f2 p)
        :
        (fun z0 : zerogpd_graph Z =>
         (f1 z0; f2 z0; q z0)) z $->
        (fun z0 : zerogpd_graph Z =>
         (f1 z0; f2 z0; q z0)) z')) proj2.1 proj2.2)
     X.1 X.2) == idmap
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
forall
x : {f1 : Z $-> G &
    {f2 : Z $-> H & g $o f1 $== h $o f2}},
?eisretr
  ((fun
      X : {f1 : Z $-> G &
          {f2 : Z $-> H & g $o f1 $== h $o f2}} =>
    (fun (f1 : Z $-> G)
       (proj2 : {f2 : Z $-> H & g $o f1 $== h $o f2})
     =>
     (fun (f2 : Z $-> H) (q : g $o f1 $== h $o f2) =>
      Build_Fun01'
        (fun z : zerogpd_graph Z => (f1 z; f2 z; q z))
        (fun (z z' : zerogpd_graph Z) (p : z $-> z')
         =>
         (fmap f1 p, fmap f2 p)
         :
         (fun z0 : zerogpd_graph Z =>
          (f1 z0; f2 z0; q z0)) z $->
         (fun z0 : zerogpd_graph Z =>
          (f1 z0; f2 z0; q z0)) z')) proj2.1 proj2.2)
      X.1 X.2) x) =
ap
  (fun
     X : {f1 : Z $-> G &
         {f2 : Z $-> H & g $o f1 $== h $o f2}} =>
   (fun (f1 : Z $-> G)
      (proj2 : {f2 : Z $-> H & g $o f1 $== h $o f2})
    =>
    (fun (f2 : Z $-> H) (q : g $o f1 $== h $o f2) =>
     Build_Fun01'
       (fun z : zerogpd_graph Z => (f1 z; f2 z; q z))
       (fun (z z' : zerogpd_graph Z) (p : z $-> z') =>
        (fmap f1 p, fmap f2 p)
        :
        (fun z0 : zerogpd_graph Z =>
         (f1 z0; f2 z0; q z0)) z $->
        (fun z0 : zerogpd_graph Z =>
         (f1 z0; f2 z0; q z0)) z')) proj2.1 proj2.2)
     X.1 X.2) (?eissect x)
    {
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
(Z $-> pullback_0gpd) ->
{f1 : Z $-> G & {f2 : Z $-> H & g $o f1 $== h $o f2}} intro f.
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
f: Z $-> pullback_0gpd
{f1 : Z $-> G & {f2 : Z $-> H & g $o f1 $== h $o f2}}
      srefine (pullback_0gpd_pr1 $o f; pullback_0gpd_pr2 $o f; _).
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
f: Z $-> pullback_0gpd
(fun f2 : Z $-> H =>
 g $o (pullback_0gpd_pr1 $o f) $== h $o f2)
  (pullback_0gpd_pr2 $o f)
      cbn beta.
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
f: Z $-> pullback_0gpd
g $o (pullback_0gpd_pr1 $o f) $==
h $o (pullback_0gpd_pr2 $o f)
      exact (fun z => pullback_0gpd_glue (f z)). }
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
(fun
   X : {f1 : Z $-> G &
       {f2 : Z $-> H & g $o f1 $== h $o f2}} =>
 (fun (f1 : Z $-> G)
    (proj2 : {f2 : Z $-> H & g $o f1 $== h $o f2}) =>
  (fun (f2 : Z $-> H) (q : g $o f1 $== h $o f2) =>
   Build_Fun01'
     (fun z : zerogpd_graph Z => (f1 z; f2 z; q z))
     (fun (z z' : zerogpd_graph Z) (p : z $-> z') =>
      (fmap f1 p, fmap f2 p)
      :
      (fun z0 : zerogpd_graph Z =>
       (f1 z0; f2 z0; q z0)) z $->
      (fun z0 : zerogpd_graph Z =>
       (f1 z0; f2 z0; q z0)) z')) proj2.1 proj2.2) X.1
   X.2)
o (fun f : Z $-> pullback_0gpd =>
   (pullback_0gpd_pr1 $o f; pullback_0gpd_pr2 $o f;
   (fun z : zerogpd_graph Z =>
    pullback_0gpd_glue (f z))
   :
   (fun f2 : Z $-> H =>
    g $o (pullback_0gpd_pr1 $o f) $== h $o f2)
     (pullback_0gpd_pr2 $o f))) == idmap
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
(fun f : Z $-> pullback_0gpd =>
 (pullback_0gpd_pr1 $o f; pullback_0gpd_pr2 $o f;
 (fun z : zerogpd_graph Z => pullback_0gpd_glue (f z))
 :
 (fun f2 : Z $-> H =>
  g $o (pullback_0gpd_pr1 $o f) $== h $o f2)
   (pullback_0gpd_pr2 $o f)))
o (fun
     X : {f1 : Z $-> G &
         {f2 : Z $-> H & g $o f1 $== h $o f2}} =>
   (fun (f1 : Z $-> G)
      (proj2 : {f2 : Z $-> H & g $o f1 $== h $o f2})
    =>
    (fun (f2 : Z $-> H) (q : g $o f1 $== h $o f2) =>
     Build_Fun01'
       (fun z : zerogpd_graph Z => (f1 z; f2 z; q z))
       (fun (z z' : zerogpd_graph Z) (p : z $-> z') =>
        (fmap f1 p, fmap f2 p)
        :
        (fun z0 : zerogpd_graph Z =>
         (f1 z0; f2 z0; q z0)) z $->
        (fun z0 : zerogpd_graph Z =>
         (f1 z0; f2 z0; q z0)) z')) proj2.1 proj2.2)
     X.1 X.2) == idmap
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
Z: ZeroGpd
forall
x : {f1 : Z $-> G &
    {f2 : Z $-> H & g $o f1 $== h $o f2}},
?eisretr
  ((fun
      X : {f1 : Z $-> G &
          {f2 : Z $-> H & g $o f1 $== h $o f2}} =>
    (fun (f1 : Z $-> G)
       (proj2 : {f2 : Z $-> H & g $o f1 $== h $o f2})
     =>
     (fun (f2 : Z $-> H) (q : g $o f1 $== h $o f2) =>
      Build_Fun01'
        (fun z : zerogpd_graph Z => (f1 z; f2 z; q z))
        (fun (z z' : zerogpd_graph Z) (p : z $-> z')
         =>
         (fmap f1 p, fmap f2 p)
         :
         (fun z0 : zerogpd_graph Z =>
          (f1 z0; f2 z0; q z0)) z $->
         (fun z0 : zerogpd_graph Z =>
          (f1 z0; f2 z0; q z0)) z')) proj2.1 proj2.2)
      X.1 X.2) x) =
ap
  (fun
     X : {f1 : Z $-> G &
         {f2 : Z $-> H & g $o f1 $== h $o f2}} =>
   (fun (f1 : Z $-> G)
      (proj2 : {f2 : Z $-> H & g $o f1 $== h $o f2})
    =>
    (fun (f2 : Z $-> H) (q : g $o f1 $== h $o f2) =>
     Build_Fun01'
       (fun z : zerogpd_graph Z => (f1 z; f2 z; q z))
       (fun (z z' : zerogpd_graph Z) (p : z $-> z') =>
        (fmap f1 p, fmap f2 p)
        :
        (fun z0 : zerogpd_graph Z =>
         (f1 z0; f2 z0; q z0)) z $->
        (fun z0 : zerogpd_graph Z =>
         (f1 z0; f2 z0; q z0)) z')) proj2.1 proj2.2)
     X.1 X.2) (?eissect x)
    all: reflexivity.
  Defined.

  (** The square brackets denote a non-maximally inserted implicit argument. *)
  Definition pullback_0gpd_homotopic [Z : ZeroGpd]
    (j k : Z $-> pullback_0gpd)
    (p1 : pullback_0gpd_pr1 $o j $== pullback_0gpd_pr1 $o k)
    (p2 : pullback_0gpd_pr2 $o j $== pullback_0gpd_pr2 $o k)
    : j $== k
    := fun z => (p1 z, p2 z).

End ZeroGpdPullback.

(** Taking pullbacks of 0-groupoids is symmetric. *)
Definition flip_pullback_0gpd {G H K : ZeroGpd} (g : G $-> K) (h : H $-> K)
  : pullback_0gpd g h $-> pullback_0gpd h g.
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
pullback_0gpd g h $-> pullback_0gpd h g
Proof.
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
pullback_0gpd g h $-> pullback_0gpd h g
  snapply Build_Fun01'.
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
zerogpd_graph (pullback_0gpd g h) ->
zerogpd_graph (pullback_0gpd h g)
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
forall a b : zerogpd_graph (pullback_0gpd g h),
(a $-> b) -> ?F a $-> ?F b
  -
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
zerogpd_graph (pullback_0gpd g h) ->
zerogpd_graph (pullback_0gpd h g) intros [x [y p]]; exact (y; (x; p^$)).
  -
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
forall a b : zerogpd_graph (pullback_0gpd g h),
(a $-> b) ->
(fun X : zerogpd_graph (pullback_0gpd g h) =>
 (fun (x : G) (proj2 : {y : H & g x $== h y}) =>
  (fun (y : H) (p : g x $== h y) => (y; x; p^$))
    proj2.1 proj2.2) X.1 X.2) a $->
(fun X : zerogpd_graph (pullback_0gpd g h) =>
 (fun (x : G) (proj2 : {y : H & g x $== h y}) =>
  (fun (y : H) (p : g x $== h y) => (y; x; p^$))
    proj2.1 proj2.2) X.1 X.2) b cbn.
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
forall a b : {x : G & {y : H & g x $== h y}},
(a.1 $-> b.1) * ((a.2).1 $-> (b.2).1) ->
((a.2).1 $-> (b.2).1) * (a.1 $-> b.1) intros ? ? [q1 q2]; exact (q2, q1).
Defined.

Definition involutive_flip_pullback_0gpd {G H K : ZeroGpd} (g : G $-> K) (h : H $-> K)
  : flip_pullback_0gpd g h $o flip_pullback_0gpd h g $== Id _.
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
flip_pullback_0gpd g h $o flip_pullback_0gpd h g $==
Id (pullback_0gpd h g)
Proof.
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
flip_pullback_0gpd g h $o flip_pullback_0gpd h g $==
Id (pullback_0gpd h g)
  intros ?; cbn; split; reflexivity.
Defined.

Definition cate_flip_pullback_0gpd {G H K : ZeroGpd} (g : G $-> K) (h : H $-> K)
  : pullback_0gpd g h $<~> pullback_0gpd h g.
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
pullback_0gpd g h $<~> pullback_0gpd h g
Proof.
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
pullback_0gpd g h $<~> pullback_0gpd h g
  snapply cate_adjointify.
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
pullback_0gpd g h $-> pullback_0gpd h g
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
pullback_0gpd h g $-> pullback_0gpd g h
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
?f $o ?g $== Id (pullback_0gpd h g)
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
?g $o ?f $== Id (pullback_0gpd g h)
  1,2: apply flip_pullback_0gpd.
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
flip_pullback_0gpd g h $o flip_pullback_0gpd h g $==
Id (pullback_0gpd h g)
G, H, K: ZeroGpd
g: G $-> K
h: H $-> K
flip_pullback_0gpd h g $o flip_pullback_0gpd g h $==
Id (pullback_0gpd g h)
  1,2: apply involutive_flip_pullback_0gpd.
Defined.