Require ImportRequire 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.
H: Funext
σ: Signature
PreCategory
Proof.
H: Funext
σ: Signature
PreCategory
  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.
H: Funext
σ: Signature
A, B: precategory_algebra σ
A <~=~> B -> A ≅ B
Proof.
H: Funext
σ: Signature
A, B: precategory_algebra σ
A <~=~> B -> A ≅ B
  intros [f [a b c]].
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: morphism (precategory_algebra σ) A B
a: morphism (precategory_algebra σ) B A
b: (a o f)%morphism = 1%morphism
c: (f o a)%morphism = 1%morphism
A ≅ B
  unshelve eapply (@BuildIsomorphic _ _ _ f).
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: morphism (precategory_algebra σ) A B
a: morphism (precategory_algebra σ) B A
b: (a o f)%morphism = 1%morphism
c: (f o a)%morphism = 1%morphism
IsIsomorphism f
  intros s.
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: morphism (precategory_algebra σ) A B
a: morphism (precategory_algebra σ) B A
b: (a o f)%morphism = 1%morphism
c: (f o a)%morphism = 1%morphism
s: Sort σ
IsEquiv (f s)
  refine (isequiv_adjointify (f s) (a s) _ _).
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: morphism (precategory_algebra σ) A B
a: morphism (precategory_algebra σ) B A
b: (a o f)%morphism = 1%morphism
c: (f o a)%morphism = 1%morphism
s: Sort σ
(λ x : B s, f s (a s x)) == idmap
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: morphism (precategory_algebra σ) A B
a: morphism (precategory_algebra σ) B A
b: (a o f)%morphism = 1%morphism
c: (f o a)%morphism = 1%morphism
s: Sort σ
(λ x : A s, a s (f s x)) == idmap
  -
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: morphism (precategory_algebra σ) A B
a: morphism (precategory_algebra σ) B A
b: (a o f)%morphism = 1%morphism
c: (f o a)%morphism = 1%morphism
s: Sort σ
(λ x : B s, f s (a s x)) == idmap exact (apD10_homomorphism c s).
  -
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: morphism (precategory_algebra σ) A B
a: morphism (precategory_algebra σ) B A
b: (a o f)%morphism = 1%morphism
c: (f o a)%morphism = 1%morphism
s: Sort σ
(λ x : A s, a s (f s x)) == idmap 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.
H: Funext
σ: Signature
A, B: precategory_algebra σ
A ≅ B -> A <~=~> B
Proof.
H: Funext
σ: Signature
A, B: precategory_algebra σ
A ≅ B -> A <~=~> B
  intros [f F G].
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: forall s : Sort σ, A s -> B s
F: IsHomomorphism f
G: IsIsomorphism f
A <~=~> B set (h := BuildHomomorphism f).
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: forall s : Sort σ, A s -> B s
F: IsHomomorphism f
G: IsIsomorphism f
h:= {| def_hom := f; is_homomorphism_hom := F |}: Homomorphism A B
A <~=~> B
  apply (@Morphisms.Build_Isomorphic _ A B h).
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: forall s : Sort σ, A s -> B s
F: IsHomomorphism f
G: IsIsomorphism f
h:= {| def_hom := f; is_homomorphism_hom := F |}: Homomorphism A B
Morphisms.IsIsomorphism h
  apply (@Morphisms.Build_IsIsomorphism _ A B h (hom_inv h)).
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: forall s : Sort σ, A s -> B s
F: IsHomomorphism f
G: IsIsomorphism f
h:= {| def_hom := f; is_homomorphism_hom := F |}: Homomorphism A B
(hom_inv h o h)%morphism = 1%morphism
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: forall s : Sort σ, A s -> B s
F: IsHomomorphism f
G: IsIsomorphism f
h:= {| def_hom := f; is_homomorphism_hom := F |}: Homomorphism A B
(h o hom_inv h)%morphism = 1%morphism
  -
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: forall s : Sort σ, A s -> B s
F: IsHomomorphism f
G: IsIsomorphism f
h:= {| def_hom := f; is_homomorphism_hom := F |}: Homomorphism A B
(hom_inv h o h)%morphism = 1%morphism apply path_hset_homomorphism.
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: forall s : Sort σ, A s -> B s
F: IsHomomorphism f
G: IsIsomorphism f
h:= {| def_hom := f; is_homomorphism_hom := F |}: Homomorphism A B
(hom_inv h o h)%morphism = 1%morphism funext s x.
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: forall s0 : Sort σ, A s0 -> B s0
F: IsHomomorphism f
G: IsIsomorphism f
h:= {| def_hom := f; is_homomorphism_hom := F |}: Homomorphism A B
s: Sort σ
x: A s
(hom_inv h o h)%morphism s x = 1%morphism s x apply eissect.
  -
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: forall s : Sort σ, A s -> B s
F: IsHomomorphism f
G: IsIsomorphism f
h:= {| def_hom := f; is_homomorphism_hom := F |}: Homomorphism A B
(h o hom_inv h)%morphism = 1%morphism apply path_hset_homomorphism.
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: forall s : Sort σ, A s -> B s
F: IsHomomorphism f
G: IsIsomorphism f
h:= {| def_hom := f; is_homomorphism_hom := F |}: Homomorphism A B
(h o hom_inv h)%morphism = 1%morphism funext s x.
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: forall s0 : Sort σ, A s0 -> B s0
F: IsHomomorphism f
G: IsIsomorphism f
h:= {| def_hom := f; is_homomorphism_hom := F |}: Homomorphism A B
s: Sort σ
x: B s
(h o hom_inv h)%morphism s x = 1%morphism 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).
H: Funext
σ: Signature
A, B: precategory_algebra σ
IsEquiv catiso_to_uaiso
Proof.
H: Funext
σ: Signature
A, B: precategory_algebra σ
IsEquiv catiso_to_uaiso
  refine (isequiv_adjointify catiso_to_uaiso uaiso_to_catiso _ _).
H: Funext
σ: Signature
A, B: precategory_algebra σ
(λ x : A ≅ B, catiso_to_uaiso (uaiso_to_catiso x)) == idmap
H: Funext
σ: Signature
A, B: precategory_algebra σ
(λ x : A <~=~> B, uaiso_to_catiso (catiso_to_uaiso x)) == idmap
  -
H: Funext
σ: Signature
A, B: precategory_algebra σ
(λ x : A ≅ B, catiso_to_uaiso (uaiso_to_catiso x)) == idmap intros [f F G].
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: forall s : Sort σ, A s -> B s
F: IsHomomorphism f
G: IsIsomorphism f
catiso_to_uaiso
  (uaiso_to_catiso
     {|
       def_isomorphic := f;
       is_homomorphism_isomorphic := F;
       is_isomorphism_isomorphic := G
     |}) =
{|
  def_isomorphic := f;
  is_homomorphism_isomorphic := F;
  is_isomorphism_isomorphic := G
|} by apply path_hset_isomorphic.
  -
H: Funext
σ: Signature
A, B: precategory_algebra σ
(λ x : A <~=~> B, uaiso_to_catiso (catiso_to_uaiso x)) == idmap intros [f F].
H: Funext
σ: Signature
A, B: precategory_algebra σ
f: morphism (precategory_algebra σ) A B
F: Morphisms.IsIsomorphism f
uaiso_to_catiso
  (catiso_to_uaiso
     {|
       Morphisms.morphism_isomorphic := f;
       Morphisms.isisomorphism_isomorphic := F
     |}) =
{|
  Morphisms.morphism_isomorphic := f; Morphisms.isisomorphism_isomorphic := 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.
H: Funext
σ: Signature
A, B: precategory_algebra σ
Morphisms.idtoiso (precategory_algebra σ) (y:=B) =
catiso_to_uaiso^-1 o isomorphic_id o (path_setalgebra A B)^-1
Proof.
H: Funext
σ: Signature
A, B: precategory_algebra σ
Morphisms.idtoiso (precategory_algebra σ) (y:=B) =
catiso_to_uaiso^-1 o isomorphic_id o (path_setalgebra A B)^-1
  funext p.
H: Funext
σ: Signature
A, B: precategory_algebra σ
p: A = B
Morphisms.idtoiso (precategory_algebra σ) p =
catiso_to_uaiso^-1 (isomorphic_id ((path_setalgebra A B)^-1 p)) destruct p.
H: Funext
σ: Signature
A: precategory_algebra σ
Morphisms.idtoiso (precategory_algebra σ) 1 =
catiso_to_uaiso^-1 (isomorphic_id ((path_setalgebra A A)^-1 1)) 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 σ).
H: Univalence
σ: Signature
IsCategory (precategory_algebra σ)
Proof.
H: Univalence
σ: Signature
IsCategory (precategory_algebra σ)
  intros A B.
H: Univalence
σ: Signature
A, B: precategory_algebra σ
IsEquiv (Morphisms.idtoiso (precategory_algebra σ) (y:=B))
  rewrite path_idtoiso_isomorphic_id.
H: Univalence
σ: Signature
A, B: precategory_algebra σ
IsEquiv
  (λ x : A = B,
   catiso_to_uaiso^-1 (isomorphic_id ((path_setalgebra A B)^-1 x)))
  apply @isequiv_compose.
H: Univalence
σ: Signature
A, B: precategory_algebra σ
IsEquiv (λ x : A = B, isomorphic_id ((path_setalgebra A B)^-1 x))
H: Univalence
σ: Signature
A, B: precategory_algebra σ
IsEquiv catiso_to_uaiso^-1
  -
H: Univalence
σ: Signature
A, B: precategory_algebra σ
IsEquiv (λ x : A = B, isomorphic_id ((path_setalgebra A B)^-1 x)) rapply isequiv_compose.
  -
H: Univalence
σ: Signature
A, B: precategory_algebra σ
IsEquiv catiso_to_uaiso^-1 apply isequiv_inverse.
Qed.

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