Library UniMath.CategoryTheory.categories.Universal_Algebra.Algebras

The univalent category of algebras over a signature.

Gianluca Amato, Marco Maggesi, Cosimo Perini Brogi 2019-2021
We use display categories to define the category of algebras and prove its univalence.

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.Univalence.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.categories.HSET.Univalence.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Total.
Require Import UniMath.CategoryTheory.DisplayedCats.SIP.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.limits.initial.

Require Import UniMath.Algebra.Universal.TermAlgebras.

Section Algebras.

  Local Open Scope sorted_scope.

  Context (σ : signature).

  Definition shSet_precategory_ob_mor : precategory_ob_mor.
  Show proof.
    use make_precategory_ob_mor.
    - exact (shSet (sorts σ)).
    - intros F G. exact (F s→ G).

  Definition shSet_precategory_data : precategory_data.
  Show proof.
    use make_precategory_data.
    - exact shSet_precategory_ob_mor.
    - intro C. simpl. apply idsfun.
    - simpl. intros F G H. intros f g. exact (g s∘ f).

  Definition is_precategory_shSet_precategory_data : is_precategory shSet_precategory_data.
  Show proof.
    repeat split.

  Definition shSet_precategory : precategory.
  Show proof.
    use make_precategory.
    - apply shSet_precategory_data.
    - apply is_precategory_shSet_precategory_data.

  Definition has_homsets_shSet_precategory : has_homsets shSet_precategory.
  Show proof.
    intros F G. simpl.
    use isaset_set_sfun_space.

  Definition shSet_category : category := (shSet_precategory ,, has_homsets_shSet_precategory).

  Definition algebras_disp : disp_cat shSet_category.
  Show proof.
    use disp_cat_from_SIP_data. simpl.
    - intro A. exact (∏ nm: names σ, A⋆ (arity nm) → A (sort nm)).
    - simpl. intros A B asA asB f. exact (@ishom σ (make_algebra A asA) (make_algebra B asB) f).
    - simpl. intros A B asA asB f opA opB.
      apply isapropishom.
    - cbn. intros A asA. apply ishomid.
    - cbn. intros A B C opA opB opC. intros f g ishomf ishomg.
      exact (ishomcomp (make_hom ishomf) (make_hom ishomg)).

  Lemma is_univalent_algebras_disp : is_univalent_disp algebras_disp.
  Show proof.
    use is_univalent_disp_from_SIP_data.
    - intro A. cbn. use impred_isaset. intro nm. cbn.
      use isaset_set_fun_space.
    - cbn. intros A op1 op2 ishomid1 _. use funextsec. intro nm. use funextfun. intro vec.
      unfold ishom in *. cbn in *. set (H1:= ishomid1 nm vec).
      rewrite staridfun in H1. apply H1.

  Local Open Scope cat.

Here follows the proof that shSet_category is univalent. The proof is obtained by following the example of the proof of univalence of the functor category.

  Lemma shSet_iso_fiber {A B : shSet_category} (i : z_iso A B): ∏ s, @z_iso HSET (A s) (B s).
  Show proof.
    intro s.
    induction i as [i [i' [p q]]].
    simpl in *.
    use make_z_iso.
    - exact (i s).
    - exact (i' s).
    - split.
      + exact (eqtohomot p s).
      + exact (eqtohomot q s).

  Definition shSet_eq_from_shSet_z_iso (F G : shSet_category) (i : z_iso F G) : F = G.
  Show proof.
    apply funextsec.
    intro s.
    apply (isotoid HSET is_univalent_HSET).
    apply shSet_iso_fiber.
    assumption.

  Lemma idtoiso_shSet_category_compute_pointwise {F G : shSet_category} (p : F = G) (s: sorts σ)
    : shSet_iso_fiber (idtoiso p) s = idtoiso(C:=HSET) (toforallpaths (λ _ , hSet) F G p s).
  Show proof.
    induction p.
    apply z_iso_eq. apply idpath.

  Lemma shSet_eq_from_shSet_z_iso_idtoiso (F G : shSet_category) (p : F = G)
    : shSet_eq_from_shSet_z_iso F G (idtoiso p) = p.
  Show proof.
    unfold shSet_eq_from_shSet_z_iso.
    apply (invmaponpathsweq (weqtoforallpaths _ _ _ )).
    simpl (pr1weq (weqtoforallpaths (λ _ : sorts σ, hSet) F G)).
    rewrite (toforallpaths_funextsec).
    apply funextsec.
    intro a.
    rewrite idtoiso_shSet_category_compute_pointwise.
    rewrite isotoid_idtoiso.
    apply idpath.

  Lemma idtoiso_shSet_eq_from_shSet_z_iso (F G : shSet_category) (i : z_iso F G)
    : idtoiso (shSet_eq_from_shSet_z_iso F G i) = i.
  Show proof.
    apply z_iso_eq.
    apply funextsec.
    intro s.
    unfold shSet_eq_from_shSet_z_iso.
    assert (H' := idtoiso_shSet_category_compute_pointwise (shSet_eq_from_shSet_z_iso F G i) s).
    simpl in *.
    assert (H2 := maponpaths (@pr1 _ _ ) H').
    simpl in H2.
    etrans.
    { apply H2. }
    intermediate_path (pr1 (idtoiso (isotoid HSET is_univalent_HSET (shSet_iso_fiber i s)))).
    - apply maponpaths.
      apply maponpaths.
      unfold shSet_eq_from_shSet_z_iso.
      rewrite toforallpaths_funextsec.
      apply idpath.
    - rewrite idtoiso_isotoid.
      apply idpath.

  Definition is_univalent_shSet_category : is_univalent shSet_category.
  Show proof.
    intros F G.
    apply (isweq_iso _ (shSet_eq_from_shSet_z_iso F G)).
    - apply shSet_eq_from_shSet_z_iso_idtoiso.
    - apply idtoiso_shSet_eq_from_shSet_z_iso.

  Definition category_algebras : category := total_category algebras_disp.

  Lemma is_univalent_category_algebras : is_univalent category_algebras.
  Show proof.
    exact (@is_univalent_total_category shSet_category algebras_disp is_univalent_shSet_category is_univalent_algebras_disp).

  Lemma isinitial_termalgebra : Initial (category_algebras).
  Show proof.
    exact (term_algebra σ ,, iscontrhomsfromgterm).

End Algebras.