blob: 1473e0879f88e480cb76b768057fe2ed1422ed4d (
plain)
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
|
(********
Isabelle/HoTT: Projections
Feb 2019
Projection functions for the dependent sum type.
********)
theory Projections
imports HoTT_Methods Prod Sum
begin
definition fst :: "[t, t] ⇒ t" where "fst A p ≡ indSum (λ_. A) (λx y. x) p"
lemma fst_type:
assumes "A: U i" and "p: ∑x: A. B x" shows "fst A p: A"
unfolding fst_def by (derive lems: assms)
declare fst_type [intro]
lemma fst_cmp:
assumes "A: U i" and "B: A ↝ U i" and "a: A" and "b: B a" shows "fst A <a, b> ≡ a"
unfolding fst_def by (subst comp) (derive lems: assms)
declare fst_cmp [comp]
definition snd :: "[t, t ⇒ t, t] ⇒ t" where "snd A B p ≡ indSum (λp. B (fst A p)) (λx y. y) p"
lemma snd_type:
assumes "A: U i" and "B: A ↝ U i" and "p: ∑x: A. B x" shows "snd A B p: B (fst A p)"
unfolding snd_def proof (routine add: assms)
fix x y assume "x: A" and "y: B x"
with assms have [comp]: "fst A <x, y> ≡ x" by derive
note ‹y: B x› then show "y: B (fst A <x, y>)" by compute
qed
lemma snd_cmp:
assumes "A: U i" and "B: A ↝ U i" and "a: A" and "b: B a" shows "snd A B <a,b> ≡ b"
unfolding snd_def by (derive lems: assms)
lemmas Proj_type [intro] = fst_type snd_type
lemmas Proj_comp [comp] = fst_cmp snd_cmp
end
|
