1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
(** 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 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.
Proof.
destruct A as [A AH], B as [B BH]. cbn in *.
transparent assert (a : (p#AH = BH)) by apply path_ishprop.
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.
Proof.
transparent assert (p :
(∀ I : IsHSetAlgebra A, path_ishprop I I = idpath)).
- intros. apply path_ishprop.
- unfold path_setalgebra. 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).
Proof.
refine (isequiv_adjointify
(path_setalgebra A B) (ap algebra_setalgebra) _ _).
- abstract (intro p; induction p; by rewrite path_setalgebra_1).
- 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.
|
