Library HoTT.Algebra.Universal.Homomorphism

Local Unset Elimination Schemes.

Require Export
  HoTT.Algebra.Universal.Algebra
  HoTT.WildCat.Core.

Require Import
  HoTT.Types.

Local Open Scope Algebra_scope.

Section is_homomorphism.
  Context {σ} {A B : Algebra σ} (f : ∀ (s : Sort σ), A s → B s).

  Definition OpPreserving {w : SymbolType σ}
    (α : Operation A w) (β : Operation B w) : Type
    := ∀ 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 α β).
  Proof.
    apply istrunc_forall.
  Qed.

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

  Global Instance hprop_is_homomorphism `{Funext}
    : IsHProp IsHomomorphism.
  Proof.
    apply istrunc_forall.
  Qed.
End is_homomorphism.

Record Homomorphism {σ} {A B : Algebra σ} : Type := Build_Homomorphism
  { def_homomorphism : ∀ (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 → ∀ s, f s == g s.
Proof.
  intro p. by destruct p.
Defined.

Definition SigHomomorphism {σ} (A B : Algebra σ) : Type :=
  { def_hom : ∀ s, A s → B s | IsHomomorphism def_hom }.

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

Global Instance hset_homomorphism `{Funext} {σ} (A B : Algebra σ)
  : IsHSet (A $-> B).
Proof.
  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.
Proof.
  apply (ap (issig_homomorphism A B)^-1)^-1.
  unfold issig_homomorphism; cbn.
  apply path_sigma_hprop.
  exact p.
Defined.

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

  Global Instance is_homomorphism_id
    : IsHomomorphism (fun s (x : A s) ⇒ x).
  Proof.
    intros u a. 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}.

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

  Global Instance is_homomorphism_compose
    (g : ∀ s, B s → C s) `{!IsHomomorphism g}
    (f : ∀ s, A s → B s) `{!IsHomomorphism f}
    : IsHomomorphism (fun s ⇒ g s o f s).
  Proof.
    intros u a.
    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).
Proof.
  by apply path_homomorphism.
Defined.

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

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

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

Global Instance is01cat_homomorphism {σ} (A B : Algebra σ)
  : Is01Cat (A $-> B).
Proof.
  apply Build_Is01Cat.
  - exact (fun f s x ⇒ idpath).
  - 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).
Proof.
  apply Build_Is0Gpd. intros f g P 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).
Proof.
  apply Build_Is0Functor.
  intros [f ?] [g ?] p 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).
Proof.
  apply Build_Is0Functor.
  intros [f ?] [g ?] p s x.
  exact (p s (h s x)).
Defined.

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

Global Instance is1cat_strong_algebra `{Funext} (σ : Signature)
  : Is1Cat_Strong (Algebra σ).
Proof.
  rapply Build_Is1Cat_Strong.
  - intros. apply assoc_homomorphism_compose.
  - intros. symmetry; apply assoc_homomorphism_compose.
  - intros. apply left_id_homomorphism_compose.
  - intros. apply right_id_homomorphism_compose.
Defined.