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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** The first three levels of homotopy type theory: homotopy propositions,
homotopy sets and homotopy one types. For more information,
https://github.com/HoTT/HoTT
and
https://homotopytypetheory.org/book
Univalence is not assumed here, and equality is Coq's usual inductive
type eq in sort Prop. This is a little different from HoTT, where
sort Prop does not exist and equality is directly in sort Type. *)
(* It is almost impossible to prove that a type is a homotopy proposition
without funext, so we assume it here. *)
Require Import Coq.Logic.FunctionalExtensionality.
(* A homotopy proposition is a type that has at most one element.
Its unique inhabitant, when it exists, is to be interpreted as the
proof of the homotopy proposition.
Homotopy propositions are therefore an alternative to the sort Prop,
to select which types represent mathematical propositions. *)
Definition IsHProp (P : Type) : Prop
:= forall p q : P, p = q.
(* A homotopy set is a type such as each equality type x = y is a
homotopy proposition. For example, any type which equality is
decidable in sort Prop is a homotopy set, as shown in file
Coq.Logic.Eqdep_dec.v. *)
Definition IsHSet (X : Type) : Prop
:= forall (x y : X) (p q : x = y), p = q.
Definition IsHOneType (X : Type) : Prop
:= forall (x y : X) (p q : x = y) (r s : p = q), r = s.
Lemma forall_hprop : forall (A : Type) (P : A -> Prop),
(forall x:A, IsHProp (P x))
-> IsHProp (forall x:A, P x).
Proof.
intros A P H p q. apply functional_extensionality_dep.
intro x. apply H.
Qed.
(* Homotopy propositions are stable by conjunction, but not by disjunction,
which can have a proof by the left and another proof by the right. *)
Lemma and_hprop : forall P Q : Prop,
IsHProp P -> IsHProp Q -> IsHProp (P /\ Q).
Proof.
intros. intros p q. destruct p,q.
replace p0 with p. replace q0 with q. reflexivity.
apply H0. apply H.
Qed.
Lemma impl_hprop : forall P Q : Prop,
IsHProp Q -> IsHProp (P -> Q).
Proof.
intros P Q H p q. apply functional_extensionality.
intros. apply H.
Qed.
Lemma false_hprop : IsHProp False.
Proof.
intros p q. contradiction.
Qed.
Lemma true_hprop : IsHProp True.
Proof.
intros p q. destruct p,q. reflexivity.
Qed.
(* All negations are homotopy propositions. *)
Lemma not_hprop : forall P : Type, IsHProp (P -> False).
Proof.
intros P p q. apply functional_extensionality.
intros. contradiction.
Qed.
(* Homotopy propositions are included in homotopy sets.
They are the first 2 levels of a cumulative hierarchy of types
indexed by the natural numbers. In homotopy type theory,
homotopy propositions are call (-1)-types and homotopy
sets 0-types. *)
Lemma hset_hprop : forall X : Type,
IsHProp X -> IsHSet X.
Proof.
intros X H.
assert (forall (x y z:X) (p : y = z), eq_trans (H x y) p = H x z).
{ intros. unfold eq_trans, eq_ind. destruct p. reflexivity. }
assert (forall (x y z:X) (p : y = z),
p = eq_trans (eq_sym (H x y)) (H x z)).
{ intros. rewrite <- (H0 x y z p). unfold eq_trans, eq_sym, eq_ind.
destruct p, (H x y). reflexivity. }
intros x y p q.
rewrite (H1 x x y p), (H1 x x y q). reflexivity.
Qed.
Lemma eq_trans_cancel : forall {X : Type} {x y z : X} (p : x = y) (q r : y = z),
(eq_trans p q = eq_trans p r) -> q = r.
Proof.
intros. destruct p. simpl in H. destruct r.
simpl in H. rewrite eq_trans_refl_l in H. exact H.
Qed.
Lemma hset_hOneType : forall X : Type,
IsHSet X -> IsHOneType X.
Proof.
intros X f x y p q.
pose (fun a => f x y p a) as g.
assert (forall a (r : q = a), eq_trans (g q) r = g a).
{ intros. destruct a. subst q. reflexivity. }
intros r s. pose proof (H p (eq_sym r)).
pose proof (H p (eq_sym s)).
rewrite <- H1 in H0. apply eq_trans_cancel in H0.
rewrite <- eq_sym_involutive. rewrite <- (eq_sym_involutive r).
rewrite H0. reflexivity.
Qed.
(* "IsHProp X" sounds like a proposition, because it asserts
a property of the type X. And indeed: *)
Lemma hprop_hprop : forall X : Type,
IsHProp (IsHProp X).
Proof.
intros X p q.
apply forall_hprop. intro x.
apply forall_hprop. intro y. intros f g.
apply (hset_hprop X p).
Qed.
Lemma hprop_hset : forall X : Type,
IsHProp (IsHSet X).
Proof.
intros X f g.
apply functional_extensionality_dep. intro x.
apply functional_extensionality_dep. intro y.
apply functional_extensionality_dep. intro a.
apply functional_extensionality_dep. intro b.
apply (hset_hOneType). exact f.
Qed.
|
