aboutsummaryrefslogtreecommitdiff
path: root/ex/HoTT Book
diff options
context:
space:
mode:
Diffstat (limited to 'ex/HoTT Book')
-rw-r--r--ex/HoTT Book/Ch1.thy37
1 files changed, 0 insertions, 37 deletions
diff --git a/ex/HoTT Book/Ch1.thy b/ex/HoTT Book/Ch1.thy
deleted file mode 100644
index 84a5cf4..0000000
--- a/ex/HoTT Book/Ch1.thy
+++ /dev/null
@@ -1,37 +0,0 @@
-theory Ch1
- imports "../../HoTT"
-begin
-
-chapter \<open>HoTT Book, Chapter 1\<close>
-
-section \<open>1.6 Dependent pair types (\<Sigma>-types)\<close>
-
-text "Prove that the only inhabitants of the \<Sigma>-type are those given by the pair constructor."
-
-schematic_goal
- assumes "(\<Sum>x:A. B(x)): U(i)" and "p: \<Sum>x:A. B(x)"
- shows "?a: p =[\<Sum>x:A. B(x)] <fst p, snd p>"
-
-text "Proof by induction on \<open>p: \<Sum>x:A. B(x)\<close>:"
-
-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> =[\<Sum>x:A. B(x)] <fst <x,y>, snd <x,y>>"
- proof (subst (0 1) comp)
- text "
- The computation rules for \<open>fst\<close> and \<open>snd\<close> require that \<open>x\<close> and \<open>y\<close> 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 \<open>fst\<close> and \<open>snd\<close>."
- show "x: A" and "y: B(x)" by (fact asm)+
-
- qed (derive lems: assms asm)
-
-qed (derive lems: assms)
-
-
-end \ No newline at end of file