blob: a577fca78ab72c566c0ed8ecb623f5f49eb2233a (
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
46
47
48
49
50
51
52
53
54
55
|
(* Title: HoTT/ex/HoTT book/Ch1.thy
Author: Josh Chen
A formalization of some content of Chapter 1 of the Homotopy Type Theory book.
*)
theory Ch1
imports "../../HoTT"
begin
chapter ‹HoTT Book, Chapter 1›
section ‹1.6 Dependent pair types (Σ-types)›
text "Propositional uniqueness principle:"
schematic_goal
assumes "(∑x:A. B(x)): U(i)" and "p: ∑x:A. B(x)"
shows "?a: p =[∑x:A. B(x)] <fst p, snd p>"
text "Proof by induction on ‹p: ∑x:A. B(x)›:"
proof (rule Sum_elim[where ?p=p])
text "We just need to prove the base case; the rest will be taken care of automatically."
fix x y assume asm: "x: A" "y: B(x)" show
"refl(<x,y>): <x,y> =[∑x:A. B(x)] <fst <x,y>, snd <x,y>>"
proof (subst (0 1) comp)
text "
The computation rules for ‹fst› and ‹snd› require that ‹x› and ‹y› have appropriate types.
The automatic proof methods have trouble picking the appropriate types, so we state them explicitly,
"
show "x: A" and "y: B(x)" by (fact asm)+
text "...twice, once each for the substitutions of ‹fst› and ‹snd›."
show "x: A" and "y: B(x)" by (fact asm)+
qed (derive lems: assms asm)
qed (derive lems: assms)
section ‹Exercises›
text "Exercise 1.13"
abbreviation "not" ("¬'(_')") where "¬(A) ≡ A → 𝟬"
text "This proof requires the use of universe cumulativity."
proposition assumes "A: U(i)" shows "❙λf. f`(inr(❙λa. f`inl(a))): ¬(¬(A + ¬(A)))"
by (derive lems: assms U_cumulative[where ?A=𝟬 and ?i=O and ?j=i])
end
|
