(** This file defines [SetAlgebra], a specialized [Algebra] where
    the carriers are always sets. *)

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


Record SetAlgebra {σ : Signature} : Type := BuildSetAlgebra
  { algebra_setalgebra : Algebra σ
  ; is_hset_algebra_setalgebra : IsHSetAlgebra algebra_setalgebra }.

Arguments SetAlgebra : clear implicits.

Global Existing Instance is_hset_algebra_setalgebra.

Global Coercion algebra_setalgebra : SetAlgebra >-> Algebra.

(** To find a path [A = B] between set algebras [A B : SetAlgebra σ],
    it is enough to find a path between the defining algebras,
    [algebra_setalgebra A = algebra_setalgebra B]. *)

Lemma path_setalgebra `{Funext} {σ} (A B : SetAlgebra σ)
  (p : algebra_setalgebra A = algebra_setalgebra B)
  : A = B.
H: Funext
σ: Signature
A, B: SetAlgebra σ
p: A = B
A = B
Proof.
H: Funext
σ: Signature
A, B: SetAlgebra σ
p: A = B
A = B
  destruct A as [A AH], B as [B BH].
H: Funext
σ: Signature
A: Algebra σ
AH: IsHSetAlgebra A
B: Algebra σ
BH: IsHSetAlgebra B
p: {|
  algebra_setalgebra := A;
  is_hset_algebra_setalgebra := AH
|} =
{|
  algebra_setalgebra := B;
  is_hset_algebra_setalgebra := BH
|}
{|
  algebra_setalgebra := A;
  is_hset_algebra_setalgebra := AH
|} =
{|
  algebra_setalgebra := B;
  is_hset_algebra_setalgebra := BH
|} cbn in *.
H: Funext
σ: Signature
A: Algebra σ
AH: IsHSetAlgebra A
B: Algebra σ
BH: IsHSetAlgebra B
p: A = B
{|
  algebra_setalgebra := A;
  is_hset_algebra_setalgebra := AH
|} =
{|
  algebra_setalgebra := B;
  is_hset_algebra_setalgebra := BH
|}
  transparent assert (a : (p#AH = BH)) by apply path_ishprop.
H: Funext
σ: Signature
A: Algebra σ
AH: IsHSetAlgebra A
B: Algebra σ
BH: IsHSetAlgebra B
p: A = B
H0:= path_ishprop (transport IsHSetAlgebra p AH) BH: transport IsHSetAlgebra p AH = BH
{|
  algebra_setalgebra := A;
  is_hset_algebra_setalgebra := AH
|} =
{|
  algebra_setalgebra := B;
  is_hset_algebra_setalgebra := BH
|}
  by path_induction.
Defined.

(** The id path is mapped to the id path by [path_setalgebra]. *)

Lemma path_setalgebra_1 `{Funext} {σ} (A : SetAlgebra σ)
  : path_setalgebra A A idpath = idpath.
H: Funext
σ: Signature
A: SetAlgebra σ
path_setalgebra A A 1 = 1
Proof.
H: Funext
σ: Signature
A: SetAlgebra σ
path_setalgebra A A 1 = 1
  transparent assert (p :
      (∀ I : IsHSetAlgebra A, path_ishprop I I = idpath)).
H: Funext
σ: Signature
A: SetAlgebra σ
forall I : IsHSetAlgebra A, path_ishprop I I = 1
H: Funext
σ: Signature
A: SetAlgebra σ
p:= ?Goal: forall I : IsHSetAlgebra A, path_ishprop I I = 1
path_setalgebra A A 1 = 1
  -
H: Funext
σ: Signature
A: SetAlgebra σ
forall I : IsHSetAlgebra A, path_ishprop I I = 1 intros.
H: Funext
σ: Signature
A: SetAlgebra σ
I: IsHSetAlgebra A
path_ishprop I I = 1 apply path_ishprop.
  -
H: Funext
σ: Signature
A: SetAlgebra σ
p:= λ I : IsHSetAlgebra A,
path_ishprop (path_ishprop I I) 1: forall I : IsHSetAlgebra A, path_ishprop I I = 1
path_setalgebra A A 1 = 1 unfold path_setalgebra.
H: Funext
σ: Signature
A: SetAlgebra σ
p:= λ I : IsHSetAlgebra A,
path_ishprop (path_ishprop I I) 1: forall I : IsHSetAlgebra A, path_ishprop I I = 1
paths_rect (IsHSetAlgebra A)
  (transport IsHSetAlgebra 1
     (is_hset_algebra_setalgebra A))
  (λ (BH : IsHSetAlgebra A)
   (_ : transport IsHSetAlgebra 1
          (is_hset_algebra_setalgebra A) = BH),
   {|
     algebra_setalgebra := A;
     is_hset_algebra_setalgebra :=
       is_hset_algebra_setalgebra A
   |} =
   {|
     algebra_setalgebra := A;
     is_hset_algebra_setalgebra := BH
   |})
  (paths_rect (Algebra σ) A
     (λ (B : Algebra σ) (p : A = B),
      {|
        algebra_setalgebra := A;
        is_hset_algebra_setalgebra :=
          is_hset_algebra_setalgebra A
      |} =
      {|
        algebra_setalgebra := B;
        is_hset_algebra_setalgebra :=
          transport IsHSetAlgebra p
            (is_hset_algebra_setalgebra A)
      |}) 1 A 1) (is_hset_algebra_setalgebra A)
  (path_ishprop
     (transport IsHSetAlgebra 1
        (is_hset_algebra_setalgebra A))
     (is_hset_algebra_setalgebra A)) = 1 by rewrite p.
Qed.

(** The function [path_setalgebra A B] is an equivalence with inverse
    [ap algebra_setalgebra]. *)

Global Instance isequiv_path_setalgebra `{Funext} {σ : Signature}
  (A B : SetAlgebra σ)
  : IsEquiv (path_setalgebra A B).
H: Funext
σ: Signature
A, B: SetAlgebra σ
IsEquiv (path_setalgebra A B)
Proof.
H: Funext
σ: Signature
A, B: SetAlgebra σ
IsEquiv (path_setalgebra A B)
  refine (isequiv_adjointify
            (path_setalgebra A B) (ap algebra_setalgebra) _ _).
H: Funext
σ: Signature
A, B: SetAlgebra σ
(λ x : A = B,
 path_setalgebra A B (ap algebra_setalgebra x)) ==
idmap
H: Funext
σ: Signature
A, B: SetAlgebra σ
(λ x : A = B,
 ap algebra_setalgebra (path_setalgebra A B x)) ==
idmap
  -
H: Funext
σ: Signature
A, B: SetAlgebra σ
(λ x : A = B,
 path_setalgebra A B (ap algebra_setalgebra x)) ==
idmap abstract (intro p; induction p; by rewrite path_setalgebra_1).
  -
H: Funext
σ: Signature
A, B: SetAlgebra σ
(λ x : A = B,
 ap algebra_setalgebra (path_setalgebra A B x)) ==
idmap abstract (
      intro e; destruct A as [A AH], B as [B BH];
      cbn in e; destruct e;
      unfold path_setalgebra; by destruct path_ishprop).
Defined.