forked from UniMath/UniMath
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy patht02_paths.v
142 lines (130 loc) · 2.83 KB
/
t02_paths.v
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
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Lemma path_inv_transitivity
(X : UU)
(x y z : X)
(p : x = y)
(q : y = z)
: z = x.
Proof.
symmetry. (* This turns the goal into x = z *)
transitivity y. (* This splits the goal into x = y and y = z *)
- exact p.
- exact q.
Qed.
Definition path_inv_transitivity'
(X : UU)
(x y z : X)
(p : x = y)
(q : y = z)
: z = x
:= !(p @ q).
Lemma postcompose_path_path
(X : UU)
(x y z : X)
(p q : x = y)
(r : y = z)
(H : p = q)
: p @ r = q @ r.
Proof.
apply (maponpaths (λ e, e @ r)).
exact H.
Defined.
Lemma compose_path_path
(X : UU)
(x y z : X)
(p q : x = y)
(r s : y = z)
(H1 : p = q)
(H2 : r = s)
: p @ r = q @ s.
Proof.
apply maponpaths_12.
- exact H1.
- exact H2.
Defined.
Lemma isaprop_function_to_unit
(X : UU)
(f g : X → unit)
: f = g.
Proof.
apply funextfun. (* This changes the goal to ∏ x, f x = g x *)
intro x.
induction (f x), (g x). (* This replaces f x and g x by tt *)
reflexivity.
Qed.
Lemma function_value_path
(X : UU)
(f : X → unit)
(x : X)
: f x = tt.
Proof.
apply (eqtohomot (g := λ _, tt)). (* This changes the goal to f = (λ _, tt) *)
apply (isaprop_function_to_unit).
Qed.
Lemma function_value_path'
(X : UU)
(f : X → unit)
(x : X)
: f x = tt.
Proof.
induction (f x).
reflexivity.
Qed.
Lemma isaprop_unit_pair
(x y : unit × unit)
: x = y.
Proof.
apply dirprodeq. (* This splits up the goal into pr1 x = pr1 y and pr2 x = pr2 y *)
- induction (pr1 x), (pr1 y).
reflexivity.
- induction (pr2 x), (pr2 y).
reflexivity.
Qed.
Definition combine_dependent_sum_paths
(X : UU)
(Y : X → UU)
(x x' : X)
(y : Y x)
(y' : Y x')
(H : ∑ (Hx : x = x'), transportf Y Hx y = y')
: (x ,, y) = (x' ,, y').
Proof.
induction H as [Hx Hy].
use total2_paths_f.
- exact Hx.
- exact Hy.
Defined.
Definition split_dependent_sum_paths
(X : UU)
(Y : X → UU)
(x x' : X)
(y : Y x)
(y' : Y x')
(H : (x ,, y) = (x' ,, y'))
: ∑ (H : x = x'), transportf Y H y = y'.
Proof.
use tpair.
- exact (base_paths (x ,, y) (x' ,, y') H).
- exact (fiber_paths H).
Defined.
Lemma isaprop_iscontr
(X : hSet)
(x x' : ∑ (x : X), (∏ y, y = x))
: x = x'.
Proof.
apply subtypePath. (* This splits the goal into `isPredicate is_even` and `pr1 m = pr1 m'` *)
- intro y. (* This changes the goal to `isaprop (∏ y', y' = y)` *)
apply impred_isaprop. (* This uses a lemma to swap the `isaprop` with the `∏ y'` *)
intro y'.
apply setproperty. (* This uses the fact that `X` is a set, so that `y' = y` is a proposition *)
- apply (pr2 x').
Qed.
Definition isaprop_empty_product (P : empty -> UU)
(f g : (∏ x, P x))
: f = g.
Proof.
apply funextsec.
intro x.
induction x.
Qed.