From HoTT Require Import Basics.From HoTT Require Import Basics.
Require Import Types.
Require Import Diagrams.ParallelPair.
Require Import Diagrams.Cocone.
Require Import Colimits.Colimit.
Require Import Colimits.Coeq.

Generalizable All Variables.

(** * Coequalizer as a colimit *)

(** In this file, we define [Coequalizer] the coequalizer of two maps as the colimit of a particular diagram, and then show that it is equivalent to [Coeq] the primitive coequalizer defined as an HIT. *)


(** ** [Coequalizer] *)

Section Coequalizer.

  Context {A B : Type}.

  Definition IsCoequalizer (f g : B -> A)
    := IsColimit (parallel_pair f g).

  Definition Coequalizer (f g : B -> A)
    := Colimit (parallel_pair f g).

  (** ** Equivalence with [Coeq] *)

  Context {f g : B -> A}.

  Definition cocone_Coeq : Cocone (parallel_pair f g) (Coeq f g).
A, B: Type
f, g: B -> A
Cocone (parallel_pair f g) (Coeq f g)
  Proof.
A, B: Type
f, g: B -> A
Cocone (parallel_pair f g) (Coeq f g)
    srapply Build_Cocone.
A, B: Type
f, g: B -> A
forall i : Graph.graph0 parallel_pair_graph,
Diagram.obj (parallel_pair f g) i -> Coeq f g
A, B: Type
f, g: B -> A
forall (i j : Graph.graph0 parallel_pair_graph)
(g0 : Graph.graph1 parallel_pair_graph i j),
?legs j o Diagram.arr (parallel_pair f g) g0 == ?legs i
    +
A, B: Type
f, g: B -> A
forall i : Graph.graph0 parallel_pair_graph,
Diagram.obj (parallel_pair f g) i -> Coeq f g intros []; [exact (coeq o g)| exact coeq].
    +
A, B: Type
f, g: B -> A
forall (i j : Graph.graph0 parallel_pair_graph)
(g0 : Graph.graph1 parallel_pair_graph i j),
(fun i0 : Graph.graph0 parallel_pair_graph =>
 if i0 as b return (Diagram.obj (parallel_pair f g) b -> Coeq f g)
 then coeq o g
 else coeq) j
o Diagram.arr (parallel_pair f g) g0 ==
(fun i0 : Graph.graph0 parallel_pair_graph =>
 if i0 as b return (Diagram.obj (parallel_pair f g) b -> Coeq f g)
 then coeq o g
 else coeq) i intros i j phi x; destruct i, j, phi; simpl;
      [ exact (cglue x) | reflexivity ].
  Defined.

  Lemma iscoequalizer_Coeq `{Funext}
    : IsColimit (parallel_pair f g) (Coeq f g).
A, B: Type
f, g: B -> A
H: Funext
IsColimit (parallel_pair f g) (Coeq f g)
  Proof.
A, B: Type
f, g: B -> A
H: Funext
IsColimit (parallel_pair f g) (Coeq f g)
    srapply (Build_IsColimit cocone_Coeq).
A, B: Type
f, g: B -> A
H: Funext
UniversalCocone cocone_Coeq
    srapply Build_UniversalCocone.
A, B: Type
f, g: B -> A
H: Funext
forall Y : Type, IsEquiv (cocone_postcompose cocone_Coeq)
    intros X.
A, B: Type
f, g: B -> A
H: Funext
X: Type
IsEquiv (cocone_postcompose cocone_Coeq)
    srapply isequiv_adjointify.
A, B: Type
f, g: B -> A
H: Funext
X: Type
Cocone (parallel_pair f g) X -> Coeq f g -> X
A, B: Type
f, g: B -> A
H: Funext
X: Type
cocone_postcompose cocone_Coeq o ?g == idmap
A, B: Type
f, g: B -> A
H: Funext
X: Type
?g o cocone_postcompose cocone_Coeq == idmap
    -
A, B: Type
f, g: B -> A
H: Funext
X: Type
Cocone (parallel_pair f g) X -> Coeq f g -> X intros C.
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
Coeq f g -> X
      srapply Coeq_rec.
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
A -> X
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
forall b : B, ?coeq' (f b) = ?coeq' (g b)
      +
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
A -> X exact (legs C false).
      +
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
forall b : B, C false (f b) = C false (g b) intros b.
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
b: B
C false (f b) = C false (g b)
        etransitivity.
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
b: B
C false (f b) = ?Goal
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
b: B
?Goal = C false (g b)
        *
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
b: B
C false (f b) = ?Goal exact (legs_comm C true false true b).
        *
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
b: B
C true b = C false (g b) exact (legs_comm C true false false b)^.
    -
A, B: Type
f, g: B -> A
H: Funext
X: Type
cocone_postcompose cocone_Coeq
o (fun C : Cocone (parallel_pair f g) X =>
   Coeq_rec X (C false)
     (fun b : B =>
      legs_comm C true false true b @ (legs_comm C true false false b)^)) ==
idmap intros C.
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
cocone_postcompose cocone_Coeq
  (Coeq_rec X (C false)
     (fun b : B =>
      legs_comm C true false true b @ (legs_comm C true false false b)^)) =
C
      srapply path_cocone.
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
forall i : Graph.graph0 parallel_pair_graph,
cocone_postcompose cocone_Coeq
  (Coeq_rec X (C false)
     (fun b : B =>
      legs_comm C true false true b @ (legs_comm C true false false b)^))
  i ==
C i
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
forall (i j : Graph.graph0 parallel_pair_graph)
(g0 : Graph.graph1 parallel_pair_graph i j)
(x : Diagram.obj (parallel_pair f g) i),
legs_comm
  (cocone_postcompose cocone_Coeq
     (Coeq_rec X (C false)
        (fun b : B =>
         legs_comm C true false true b @ (legs_comm C true false false b)^)))
  i j g0 x @
?path_legs i x =
?path_legs j (Diagram.arr (parallel_pair f g) g0 x) @ legs_comm C i j g0 x
      +
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
forall i : Graph.graph0 parallel_pair_graph,
cocone_postcompose cocone_Coeq
  (Coeq_rec X (C false)
     (fun b : B =>
      legs_comm C true false true b @ (legs_comm C true false false b)^))
  i ==
C i intros i x; destruct i; simpl.
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
x: Diagram.obj (parallel_pair f g) true
C false (g x) = C true x
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
x: Diagram.obj (parallel_pair f g) false
C false x = C false x
        *
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
x: Diagram.obj (parallel_pair f g) true
C false (g x) = C true x exact (legs_comm C true false false x).
        *
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
x: Diagram.obj (parallel_pair f g) false
C false x = C false x reflexivity.
      +
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
forall (i j : Graph.graph0 parallel_pair_graph)
(g0 : Graph.graph1 parallel_pair_graph i j)
(x : Diagram.obj (parallel_pair f g) i),
legs_comm
  (cocone_postcompose cocone_Coeq
     (Coeq_rec X (C false)
        (fun b : B =>
         legs_comm C true false true b @ (legs_comm C true false false b)^)))
  i j g0 x @
(fun i0 : Graph.graph0 parallel_pair_graph =>
 (fun x0 : Diagram.obj (parallel_pair f g) i0 =>
  (if i0 as b
    return
      (forall x1 : Diagram.obj (parallel_pair f g) b,
       cocone_postcompose cocone_Coeq
         (Coeq_rec X (C false)
            (fun b0 : B =>
             legs_comm C true false true b0 @
             (legs_comm C true false false b0)^))
         b x1 =
       C b x1)
   then
    fun x1 : Diagram.obj (parallel_pair f g) true =>
    legs_comm C true false false x1
    :
    cocone_postcompose cocone_Coeq
      (Coeq_rec X (C false)
         (fun b : B =>
          legs_comm C true false true b @ (legs_comm C true false false b)^))
      true x1 =
    C true x1
   else
    fun x1 : Diagram.obj (parallel_pair f g) false =>
    1
    :
    cocone_postcompose cocone_Coeq
      (Coeq_rec X (C false)
         (fun b : B =>
          legs_comm C true false true b @ (legs_comm C true false false b)^))
      false x1 =
    C false x1) x0)
 :
 cocone_postcompose cocone_Coeq
   (Coeq_rec X (C false)
      (fun b : B =>
       legs_comm C true false true b @ (legs_comm C true false false b)^))
   i0 ==
 C i0) i x =
(fun i0 : Graph.graph0 parallel_pair_graph =>
 (fun x0 : Diagram.obj (parallel_pair f g) i0 =>
  (if i0 as b
    return
      (forall x1 : Diagram.obj (parallel_pair f g) b,
       cocone_postcompose cocone_Coeq
         (Coeq_rec X (C false)
            (fun b0 : B =>
             legs_comm C true false true b0 @
             (legs_comm C true false false b0)^))
         b x1 =
       C b x1)
   then
    fun x1 : Diagram.obj (parallel_pair f g) true =>
    legs_comm C true false false x1
    :
    cocone_postcompose cocone_Coeq
      (Coeq_rec X (C false)
         (fun b : B =>
          legs_comm C true false true b @ (legs_comm C true false false b)^))
      true x1 =
    C true x1
   else
    fun x1 : Diagram.obj (parallel_pair f g) false =>
    1
    :
    cocone_postcompose cocone_Coeq
      (Coeq_rec X (C false)
         (fun b : B =>
          legs_comm C true false true b @ (legs_comm C true false false b)^))
      false x1 =
    C false x1) x0)
 :
 cocone_postcompose cocone_Coeq
   (Coeq_rec X (C false)
      (fun b : B =>
       legs_comm C true false true b @ (legs_comm C true false false b)^))
   i0 ==
 C i0) j (Diagram.arr (parallel_pair f g) g0 x) @
legs_comm C i j g0 x intros i j phi x; destruct i, j, phi; simpl.
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
x: Diagram.obj (parallel_pair f g) true
ap
  (Coeq_rec X (C false)
     (fun b : B =>
      legs_comm C true false true b @ (legs_comm C true false false b)^))
  (cglue x) @
legs_comm C true false false x = 1 @ legs_comm C true false true x
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
x: Diagram.obj (parallel_pair f g) true
1 @ legs_comm C true false false x = 1 @ legs_comm C true false false x
        *
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
x: Diagram.obj (parallel_pair f g) true
ap
  (Coeq_rec X (C false)
     (fun b : B =>
      legs_comm C true false true b @ (legs_comm C true false false b)^))
  (cglue x) @
legs_comm C true false false x = 1 @ legs_comm C true false true x hott_simpl.
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
x: Diagram.obj (parallel_pair f g) true
ap
  (Coeq_rec X (C false)
     (fun b : B =>
      legs_comm C true false true b @ (legs_comm C true false false b)^))
  (cglue x) @
legs_comm C true false false x = legs_comm C true false true x
          match goal with
          | [|- ap (Coeq_rec ?a ?b ?c) _ @ _ = _ ]
            => rewrite (Coeq_rec_beta_cglue a b c)
          end.
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
x: Diagram.obj (parallel_pair f g) true
(legs_comm C true false true x @ (legs_comm C true false false x)^) @
legs_comm C true false false x = legs_comm C true false true x
          hott_simpl.
        *
A, B: Type
f, g: B -> A
H: Funext
X: Type
C: Cocone (parallel_pair f g) X
x: Diagram.obj (parallel_pair f g) true
1 @ legs_comm C true false false x = 1 @ legs_comm C true false false x reflexivity.
    -
A, B: Type
f, g: B -> A
H: Funext
X: Type
(fun C : Cocone (parallel_pair f g) X =>
 Coeq_rec X (C false)
   (fun b : B =>
    legs_comm C true false true b @ (legs_comm C true false false b)^))
o cocone_postcompose cocone_Coeq == idmap intros F.
A, B: Type
f, g: B -> A
H: Funext
X: Type
F: Coeq f g -> X
Coeq_rec X (cocone_postcompose cocone_Coeq F false)
  (fun b : B =>
   legs_comm (cocone_postcompose cocone_Coeq F) true false true b @
   (legs_comm (cocone_postcompose cocone_Coeq F) true false false b)^) =
F
      apply path_forall.
A, B: Type
f, g: B -> A
H: Funext
X: Type
F: Coeq f g -> X
Coeq_rec X (cocone_postcompose cocone_Coeq F false)
  (fun b : B =>
   legs_comm (cocone_postcompose cocone_Coeq F) true false true b @
   (legs_comm (cocone_postcompose cocone_Coeq F) true false false b)^) ==
F
      match goal with
        | [|- ?G == _ ] => simple refine (Coeq_ind (fun w => G w = F w) _ _)
      end.
A, B: Type
f, g: B -> A
H: Funext
X: Type
F: Coeq f g -> X
forall a : A,
(fun w : Coeq f g =>
 Coeq_rec X (cocone_postcompose cocone_Coeq F false)
   (fun b : B =>
    legs_comm (cocone_postcompose cocone_Coeq F) true false true b @
    (legs_comm (cocone_postcompose cocone_Coeq F) true false false b)^)
   w =
 F w) (coeq a)
A, B: Type
f, g: B -> A
H: Funext
X: Type
F: Coeq f g -> X
forall b : B,
transport
  (fun w : Coeq f g =>
   Coeq_rec X (cocone_postcompose cocone_Coeq F false)
     (fun b0 : B =>
      legs_comm (cocone_postcompose cocone_Coeq F) true false true b0 @
      (legs_comm (cocone_postcompose cocone_Coeq F) true false false b0)^)
     w =
   F w)
  (cglue b) (?coeq' (f b)) =
?coeq' (g b)
      +
A, B: Type
f, g: B -> A
H: Funext
X: Type
F: Coeq f g -> X
forall a : A,
(fun w : Coeq f g =>
 Coeq_rec X (cocone_postcompose cocone_Coeq F false)
   (fun b : B =>
    legs_comm (cocone_postcompose cocone_Coeq F) true false true b @
    (legs_comm (cocone_postcompose cocone_Coeq F) true false false b)^)
   w =
 F w) (coeq a) reflexivity.
      +
A, B: Type
f, g: B -> A
H: Funext
X: Type
F: Coeq f g -> X
forall b : B,
transport
  (fun w : Coeq f g =>
   Coeq_rec X (cocone_postcompose cocone_Coeq F false)
     (fun b0 : B =>
      legs_comm (cocone_postcompose cocone_Coeq F) true false true b0 @
      (legs_comm (cocone_postcompose cocone_Coeq F) true false false b0)^)
     w =
   F w)
  (cglue b) ((fun a : A => 1) (f b)) =
(fun a : A => 1) (g b) intros b.
A, B: Type
f, g: B -> A
H: Funext
X: Type
F: Coeq f g -> X
b: B
transport
  (fun w : Coeq f g =>
   Coeq_rec X (cocone_postcompose cocone_Coeq F false)
     (fun b0 : B =>
      legs_comm (cocone_postcompose cocone_Coeq F) true false true b0 @
      (legs_comm (cocone_postcompose cocone_Coeq F) true false false b0)^)
     w =
   F w)
  (cglue b) ((fun a : A => 1) (f b)) =
(fun a : A => 1) (g b)
        transport_paths FlFr; simpl.
A, B: Type
f, g: B -> A
H: Funext
X: Type
F: Coeq f g -> X
b: B
ap (Coeq_rec X (fun x : A => F (coeq x)) (fun b0 : B => ap F (cglue b0) @ 1))
  (cglue b) @
1 = 1 @ ap F (cglue b)
        apply equiv_p1_1q.
A, B: Type
f, g: B -> A
H: Funext
X: Type
F: Coeq f g -> X
b: B
ap (Coeq_rec X (fun x : A => F (coeq x)) (fun b0 : B => ap F (cglue b0) @ 1))
  (cglue b) =
ap F (cglue b)
        refine (Coeq_rec_beta_cglue _ _ _ _ @ _).
A, B: Type
f, g: B -> A
H: Funext
X: Type
F: Coeq f g -> X
b: B
ap F (cglue b) @ 1 = ap F (cglue b)
        apply concat_p1.
  Defined.

  Definition equiv_Coeq_Coequalizer `{Funext}
    : Coeq f g <~> Coequalizer f g.
A, B: Type
f, g: B -> A
H: Funext
Coeq f g <~> Coequalizer f g
  Proof.
A, B: Type
f, g: B -> A
H: Funext
Coeq f g <~> Coequalizer f g
    srapply colimit_unicity.
A, B: Type
f, g: B -> A
H: Funext
Graph.Graph
A, B: Type
f, g: B -> A
H: Funext
Diagram.Diagram ?G
A, B: Type
f, g: B -> A
H: Funext
IsColimit ?D (Coeq f g)
A, B: Type
f, g: B -> A
H: Funext
IsColimit ?D (Coequalizer f g)
    3: eapply iscoequalizer_Coeq.
A, B: Type
f, g: B -> A
H: Funext
IsColimit (parallel_pair f g) (Coequalizer f g)
    eapply iscolimit_colimit.
  Defined.

End Coequalizer.