diff options
Diffstat (limited to 'ex/HoTT Book/Ch1.thy')
-rw-r--r-- | ex/HoTT Book/Ch1.thy | 37 |
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 |