ua_category.v

Require Import
  HoTT.Types
  HoTT.Categories.Category.Core
  HoTT.Categories.Category.Univalent
  HoTT.Classes.theory.ua_isomorphic.



Import Morphisms.CategoryMorphismsNotations isomorphic_notations.


Local Open Scope category.


(** Given any signature [σ], there is a precategory of set algebras
    and homomorphisms for that signature. *)

Lemma precategory_algebra `{Funext} (σ : Signature) : PreCategory.

Proof.

  apply (@Build_PreCategory
           (SetAlgebra σ) Homomorphism hom_id (@hom_compose σ));
    [intros; by apply path_hset_homomorphism .. | exact _].

Defined.


(** Category isomorphic implies algebra isomorphic. *)

Lemma catiso_to_uaiso `{Funext} {σ} {A B : object (precategory_algebra σ)}
  : A <~=~> B → A ≅ B.

Proof.

  intros [f [a b c]].

  unshelve eapply (@BuildIsomorphic _ _ _ f).

  intros s.

  refine (isequiv_adjointify (f s) (a s) _ _).

 exact (apD10_homomorphism c s).

 exact (apD10_homomorphism b s).

Defined.


(** Algebra isomorphic implies category isomorphic. *)

Lemma uaiso_to_catiso `{Funext} {σ} {A B : object (precategory_algebra σ)}
  : A ≅ B → A <~=~> B.

Proof.

  intros [f F G].

 set (h := BuildHomomorphism f).

  apply (@Morphisms.Build_Isomorphic _ A B h).

  apply (@Morphisms.Build_IsIsomorphism _ A B h (hom_inv h)).

 apply path_hset_homomorphism.

 funext s x.

 apply eissect.

 apply path_hset_homomorphism.

 funext s x.

 apply eisretr.

Defined.


(** Category isomorphic and algebra isomorphic is equivalent. *)

Instance isequiv_catiso_to_uaiso `{Funext} {σ : Signature}
  (A B : object (precategory_algebra σ))
  : IsEquiv (@catiso_to_uaiso _ σ A B).

Proof.

  refine (isequiv_adjointify catiso_to_uaiso uaiso_to_catiso _ _).

 intros [f F G].

 by apply path_hset_isomorphic.

 intros [f F].

 by apply Morphisms.path_isomorphic.

Defined.


(** [Morphisms.idtoiso] factorizes as the composition of equivalences. *)

Lemma path_idtoiso_isomorphic_id `{Funext} {σ : Signature}
  (A B : object (precategory_algebra σ))
  : @Morphisms.idtoiso (precategory_algebra σ) A B
    = catiso_to_uaiso^-1 o isomorphic_id o (path_setalgebra A B)^-1.

Proof.

  funext p.

 destruct p.

 by apply Morphisms.path_isomorphic.

Defined.


(** The precategory of set algebras and homomorphisms for a signature
    is a (univalent) category. *)

Lemma iscategory_algebra `{Univalence} (σ : Signature)
  : IsCategory (precategory_algebra σ).

Proof.

  intros A B.

  rewrite path_idtoiso_isomorphic_id.

  apply @isequiv_compose.

 rapply isequiv_compose.

 apply isequiv_inverse.

Qed.


Definition category_algebra `{Univalence} (σ : Signature) : Category
  := Build_Category (iscategory_algebra σ).

Timings for ua_category.v