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

Require Export HoTT.Classes.interfaces.ua_algebra.


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

Arguments SetAlgebra : clear implicits.

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 σ) (p0 : A = B),
      {|
        algebra_setalgebra := A;
        is_hset_algebra_setalgebra := is_hset_algebra_setalgebra A
      |} =
      {|
        algebra_setalgebra := B;
        is_hset_algebra_setalgebra :=
          transport IsHSetAlgebra p0 (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]. *)

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.