Require Import Basics Types.Sigma Types.Paths.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

(** Equalizers *)

Definition Equalizer {A B} (f g : A -> B)
  := {x : A & f x = g x}.

Definition functor_equalizer {A B A' B'} (f g : A -> B)
           (f' g' : A' -> B')
           (h : B -> B') (k : A -> A')
           (p : h o f == f' o k) (q : h o g == g' o k)
  : Equalizer f g -> Equalizer f' g'.
A, B, A', B': Type
f, g: A -> B
f', g': A' -> B'
h: B -> B'
k: A -> A'
p: h o f == f' o k
q: h o g == g' o k
Equalizer f g -> Equalizer f' g'
Proof.
A, B, A', B': Type
f, g: A -> B
f', g': A' -> B'
h: B -> B'
k: A -> A'
p: h o f == f' o k
q: h o g == g' o k
Equalizer f g -> Equalizer f' g'
  intros [x r].
A, B, A', B': Type
f, g: A -> B
f', g': A' -> B'
h: B -> B'
k: A -> A'
p: h o f == f' o k
q: h o g == g' o k
x: A
r: f x = g x
Equalizer f' g'
  exists (k x).
A, B, A', B': Type
f, g: A -> B
f', g': A' -> B'
h: B -> B'
k: A -> A'
p: h o f == f' o k
q: h o g == g' o k
x: A
r: f x = g x
f' (k x) = g' (k x)
  exact ((p x)^ @ (ap h r) @ (q x)).
Defined.

Definition equiv_functor_equalizer {A B A' B'} (f g : A -> B)
           (f' g' : A' -> B')
           (h : B <~> B') (k : A <~> A')
           (p : h o f == f' o k) (q : h o g == g' o k)
  : Equalizer f g <~> Equalizer f' g'.
A, B, A', B': Type
f, g: A -> B
f', g': A' -> B'
h: B <~> B'
k: A <~> A'
p: h o f == f' o k
q: h o g == g' o k
Equalizer f g <~> Equalizer f' g'
Proof.
A, B, A', B': Type
f, g: A -> B
f', g': A' -> B'
h: B <~> B'
k: A <~> A'
p: h o f == f' o k
q: h o g == g' o k
Equalizer f g <~> Equalizer f' g'
  unfold Equalizer.
A, B, A', B': Type
f, g: A -> B
f', g': A' -> B'
h: B <~> B'
k: A <~> A'
p: h o f == f' o k
q: h o g == g' o k
{x : A & f x = g x} <~> {x : A' & f' x = g' x}
  srapply (equiv_functor_sigma' k).
A, B, A', B': Type
f, g: A -> B
f', g': A' -> B'
h: B <~> B'
k: A <~> A'
p: h o f == f' o k
q: h o g == g' o k
forall a : A,
(fun x : A => f x = g x) a <~>
(fun x : A' => f' x = g' x) (k a)
  -
A, B, A', B': Type
f, g: A -> B
f', g': A' -> B'
h: B <~> B'
k: A <~> A'
p: h o f == f' o k
q: h o g == g' o k
forall a : A,
(fun x : A => f x = g x) a <~>
(fun x : A' => f' x = g' x) (k a) intro a; cbn.
A, B, A', B': Type
f, g: A -> B
f', g': A' -> B'
h: B <~> B'
k: A <~> A'
p: h o f == f' o k
q: h o g == g' o k
a: A
f a = g a <~> f' (k a) = g' (k a)
    refine (_ oE _).
A, B, A', B': Type
f, g: A -> B
f', g': A' -> B'
h: B <~> B'
k: A <~> A'
p: h o f == f' o k
q: h o g == g' o k
a: A
?Goal <~> f' (k a) = g' (k a)
A, B, A', B': Type
f, g: A -> B
f', g': A' -> B'
h: B <~> B'
k: A <~> A'
p: h o f == f' o k
q: h o g == g' o k
a: A
f a = g a <~> ?Goal
    2: rapply (equiv_ap h).
A, B, A', B': Type
f, g: A -> B
f', g': A' -> B'
h: B <~> B'
k: A <~> A'
p: h o f == f' o k
q: h o g == g' o k
a: A
h (f a) = h (g a) <~> f' (k a) = g' (k a)
    exact (equiv_concat_r (q a) _ oE equiv_concat_l (p a)^ _).
Defined.