blob: c89b5697cd6710d582b75b254e260bcd82c51513 (
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
|
(********
Isabelle/HoTT: Projections
Feb 2019
Projection functions for the dependent sum type.
********)
theory Projections
imports Prod Sum
begin
definition fst ("(2fst[_,/ _])")
where "fst[A, B] ≡ λ(p: ∑x: A. B x). indSum (λ_. A) (λx y. x) p"
definition snd ("(2snd[_,/ _])")
where "snd[A, B] ≡ λ(p: ∑x: A. B x). indSum (λp. B (fst[A, B]`p)) (λx y. y) p"
lemma fst_type:
assumes [intro]: "A: U i" "B: A ↝ U i"
shows "fst[A, B]: (∑x: A. B x) → A"
unfolding fst_def by derive
lemma fst_cmp:
assumes [intro]: "A: U i" "B: A ↝ U i" "a: A" "b: B a"
shows "fst[A, B]`<a, b> ≡ a"
unfolding fst_def by derive
lemma snd_type:
assumes [intro]: "A: U i" "B: A ↝ U i"
shows "snd[A, B]: ∏(p: ∑x: A. B x). B (fst[A,B]`p)"
unfolding snd_def by (derive lems: fst_type comp: fst_cmp)
lemma snd_cmp:
assumes [intro]: "A: U i" "B: A ↝ U i" "a: A" "b: B a"
shows "snd[A, B]`<a, b> ≡ b"
unfolding snd_def proof derive qed (derive lems: assms fst_type comp: fst_cmp)
lemmas proj_type [intro] = fst_type snd_type
lemmas proj_comp [comp] = fst_cmp snd_cmp
end
|
