From d8699451025a3bd5e8955e07fa879ed248418949 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 16 Aug 2018 16:28:50 +0200 Subject: Some comments and reorganization --- ex/HoTT Book/Ch1.thy | 37 ------------------------------------- 1 file changed, 37 deletions(-) delete mode 100644 ex/HoTT Book/Ch1.thy (limited to 'ex/HoTT Book/Ch1.thy') 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 \HoTT Book, Chapter 1\ - -section \1.6 Dependent pair types (\-types)\ - -text "Prove that the only inhabitants of the \-type are those given by the pair constructor." - -schematic_goal - assumes "(\x:A. B(x)): U(i)" and "p: \x:A. B(x)" - shows "?a: p =[\x:A. B(x)] " - -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:A. B(x)] , snd >" - 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) - - -end \ No newline at end of file -- cgit v1.2.3