blob: 509402bb183a84521d92c6392cb8d038aaf36b22 (
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
|
(*
Title: Projections.thy
Author: Joshua Chen
Date: 2018
Projection functions ‹fst› and ‹snd› for the dependent sum type.
*)
theory Projections
imports HoTT_Methods Prod Sum
begin
definition fst :: "t ⇒ t" where "fst p ≡ ind⇩∑ (λx y. x) p"
definition snd :: "t ⇒ t" where "snd p ≡ ind⇩∑ (λx y. y) p"
lemma fst_type:
assumes "A: U i" and "B: A ⟶ U i" and "p: ∑x:A. B x" shows "fst p: A"
unfolding fst_def by (derive lems: assms)
lemma fst_comp:
assumes "A: U i" and "B: A ⟶ U i" and "a: A" and "b: B a" shows "fst <a,b> ≡ a"
unfolding fst_def by compute (derive lems: assms)
lemma snd_type:
assumes "A: U i" and "B: A ⟶ U i" and "p: ∑x:A. B x" shows "snd p: B (fst p)"
unfolding snd_def proof (derive lems: assms)
show "⋀p. p: ∑x:A. B x ⟹ fst p: A" using assms(1-2) by (rule fst_type)
fix x y assume asm: "x: A" "y: B x"
show "y: B (fst <x,y>)" by (derive lems: asm assms fst_comp)
qed
lemma snd_comp:
assumes "A: U i" and "B: A ⟶ U i" and "a: A" and "b: B a" shows "snd <a,b> ≡ b"
unfolding snd_def by (derive lems: assms)
lemmas Proj_types [intro] = fst_type snd_type
lemmas Proj_comps [comp] = fst_comp snd_comp
end
|
