Require Import Basics.Overture.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Basics.Tactics.
Require Import Basics.PathGroupoids.
Require Import Types.Paths.
Require Import Colimits.Coeq.
Require Import Cubical.DPath.
Require Import WildCat.Core.
Require Import WildCat.Displayed.
Require Import WildCat.Equiv.
Require Import WildCat.EquivGpd.
Require Import WildCat.Forall.
Require Import WildCat.Paths.
Require Import WildCat.ZeroGroupoid.

(** Using wild 0-groupoids, the universal property can be proven without funext. A simple equivalence of 0-groupoids between [Coeq f g -> P] and [{ h : A -> P & h o f == h o g }] would not carry all the higher-dimensional information, but if we generalize it to dependent functions, then it does suffice. *)
Section UnivProp.
  Context {B A : Type} (f g : B -> A) (P : Coeq f g -> Type).

  (** This allows Coq to infer 0-groupoid structures of the form [@isgraph_forall C P (fun c => isgraph_paths (P c))] on any type of the form [forall c, P c]. *)
  Local Existing Instances isgraph_forall is01cat_forall is0gpd_forall | 1.
  Local Existing Instances isgraph_total is01cat_total is0gpd_total | 1.
  Local Existing Instances isgraph_paths is01cat_paths is0gpd_paths | 2.

  (** The codomain of the equivalence is a sigma-groupoid of this family. *)
  Definition Coeq_ind_data (h : forall a : A, P (coeq a))
    := forall b : B, DPath P (cglue b) (h (f b)) (h (g b)).

  (** We consider [Coeq_ind_data] to be a displayed 0-groupoid, where objects over [h : forall a : A, P (coeq a)] are dependent paths as defined above and morphisms over [p : h == k] are witnesses that p commutes with the homotopies over [h] and [k]. *)
  Local Instance isdgraph_Coeq_ind_data : IsDGraph Coeq_ind_data.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
IsDGraph Coeq_ind_data
  Proof.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
IsDGraph Coeq_ind_data
    intros h k p r s.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall a : A, P (coeq a)
p: h $-> k
r: Coeq_ind_data h
s: Coeq_ind_data k
Type
    exact (forall b, ap (transport P (cglue b)) (p (f b)) @ s b = r b @ p (g b)).
  Defined.

  Local Instance isd01cat_Coeq_ind_data : IsD01Cat Coeq_ind_data.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
IsD01Cat Coeq_ind_data
  Proof.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
IsD01Cat Coeq_ind_data
    nrapply Build_IsD01Cat.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
forall (a : forall a : A, P (coeq a))
(a' : Coeq_ind_data a), DHom (Id a) a' a'
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
forall (a : forall a : A, P (coeq a))
(b c : forall a0 : A, P (coeq a0)) (g0 : b $-> c)
(f0 : a $-> b) (a' : Coeq_ind_data a)
(b' : Coeq_ind_data b) (c' : Coeq_ind_data c),
DHom g0 b' c' ->
DHom f0 a' b' -> DHom (g0 $o f0) a' c'
    -
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
forall (a : forall a : A, P (coeq a))
(a' : Coeq_ind_data a), DHom (Id a) a' a' intros h h' b; exact (concat_1p_p1 _).
    -
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
forall (a : forall a : A, P (coeq a))
(b c : forall a0 : A, P (coeq a0)) (g0 : b $-> c)
(f0 : a $-> b) (a' : Coeq_ind_data a)
(b' : Coeq_ind_data b) (c' : Coeq_ind_data c),
DHom g0 b' c' ->
DHom f0 a' b' -> DHom (g0 $o f0) a' c' intros h k j p q h' k' j' p' q' b.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k, j: forall a : A, P (coeq a)
p: k $-> j
q: h $-> k
h': Coeq_ind_data h
k': Coeq_ind_data k
j': Coeq_ind_data j
p': DHom p k' j'
q': DHom q h' k'
b: B
ap (transport P (cglue b)) ((p $o q) (f b)) @ j' b =
h' b @ (p $o q) (g b)
      lhs nrapply ap_pp_p.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k, j: forall a : A, P (coeq a)
p: k $-> j
q: h $-> k
h': Coeq_ind_data h
k': Coeq_ind_data k
j': Coeq_ind_data j
p': DHom p k' j'
q': DHom q h' k'
b: B
ap (transport P (cglue b)) (q (f b)) @
(ap (transport P (cglue b)) (p (f b)) @ j' b) =
h' b @ (p $o q) (g b)
      lhs nrapply (whiskerL _ (p' b)).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k, j: forall a : A, P (coeq a)
p: k $-> j
q: h $-> k
h': Coeq_ind_data h
k': Coeq_ind_data k
j': Coeq_ind_data j
p': DHom p k' j'
q': DHom q h' k'
b: B
ap (transport P (cglue b)) (q (f b)) @
(k' b @ p (g b)) = h' b @ (p $o q) (g b)
      lhs nrapply concat_p_pp.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k, j: forall a : A, P (coeq a)
p: k $-> j
q: h $-> k
h': Coeq_ind_data h
k': Coeq_ind_data k
j': Coeq_ind_data j
p': DHom p k' j'
q': DHom q h' k'
b: B
(ap (transport P (cglue b)) (q (f b)) @ k' b) @
p (g b) = h' b @ (p $o q) (g b)
      lhs nrapply (whiskerR (q' b)).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k, j: forall a : A, P (coeq a)
p: k $-> j
q: h $-> k
h': Coeq_ind_data h
k': Coeq_ind_data k
j': Coeq_ind_data j
p': DHom p k' j'
q': DHom q h' k'
b: B
(h' b @ q (g b)) @ p (g b) = h' b @ (p $o q) (g b)
      nrapply concat_pp_p.
  Defined.

  Local Instance isd0gpd_Coeq_ind_data : IsD0Gpd Coeq_ind_data.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
IsD0Gpd Coeq_ind_data
  Proof.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
IsD0Gpd Coeq_ind_data
    intros h k p r s p' b.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall a : A, P (coeq a)
p: h $== k
r: Coeq_ind_data h
s: Coeq_ind_data k
p': DHom p r s
b: B
ap (transport P (cglue b)) (p^$ (f b)) @ r b =
s b @ p^$ (g b)
    lhs nrapply (whiskerR (ap_V _ _)).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall a : A, P (coeq a)
p: h $== k
r: Coeq_ind_data h
s: Coeq_ind_data k
p': DHom p r s
b: B
(ap (transport P (cglue b)) (p (f b)))^ @ r b =
s b @ p^$ (g b)
    nrapply moveL_pV.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall a : A, P (coeq a)
p: h $== k
r: Coeq_ind_data h
s: Coeq_ind_data k
p': DHom p r s
b: B
((ap (transport P (cglue b)) (p (f b)))^ @ r b) @
p (g b) = s b
    lhs nrapply concat_pp_p.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall a : A, P (coeq a)
p: h $== k
r: Coeq_ind_data h
s: Coeq_ind_data k
p': DHom p r s
b: B
(ap (transport P (cglue b)) (p (f b)))^ @
(r b @ p (g b)) = s b
    lhs nrapply (whiskerL _ (p' b)^).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall a : A, P (coeq a)
p: h $== k
r: Coeq_ind_data h
s: Coeq_ind_data k
p': DHom p r s
b: B
(ap (transport P (cglue b)) (p (f b)))^ @
(ap (transport P (cglue b)) (p (f b)) @ s b) = s b
    lhs nrapply concat_p_pp.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall a : A, P (coeq a)
p: h $== k
r: Coeq_ind_data h
s: Coeq_ind_data k
p': DHom p r s
b: B
((ap (transport P (cglue b)) (p (f b)))^ @
 ap (transport P (cglue b)) (p (f b))) @ s b = s b
    lhs nrapply (whiskerR (concat_Vp _)).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall a : A, P (coeq a)
p: h $== k
r: Coeq_ind_data h
s: Coeq_ind_data k
p': DHom p r s
b: B
1 @ s b = s b
    nrapply concat_1p.
  Defined.

  (** Here is the functor. The domain is the fully-applied type of [Coeq_ind]: sections of [P] over [Coeq f g]. The codomain consists of input data for [Coeq_ind] given a 0-groupoid structure via [is0gpd_total]. *)
  Definition Coeq_ind_inv : (forall z : Coeq f g, P z) -> sig Coeq_ind_data.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
(forall z : Coeq f g, P z) ->
{x : _ & Coeq_ind_data x}
  Proof.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
(forall z : Coeq f g, P z) ->
{x : _ & Coeq_ind_data x}
    intros h.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall z : Coeq f g, P z
{x : _ & Coeq_ind_data x}
    exists (h o coeq).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall z : Coeq f g, P z
Coeq_ind_data (fun x : A => h (coeq x))
    intros b.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall z : Coeq f g, P z
b: B
DPath P (cglue b) (h (coeq (f b))) (h (coeq (g b)))
    exact (apD h (cglue b)).
  Defined.

  (** Use [Set Printing Implicit] to see the 0-groupoid structures described above. *)
  Local Instance is0functor_Coeq_ind_inv : Is0Functor Coeq_ind_inv.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
Is0Functor Coeq_ind_inv
  Proof.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
Is0Functor Coeq_ind_inv
    nrapply Build_Is0Functor.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
forall a b : forall z : Coeq f g, P z,
(a $-> b) -> Coeq_ind_inv a $-> Coeq_ind_inv b
    intros h k p.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall z : Coeq f g, P z
p: h $-> k
Coeq_ind_inv h $-> Coeq_ind_inv k
    exists (p o coeq).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall z : Coeq f g, P z
p: h $-> k
DHom (fun x : A => p (coeq x)) (Coeq_ind_inv h).2
  (Coeq_ind_inv k).2
    intros b.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall z : Coeq f g, P z
p: h $-> k
b: B
ap (transport P (cglue b)) (p (coeq (f b))) @
(Coeq_ind_inv k).2 b =
(Coeq_ind_inv h).2 b @ p (coeq (g b))
    nrapply moveL_pM.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall z : Coeq f g, P z
p: h $-> k
b: B
(ap (transport P (cglue b)) (p (coeq (f b))) @
 (Coeq_ind_inv k).2 b) @ (p (coeq (g b)))^ =
apD h (cglue b)
    exact ((apD_homotopic p (cglue b))^).
  Defined.

  Local Instance issurjinj_Coeq_ind_inv : IsSurjInj Coeq_ind_inv.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
IsSurjInj Coeq_ind_inv
  Proof.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
IsSurjInj Coeq_ind_inv
    nrapply Build_IsSurjInj.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
SplEssSurj Coeq_ind_inv
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
forall x y : forall z : Coeq f g, P z,
Coeq_ind_inv x $== Coeq_ind_inv y -> x $== y
    -
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
SplEssSurj Coeq_ind_inv intros [h r].
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall a : A, P (coeq a)
r: Coeq_ind_data h
{a : forall z : Coeq f g, P z &
Coeq_ind_inv a $== (h; r)}
      exists (Coeq_ind P h r).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall a : A, P (coeq a)
r: Coeq_ind_data h
Coeq_ind_inv (Coeq_ind P h r) $== (h; r)
      exists (fun a => idpath).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall a : A, P (coeq a)
r: Coeq_ind_data h
DHom (fun a : A => 1)
  (Coeq_ind_inv (Coeq_ind P h r)).2 r
      intros b.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall a : A, P (coeq a)
r: Coeq_ind_data h
b: B
ap (transport P (cglue b)) 1 @ r b =
(Coeq_ind_inv (Coeq_ind P h r)).2 b @ 1
      nrefine (concat_1p _ @ _ @ (concat_p1 _)^).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall a : A, P (coeq a)
r: Coeq_ind_data h
b: B
r b = apD (Coeq_ind P h r) (cglue b)
      symmetry.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h: forall a : A, P (coeq a)
r: Coeq_ind_data h
b: B
apD (Coeq_ind P h r) (cglue b) = r b
      nrapply Coeq_ind_beta_cglue.
    -
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
forall x y : forall z : Coeq f g, P z,
Coeq_ind_inv x $== Coeq_ind_inv y -> x $== y intros h k [p p'].
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall z : Coeq f g, P z
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
p': DHom p (Coeq_ind_inv h).2 (Coeq_ind_inv k).2
h $== k
      snrapply Coeq_ind.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall z : Coeq f g, P z
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
p': DHom p (Coeq_ind_inv h).2 (Coeq_ind_inv k).2
forall a : A,
(fun w : Coeq f g => h w $-> k w) (coeq a)
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall z : Coeq f g, P z
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
p': DHom p (Coeq_ind_inv h).2 (Coeq_ind_inv k).2
forall b : B,
transport (fun w : Coeq f g => h w $-> k w) (cglue b)
  (?coeq' (f b)) = ?coeq' (g b)
      1: exact p.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall z : Coeq f g, P z
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
p': DHom p (Coeq_ind_inv h).2 (Coeq_ind_inv k).2
forall b : B,
transport (fun w : Coeq f g => h w $-> k w) (cglue b)
  (p (f b)) = p (g b)
      intros b; specialize (p' b).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall z : Coeq f g, P z
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
b: B
p': ap (transport P (cglue b)) (p (f b)) @
(Coeq_ind_inv k).2 b =
(Coeq_ind_inv h).2 b @ p (g b)
transport (fun w : Coeq f g => h w $-> k w) (cglue b)
  (p (f b)) = p (g b)
      lhs nrapply transport_paths_FlFr_D.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall z : Coeq f g, P z
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
b: B
p': ap (transport P (cglue b)) (p (f b)) @
(Coeq_ind_inv k).2 b =
(Coeq_ind_inv h).2 b @ p (g b)
((apD h (cglue b))^ @
 ap (transport P (cglue b)) (p (f b))) @
apD k (cglue b) = p (g b)
      lhs nrapply concat_pp_p.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall z : Coeq f g, P z
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
b: B
p': ap (transport P (cglue b)) (p (f b)) @
(Coeq_ind_inv k).2 b =
(Coeq_ind_inv h).2 b @ p (g b)
(apD h (cglue b))^ @
(ap (transport P (cglue b)) (p (f b)) @
 apD k (cglue b)) = p (g b)
      lhs nrapply (whiskerL _ p').
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall z : Coeq f g, P z
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
b: B
p': ap (transport P (cglue b)) (p (f b)) @
(Coeq_ind_inv k).2 b =
(Coeq_ind_inv h).2 b @ p (g b)
(apD h (cglue b))^ @ ((Coeq_ind_inv h).2 b @ p (g b)) =
p (g b)
      lhs nrapply concat_p_pp.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall z : Coeq f g, P z
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
b: B
p': ap (transport P (cglue b)) (p (f b)) @
(Coeq_ind_inv k).2 b =
(Coeq_ind_inv h).2 b @ p (g b)
((apD h (cglue b))^ @ apD h (cglue b)) @ p (g b) =
p (g b)
      lhs nrapply (whiskerR (concat_Vp _)).
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
h, k: forall z : Coeq f g, P z
p: (Coeq_ind_inv h).1 $-> (Coeq_ind_inv k).1
b: B
p': ap (transport P (cglue b)) (p (f b)) @
(Coeq_ind_inv k).2 b =
(Coeq_ind_inv h).2 b @ p (g b)
1 @ p (g b) = p (g b)
      nrapply concat_1p.
  Defined.

  Definition equiv_0gpd_Coeq_ind
    : Build_ZeroGpd (forall z : Coeq f g, P z) _ _ _
      $<~> Build_ZeroGpd (sig Coeq_ind_data) _ _ _.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
{|
  carrier := forall z : Coeq f g, P z;
  isgraph_carrier := isgraph_forall (Coeq f g) P;
  is01cat_carrier := is01cat_forall (Coeq f g) P;
  is0gpd_carrier := is0gpd_forall (Coeq f g) P
|} $<~>
{|
  carrier := {x : _ & Coeq_ind_data x};
  isgraph_carrier := isgraph_total Coeq_ind_data;
  is01cat_carrier := is01cat_total Coeq_ind_data;
  is0gpd_carrier := is0gpd_total Coeq_ind_data
|}
  Proof.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
{|
  carrier := forall z : Coeq f g, P z;
  isgraph_carrier := isgraph_forall (Coeq f g) P;
  is01cat_carrier := is01cat_forall (Coeq f g) P;
  is0gpd_carrier := is0gpd_forall (Coeq f g) P
|} $<~>
{|
  carrier := {x : _ & Coeq_ind_data x};
  isgraph_carrier := isgraph_total Coeq_ind_data;
  is01cat_carrier := is01cat_total Coeq_ind_data;
  is0gpd_carrier := is0gpd_total Coeq_ind_data
|}
    snrapply Build_CatEquiv.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
{|
  carrier := forall z : Coeq f g, P z;
  isgraph_carrier := isgraph_forall (Coeq f g) P;
  is01cat_carrier := is01cat_forall (Coeq f g) P;
  is0gpd_carrier := is0gpd_forall (Coeq f g) P
|} $->
{|
  carrier := {x : _ & Coeq_ind_data x};
  isgraph_carrier := isgraph_total Coeq_ind_data;
  is01cat_carrier := is01cat_total Coeq_ind_data;
  is0gpd_carrier := is0gpd_total Coeq_ind_data
|}
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
CatIsEquiv ?f
    1: rapply Build_Morphism_0Gpd.
B, A: Type
f, g: B -> A
P: Coeq f g -> Type
CatIsEquiv
  {|
    fun_0gpd := Coeq_ind_inv;
    is0functor_fun_0gpd := is0functor_Coeq_ind_inv
  |}
    rapply isequiv_0gpd_issurjinj.
  Defined.

End UnivProp.