(** This file implements algebra homomorphism. We show that algebras form a wild category with homomorphisms. The [WildCat] module provides some nice notations that we we use: [A $-> B] for homomorphism, [Id] for the identity homomorphism and [g $o f] for composition. *)

Local Unset Elimination Schemes.

Require Export
  HoTT.Algebra.Universal.Algebra
  HoTT.WildCat.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Require Import
  HoTT.Types.

Local Open Scope Algebra_scope.

Section is_homomorphism.
  Context {σ} {A B : Algebra σ} (f : forall (s : Sort σ), A s -> B s).

  Definition OpPreserving {w : SymbolType σ}
    (α : Operation A w) (β : Operation B w) : Type
    := forall a : DomOperation A w,
        f (sort_cod w) (α a) = β (fun i => f (sorts_dom w i) (a i)).

  Global Instance hprop_oppreserving `{Funext} {w : SymbolType σ}
    (α : Operation A w) (β : Operation B w)
    : IsHProp (OpPreserving α β).
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
H: Funext
w: SymbolType σ
α: Operation A w
β: Operation B w
IsHProp (OpPreserving α β)
  Proof.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
H: Funext
w: SymbolType σ
α: Operation A w
β: Operation B w
IsHProp (OpPreserving α β)
    apply istrunc_forall.
  Qed.

  Class IsHomomorphism : Type
    := oppreserving_hom : forall (u : Symbol σ), OpPreserving u.#A u.#B.

  Global Instance hprop_is_homomorphism `{Funext}
    : IsHProp IsHomomorphism.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
H: Funext
IsHProp IsHomomorphism
  Proof.
σ: Signature
A, B: Algebra σ
f: forall s : Sort σ, A s -> B s
H: Funext
IsHProp IsHomomorphism
    apply istrunc_forall.
  Qed.
End is_homomorphism.

Record Homomorphism {σ} {A B : Algebra σ} : Type := Build_Homomorphism
  { def_homomorphism : forall (s : Sort σ), A s -> B s
  ; is_homomorphism : IsHomomorphism def_homomorphism }.

Arguments Homomorphism {σ}.

Arguments Build_Homomorphism {σ A B} def_homomorphism {is_homomorphism}.

Global Coercion def_homomorphism : Homomorphism >-> Funclass.

Global Existing Instance is_homomorphism.

Global Instance isgraph_algebra (σ : Signature) : IsGraph (Algebra σ)
  := Build_IsGraph (Algebra σ) Homomorphism.

Lemma apD10_homomorphism {σ} {A B : Algebra σ} {f g : A $-> B}
  : f = g -> forall s, f s == g s.
σ: Signature
A, B: Algebra σ
f, g: A $-> B
f = g -> forall s : Sort σ, f s == g s
Proof.
σ: Signature
A, B: Algebra σ
f, g: A $-> B
f = g -> forall s : Sort σ, f s == g s
  intro p.
σ: Signature
A, B: Algebra σ
f, g: A $-> B
p: f = g
forall s : Sort σ, f s == g s by destruct p.
Defined.

Definition SigHomomorphism {σ} (A B : Algebra σ) : Type :=
  { def_hom : forall s, A s -> B s | IsHomomorphism def_hom }.

Lemma issig_homomorphism {σ} (A B : Algebra σ)
  : SigHomomorphism A B <~> (A $-> B).
σ: Signature
A, B: Algebra σ
SigHomomorphism A B <~> (A $-> B)
Proof.
σ: Signature
A, B: Algebra σ
SigHomomorphism A B <~> (A $-> B)
  issig.
Defined.

Global Instance hset_homomorphism `{Funext} {σ} (A B : Algebra σ)
  : IsHSet (A $-> B).
H: Funext
σ: Signature
A, B: Algebra σ
IsHSet (A $-> B)
Proof.
H: Funext
σ: Signature
A, B: Algebra σ
IsHSet (A $-> B)
  apply (istrunc_equiv_istrunc _ (issig_homomorphism A B)).
Qed.

Lemma path_homomorphism `{Funext} {σ} {A B : Algebra σ}
  (f g : A $-> B) (p : def_homomorphism f = def_homomorphism g)
  : f = g.
H: Funext
σ: Signature
A, B: Algebra σ
f, g: A $-> B
p: f = g
f = g
Proof.
H: Funext
σ: Signature
A, B: Algebra σ
f, g: A $-> B
p: f = g
f = g
  apply (ap (issig_homomorphism A B)^-1)^-1.
H: Funext
σ: Signature
A, B: Algebra σ
f, g: A $-> B
p: f = g
(issig_homomorphism A B)^-1 f =
(issig_homomorphism A B)^-1 g
  unfold issig_homomorphism; cbn.
H: Funext
σ: Signature
A, B: Algebra σ
f, g: A $-> B
p: f = g
(f; is_homomorphism f) = (g; is_homomorphism g)
  apply path_sigma_hprop.
H: Funext
σ: Signature
A, B: Algebra σ
f, g: A $-> B
p: f = g
(f; is_homomorphism f).1 = (g; is_homomorphism g).1
  exact p.
Defined.

(** The identity homomorphism. *)

Section homomorphism_id.
  Context {σ} (A : Algebra σ).

  Global Instance is_homomorphism_id
    : IsHomomorphism (fun s (x : A s) => x).
σ: Signature
A: Algebra σ
IsHomomorphism (fun s : Sort σ => idmap)
  Proof.
σ: Signature
A: Algebra σ
IsHomomorphism (fun s : Sort σ => idmap)
    intros u a.
σ: Signature
A: Algebra σ
u: Symbol σ
a: forall i : Arity (σ u), A (sorts_dom (σ u) i)
u.#A a = u.#A (fun i : Arity (σ u) => a i) reflexivity.
  Defined.

  Definition homomorphism_id : A $-> A
    := Build_Homomorphism (fun s (x : A s) => x).

End homomorphism_id.

Arguments homomorphism_id {σ} A%Algebra_scope , {σ} {A}.

(** Composition of homomorphisms. *)

Section homomorphism_compose.
  Context {σ} {A B C : Algebra σ}.

  Global Instance is_homomorphism_compose
    (g : forall s, B s -> C s) `{!IsHomomorphism g}
    (f : forall s, A s -> B s) `{!IsHomomorphism f}
    : IsHomomorphism (fun s => g s o f s).
σ: Signature
A, B, C: Algebra σ
g: forall s : Sort σ, B s -> C s
IsHomomorphism0: IsHomomorphism g
f: forall s : Sort σ, A s -> B s
IsHomomorphism1: IsHomomorphism f
IsHomomorphism (fun s : Sort σ => g s o f s)
  Proof.
σ: Signature
A, B, C: Algebra σ
g: forall s : Sort σ, B s -> C s
IsHomomorphism0: IsHomomorphism g
f: forall s : Sort σ, A s -> B s
IsHomomorphism1: IsHomomorphism f
IsHomomorphism (fun s : Sort σ => g s o f s)
    intros u a.
σ: Signature
A, B, C: Algebra σ
g: forall s : Sort σ, B s -> C s
IsHomomorphism0: IsHomomorphism g
f: forall s : Sort σ, A s -> B s
IsHomomorphism1: IsHomomorphism f
u: Symbol σ
a: forall i : Arity (σ u), A (sorts_dom (σ u) i)
g (sort_cod (σ u)) (f (sort_cod (σ u)) (u.#A a)) =
u.#C
  (fun i : Arity (σ u) =>
   g (sorts_dom (σ u) i) (f (sorts_dom (σ u) i) (a i)))
    by rewrite <- (oppreserving_hom g), (oppreserving_hom f).
  Qed.

  Definition homomorphism_compose (g : B $-> C) (f : A $-> B) : A $-> C
    := Build_Homomorphism (fun s => g s o f s).

End homomorphism_compose.

Global Instance is01cat_algebra (σ : Signature) : Is01Cat (Algebra σ)
  := Build_Is01Cat (Algebra σ) _
      (fun _ => homomorphism_id) (fun _ _ _ => homomorphism_compose).

Lemma assoc_homomorphism_compose `{Funext} {σ}
  {A B C D : Algebra σ} (h : C $-> D) (g : B $-> C) (f : A $-> B)
  : (h $o g) $o f = h $o (g $o f).
H: Funext
σ: Signature
A, B, C, D: Algebra σ
h: C $-> D
g: B $-> C
f: A $-> B
h $o g $o f = h $o (g $o f)
Proof.
H: Funext
σ: Signature
A, B, C, D: Algebra σ
h: C $-> D
g: B $-> C
f: A $-> B
h $o g $o f = h $o (g $o f)
  by apply path_homomorphism.
Defined.

Lemma left_id_homomorphism_compose `{Funext} {σ}
  {A B : Algebra σ} (f : A $-> B)
  : Id B $o f = f.
H: Funext
σ: Signature
A, B: Algebra σ
f: A $-> B
Id B $o f = f
Proof.
H: Funext
σ: Signature
A, B: Algebra σ
f: A $-> B
Id B $o f = f
  by apply path_homomorphism.
Defined.

Lemma right_id_homomorphism_compose `{Funext} {σ}
  {A B : Algebra σ} (f : A $-> B)
  : f $o Id A = f.
H: Funext
σ: Signature
A, B: Algebra σ
f: A $-> B
f $o Id A = f
Proof.
H: Funext
σ: Signature
A, B: Algebra σ
f: A $-> B
f $o Id A = f
  by apply path_homomorphism.
Defined.

Global Instance is2graph_algebra {σ} : Is2Graph (Algebra σ)
  := fun A B
    => Build_IsGraph _ (fun (f g : A $-> B) => forall s, f s == g s).

Global Instance is01cat_homomorphism {σ} (A B : Algebra σ)
  : Is01Cat (A $-> B).
σ: Signature
A, B: Algebra σ
Is01Cat (A $-> B)
Proof.
σ: Signature
A, B: Algebra σ
Is01Cat (A $-> B)
  apply Build_Is01Cat.
σ: Signature
A, B: Algebra σ
forall a : A $-> B, a $-> a
σ: Signature
A, B: Algebra σ
forall a b c : A $-> B,
(b $-> c) -> (a $-> b) -> a $-> c
  -
σ: Signature
A, B: Algebra σ
forall a : A $-> B, a $-> a exact (fun f s x => idpath).
  -
σ: Signature
A, B: Algebra σ
forall a b c : A $-> B,
(b $-> c) -> (a $-> b) -> a $-> c exact (fun f g h P Q s x => Q s x @ P s x).
Defined.

Global Instance is0gpd_homomorphism {σ} {A B : Algebra σ}
  : Is0Gpd (A $-> B).
σ: Signature
A, B: Algebra σ
Is0Gpd (A $-> B)
Proof.
σ: Signature
A, B: Algebra σ
Is0Gpd (A $-> B)
  apply Build_Is0Gpd.
σ: Signature
A, B: Algebra σ
forall a b : A $-> B, (a $-> b) -> b $-> a intros f g P s x.
σ: Signature
A, B: Algebra σ
f, g: A $-> B
P: f $-> g
s: Sort σ
x: A s
g s x = f s x exact (P s x)^.
Defined.

Global Instance is0functor_postcomp_homomorphism {σ}
  (A : Algebra σ) {B C : Algebra σ} (h : B $-> C)
  : Is0Functor (@cat_postcomp (Algebra σ) _ _ A B C h).
σ: Signature
A, B, C: Algebra σ
h: B $-> C
Is0Functor (cat_postcomp A h)
Proof.
σ: Signature
A, B, C: Algebra σ
h: B $-> C
Is0Functor (cat_postcomp A h)
  apply Build_Is0Functor.
σ: Signature
A, B, C: Algebra σ
h: B $-> C
forall a b : A $-> B,
(a $-> b) -> cat_postcomp A h a $-> cat_postcomp A h b
  intros [f ?] [g ?] p s x.
σ: Signature
A, B, C: Algebra σ
h: B $-> C
f: forall s : Sort σ, A s -> B s
is_homomorphism0: IsHomomorphism f
g: forall s : Sort σ, A s -> B s
is_homomorphism1: IsHomomorphism g
p: {|
  def_homomorphism := f;
  is_homomorphism := is_homomorphism0
|} $->
{|
  def_homomorphism := g;
  is_homomorphism := is_homomorphism1
|}
s: Sort σ
x: A s
cat_postcomp A h
  {|
    def_homomorphism := f;
    is_homomorphism := is_homomorphism0
  |} s x =
cat_postcomp A h
  {|
    def_homomorphism := g;
    is_homomorphism := is_homomorphism1
  |} s x
  exact (ap (h s) (p s x)).
Defined.

Global Instance is0functor_precomp_homomorphism {σ}
  {A B : Algebra σ} (h : A $-> B) (C : Algebra σ)
  : Is0Functor (@cat_precomp (Algebra σ) _ _ A B C h).
σ: Signature
A, B: Algebra σ
h: A $-> B
C: Algebra σ
Is0Functor (cat_precomp C h)
Proof.
σ: Signature
A, B: Algebra σ
h: A $-> B
C: Algebra σ
Is0Functor (cat_precomp C h)
  apply Build_Is0Functor.
σ: Signature
A, B: Algebra σ
h: A $-> B
C: Algebra σ
forall a b : B $-> C,
(a $-> b) -> cat_precomp C h a $-> cat_precomp C h b
  intros [f ?] [g ?] p s x.
σ: Signature
A, B: Algebra σ
h: A $-> B
C: Algebra σ
f: forall s : Sort σ, B s -> C s
is_homomorphism0: IsHomomorphism f
g: forall s : Sort σ, B s -> C s
is_homomorphism1: IsHomomorphism g
p: {|
  def_homomorphism := f;
  is_homomorphism := is_homomorphism0
|} $->
{|
  def_homomorphism := g;
  is_homomorphism := is_homomorphism1
|}
s: Sort σ
x: A s
cat_precomp C h
  {|
    def_homomorphism := f;
    is_homomorphism := is_homomorphism0
  |} s x =
cat_precomp C h
  {|
    def_homomorphism := g;
    is_homomorphism := is_homomorphism1
  |} s x
  exact (p s (h s x)).
Defined.

Global Instance is1cat_algebra (σ : Signature) : Is1Cat (Algebra σ).
σ: Signature
Is1Cat (Algebra σ)
Proof.
σ: Signature
Is1Cat (Algebra σ)
  by rapply Build_Is1Cat.
Defined.

Global Instance is1cat_strong_algebra `{Funext} (σ : Signature)
  : Is1Cat_Strong (Algebra σ).
H: Funext
σ: Signature
Is1Cat_Strong (Algebra σ)
Proof.
H: Funext
σ: Signature
Is1Cat_Strong (Algebra σ)
  rapply Build_Is1Cat_Strong.
H: Funext
σ: Signature
forall (a b c d : Algebra σ) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o g $o f = h $o (g $o f)
H: Funext
σ: Signature
forall (a b c d : Algebra σ) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o (g $o f) = h $o g $o f
H: Funext
σ: Signature
forall (a b : Algebra σ) (f : a $-> b), Id b $o f = f
H: Funext
σ: Signature
forall (a b : Algebra σ) (f : a $-> b), f $o Id a = f
  -
H: Funext
σ: Signature
forall (a b c d : Algebra σ) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o g $o f = h $o (g $o f) intros.
H: Funext
σ: Signature
a, b, c, d: Algebra σ
f: a $-> b
g: b $-> c
h: c $-> d
h $o g $o f = h $o (g $o f) apply assoc_homomorphism_compose.
  -
H: Funext
σ: Signature
forall (a b c d : Algebra σ) (f : a $-> b)
(g : b $-> c) (h : c $-> d),
h $o (g $o f) = h $o g $o f intros.
H: Funext
σ: Signature
a, b, c, d: Algebra σ
f: a $-> b
g: b $-> c
h: c $-> d
h $o (g $o f) = h $o g $o f symmetry; apply assoc_homomorphism_compose.
  -
H: Funext
σ: Signature
forall (a b : Algebra σ) (f : a $-> b), Id b $o f = f intros.
H: Funext
σ: Signature
a, b: Algebra σ
f: a $-> b
Id b $o f = f apply left_id_homomorphism_compose.
  -
H: Funext
σ: Signature
forall (a b : Algebra σ) (f : a $-> b), f $o Id a = f intros.
H: Funext
σ: Signature
a, b: Algebra σ
f: a $-> b
f $o Id a = f apply right_id_homomorphism_compose.
Defined.