(** This file develops [Isomorphic], [≅]. See ua_homomorphism.v for
    [IsHomomorphism] and [IsIsomorphism]. *)

Require Export HoTT.Classes.theory.ua_homomorphism.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Require Import
  HoTT.Types
  HoTT.Tactics.

(** Two algebras [A B : Algebra σ] are isomorphic if there is an
    isomorphism [∀ s, A s → B s]. *)

Record Isomorphic {σ : Signature} (A B : Algebra σ) := BuildIsomorphic
  { def_isomorphic : ∀ s, A s → B s
  ; is_homomorphism_isomorphic :: IsHomomorphism def_isomorphic
  ; is_isomorphism_isomorphic :: IsIsomorphism def_isomorphic }.

Arguments BuildIsomorphic {σ A B} def_isomorphic
            {is_homomorphism_isomorphic} {is_isomorphism_isomorphic}.

Arguments def_isomorphic {σ A B}.
Arguments is_homomorphism_isomorphic {σ A B}.
Arguments is_isomorphism_isomorphic {σ A B}.

Module isomorphic_notations.
  Global Notation "A ≅ B" := (Isomorphic A B) : Algebra_scope.
End isomorphic_notations.

Import isomorphic_notations.

Definition SigIsomorphic {σ : Signature} (A B : Algebra σ) :=
  { def_iso : ∀ s, A s → B s
  | { _ : IsHomomorphism def_iso | IsIsomorphism def_iso }}.

Lemma issig_isomorphic {σ : Signature} (A B : Algebra σ)
  : SigIsomorphic A B <~> A ≅ B.
σ: Signature
A, B: Algebra σ
SigIsomorphic A B <~> A ≅ B
Proof.
σ: Signature
A, B: Algebra σ
SigIsomorphic A B <~> A ≅ B
  issig.
Defined.

(** Isomorphic algebras can be identified [A ≅ B → A = B]. *)

Corollary id_isomorphic `{Univalence} {σ} {A B : Algebra σ} (e : A ≅ B)
  : A = B.
H: Univalence
σ: Signature
A, B: Algebra σ
e: A ≅ B
A = B
Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
e: A ≅ B
A = B
  exact (path_isomorphism (def_isomorphic e)).
Defined.

(** Identified algebras are isomorphic [A = B → A ≅ B] *)

Lemma isomorphic_id {σ} {A B : Algebra σ} (p : A = B) : A ≅ B.
σ: Signature
A, B: Algebra σ
p: A = B
A ≅ B
Proof.
σ: Signature
A, B: Algebra σ
p: A = B
A ≅ B
  destruct p.
σ: Signature
A: Algebra σ
A ≅ A exact (BuildIsomorphic (hom_id A)).
Defined.

(** To find a path between two witnesses [F G : A ≅ B], it suffices
    to find a path between the defining families of functions and
    the [is_homomorphism_hom] witnesses. *)

Lemma path_isomorphic `{Funext} {σ : Signature} {A B : Algebra σ}
  (F G : A ≅ B) (a : def_isomorphic F = def_isomorphic G)
  (b : a#(is_homomorphism_isomorphic F) = is_homomorphism_isomorphic G)
  : F = G.
H: Funext
σ: Signature
A, B: Algebra σ
F, G: A ≅ B
a: def_isomorphic F = def_isomorphic G
b: transport IsHomomorphism a
  (is_homomorphism_isomorphic F) =
is_homomorphism_isomorphic G
F = G
Proof.
H: Funext
σ: Signature
A, B: Algebra σ
F, G: A ≅ B
a: def_isomorphic F = def_isomorphic G
b: transport IsHomomorphism a
  (is_homomorphism_isomorphic F) =
is_homomorphism_isomorphic G
F = G
  apply (ap (issig_isomorphic A B)^-1)^-1.
H: Funext
σ: Signature
A, B: Algebra σ
F, G: A ≅ B
a: def_isomorphic F = def_isomorphic G
b: transport IsHomomorphism a
  (is_homomorphism_isomorphic F) =
is_homomorphism_isomorphic G
(issig_isomorphic A B)^-1 F =
(issig_isomorphic A B)^-1 G
  srapply path_sigma.
H: Funext
σ: Signature
A, B: Algebra σ
F, G: A ≅ B
a: def_isomorphic F = def_isomorphic G
b: transport IsHomomorphism a
  (is_homomorphism_isomorphic F) =
is_homomorphism_isomorphic G
((issig_isomorphic A B)^-1 F).1 =
((issig_isomorphic A B)^-1 G).1
H: Funext
σ: Signature
A, B: Algebra σ
F, G: A ≅ B
a: def_isomorphic F = def_isomorphic G
b: transport IsHomomorphism a
  (is_homomorphism_isomorphic F) =
is_homomorphism_isomorphic G
transport
  (λ def_iso : forall s : Sort σ, A s -> B s,
   {H : IsHomomorphism def_iso &
   IsIsomorphism def_iso}) ?p
  ((issig_isomorphic A B)^-1 F).2 =
((issig_isomorphic A B)^-1 G).2
  -
H: Funext
σ: Signature
A, B: Algebra σ
F, G: A ≅ B
a: def_isomorphic F = def_isomorphic G
b: transport IsHomomorphism a
  (is_homomorphism_isomorphic F) =
is_homomorphism_isomorphic G
((issig_isomorphic A B)^-1 F).1 =
((issig_isomorphic A B)^-1 G).1 exact a.
  -
H: Funext
σ: Signature
A, B: Algebra σ
F, G: A ≅ B
a: def_isomorphic F = def_isomorphic G
b: transport IsHomomorphism a
  (is_homomorphism_isomorphic F) =
is_homomorphism_isomorphic G
transport
  (λ def_iso : forall s : Sort σ, A s -> B s,
   {H : IsHomomorphism def_iso &
   IsIsomorphism def_iso}) a
  ((issig_isomorphic A B)^-1 F).2 =
((issig_isomorphic A B)^-1 G).2 apply path_sigma_hprop.
H: Funext
σ: Signature
A, B: Algebra σ
F, G: A ≅ B
a: def_isomorphic F = def_isomorphic G
b: transport IsHomomorphism a
  (is_homomorphism_isomorphic F) =
is_homomorphism_isomorphic G
(transport
   (λ def_iso : forall s : Sort σ, A s -> B s,
    {H : IsHomomorphism def_iso &
    IsIsomorphism def_iso}) a
   ((issig_isomorphic A B)^-1 F).2).1 =
(((issig_isomorphic A B)^-1 G).2).1
    refine (ap _ (transport_sigma _ _) @ _).
H: Funext
σ: Signature
A, B: Algebra σ
F, G: A ≅ B
a: def_isomorphic F = def_isomorphic G
b: transport IsHomomorphism a
  (is_homomorphism_isomorphic F) =
is_homomorphism_isomorphic G
(transport IsHomomorphism a
   (((issig_isomorphic A B)^-1 F).2).1;
transportD IsHomomorphism IsIsomorphism a
  (((issig_isomorphic A B)^-1 F).2).1
  (((issig_isomorphic A B)^-1 F).2).2).1 =
(((issig_isomorphic A B)^-1 G).2).1
    apply b.
Defined.

(** Suppose [IsHSetAlgebra B]. To find a path between two isomorphic
    witnesses [F G : A ≅ B], it suffices to find a path between the
    defining families of functions. *)

Lemma path_hset_isomorphic `{Funext} {σ : Signature} {A B : Algebra σ}
  `{IsHSetAlgebra B} (F G : A ≅ B)
  (a : def_isomorphic F = def_isomorphic G)
  : F = G.
H: Funext
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
F, G: A ≅ B
a: def_isomorphic F = def_isomorphic G
F = G
Proof.
H: Funext
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
F, G: A ≅ B
a: def_isomorphic F = def_isomorphic G
F = G
  apply (path_isomorphic F G a).
H: Funext
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
F, G: A ≅ B
a: def_isomorphic F = def_isomorphic G
transport IsHomomorphism a
  (is_homomorphism_isomorphic F) =
is_homomorphism_isomorphic G apply path_ishprop.
Defined.

Section path_def_isomorphic_id_transport.
  Context {σ : Signature} {A B : Algebra σ}.

  Lemma path_def_isomorphic_id_transport_dom (p : A = B)
    : def_isomorphic (isomorphic_id p)
      = transport (λ C, ∀ s, C s → B s) (ap carriers p)^ (hom_id B).
σ: Signature
A, B: Algebra σ
p: A = B
def_isomorphic (isomorphic_id p) =
transport
  (λ C : Carriers σ, forall s : Sort σ, C s -> B s)
  (ap carriers p)^ (hom_id B)
  Proof.
σ: Signature
A, B: Algebra σ
p: A = B
def_isomorphic (isomorphic_id p) =
transport
  (λ C : Carriers σ, forall s : Sort σ, C s -> B s)
  (ap carriers p)^ (hom_id B)
    by path_induction.
  Defined.

  Lemma path_def_isomorphic_id_transport_cod (p : A = B)
    : def_isomorphic (isomorphic_id p)
      = transport (λ C, ∀ s, A s → C s) (ap carriers p) (hom_id A).
σ: Signature
A, B: Algebra σ
p: A = B
def_isomorphic (isomorphic_id p) =
transport
  (λ C : Carriers σ, forall s : Sort σ, A s -> C s)
  (ap carriers p) (hom_id A)
  Proof.
σ: Signature
A, B: Algebra σ
p: A = B
def_isomorphic (isomorphic_id p) =
transport
  (λ C : Carriers σ, forall s : Sort σ, A s -> C s)
  (ap carriers p) (hom_id A)
    by path_induction.
  Defined.
End path_def_isomorphic_id_transport.

(** If [IsHSetAlgebra A], then [path_isomorphism] maps the identity
    homomorphism of [A] to the identity path. *)

(* I suspect that the following lemma holds even when [A] is not a set
   algebra. To show this, [path_isomorphism] and [path_operations_equiv]
   should be made transparent, which they are not at the moment. *)

Lemma path_path_isomorphism_hom_id_hset `{Univalence} {σ : Signature}
  (A : Algebra σ) `{IsHSetAlgebra A}
  : path_isomorphism (hom_id A) = idpath.
H: Univalence
σ: Signature
A: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra A
path_isomorphism (hom_id A) = 1
Proof.
H: Univalence
σ: Signature
A: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra A
path_isomorphism (hom_id A) = 1
  apply path_path_hset_algebra.
H: Univalence
σ: Signature
A: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra A
ap carriers (path_isomorphism (hom_id A)) =
ap carriers 1
  rewrite path_ap_carriers_path_algebra.
H: Univalence
σ: Signature
A: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra A
path_forall A A
  (λ i : Sort σ,
   path_universe (equiv_isomorphism (hom_id A) i)) =
ap carriers 1
  apply (paths_ind (λ s, idpath) (λ f _, path_forall A A f = idpath)).
H: Univalence
σ: Signature
A: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra A
path_forall A A (λ s : Sort σ, 1) = 1
H: Univalence
σ: Signature
A: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra A
(λ s : Sort σ, 1) =
(λ i : Sort σ,
 path_universe (equiv_isomorphism (hom_id A) i))
  -
H: Univalence
σ: Signature
A: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra A
path_forall A A (λ s : Sort σ, 1) = 1 apply path_forall_1.
  -
H: Univalence
σ: Signature
A: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra A
(λ s : Sort σ, 1) =
(λ i : Sort σ,
 path_universe (equiv_isomorphism (hom_id A) i)) intros.
H: Univalence
σ: Signature
A: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra A
(λ s : Sort σ, 1) =
(λ i : Sort σ,
 path_universe (equiv_isomorphism (hom_id A) i))
    funext s.
H: Univalence
σ: Signature
A: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra A
s: Sort σ
1 = path_universe (equiv_isomorphism (hom_id A) s)
    symmetry.
H: Univalence
σ: Signature
A: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra A
s: Sort σ
path_universe (equiv_isomorphism (hom_id A) s) = 1
    rewrite (path_ishprop _ (isequiv_idmap (A s))).
H: Univalence
σ: Signature
A: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra A
s: Sort σ
path_universe (equiv_isomorphism (hom_id A) s) = 1
    apply path_universe_1.
Qed.

(** The following section shows that [isomorphic_id] is an equivalence
    with inverse [id_isomorphic]. *)

Section isequiv_isomorphic_id.
  Context `{Univalence} {σ} (A B : Algebra σ) `{IsHSetAlgebra B}.

  Lemma sect_id_isomorphic : (@isomorphic_id σ A B) o id_isomorphic == idmap.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
isomorphic_id o id_isomorphic == idmap
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
isomorphic_id o id_isomorphic == idmap
    intro F.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
F: A ≅ B
isomorphic_id (id_isomorphic F) = F
    apply path_hset_isomorphic.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
F: A ≅ B
def_isomorphic (isomorphic_id (id_isomorphic F)) =
def_isomorphic F
    rewrite path_def_isomorphic_id_transport_cod.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
F: A ≅ B
transport
  (λ C : Carriers σ, forall s : Sort σ, A s -> C s)
  (ap carriers (id_isomorphic F)) (hom_id A) =
def_isomorphic F
    funext s x.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
F: A ≅ B
s: Sort σ
x: A s
transport
  (λ C : Carriers σ, forall s : Sort σ, A s -> C s)
  (ap carriers (id_isomorphic F)) (hom_id A) s x =
def_isomorphic F s x
    rewrite !transport_forall_constant.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
F: A ≅ B
s: Sort σ
x: A s
transport (λ x : Carriers σ, x s)
  (ap carriers (id_isomorphic F)) (hom_id A s x) =
def_isomorphic F s x
    rewrite path_ap_carriers_path_algebra.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
F: A ≅ B
s: Sort σ
x: A s
transport (λ x : Carriers σ, x s)
  (path_forall A B
     (λ i : Sort σ,
      path_universe
        (equiv_isomorphism (def_isomorphic F) i)))
  (hom_id A s x) = def_isomorphic F s x
    transport_path_forall_hammer.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
F: A ≅ B
s: Sort σ
x: A s
transport idmap
  (path_universe
     (equiv_isomorphism (def_isomorphic F) s))
  (hom_id A s x) = def_isomorphic F s x
    apply transport_path_universe.
  Qed.

  Lemma sect_isomorphic_id : id_isomorphic o (@isomorphic_id σ A B) == idmap.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
id_isomorphic o isomorphic_id == idmap
  Proof.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
id_isomorphic o isomorphic_id == idmap
    intro p.
H: Univalence
σ: Signature
A, B: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra B
p: A = B
id_isomorphic (isomorphic_id p) = p
    destruct p.
H: Univalence
σ: Signature
A: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra A
id_isomorphic (isomorphic_id 1) = 1
    apply path_path_isomorphism_hom_id_hset.
H: Univalence
σ: Signature
A: Algebra σ
IsHSetAlgebra0: IsHSetAlgebra A
IsHSetAlgebra A
    exact _.
  Qed.

  #[export] Instance isequiv_isomorphic_id : IsEquiv (@isomorphic_id σ A B)
    := isequiv_adjointify
          isomorphic_id
          id_isomorphic
          sect_id_isomorphic
          sect_isomorphic_id.

End isequiv_isomorphic_id.