From c2dfffffb7586662c67e44a2d255a1a97ab0398b Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 2 Apr 2020 17:57:48 +0200
Subject: Brand-spanking new version using Spartan infrastructure

---
 ex/Book/Ch1.thy | 50 --------------------------------------------------
 1 file changed, 50 deletions(-)
 delete mode 100644 ex/Book/Ch1.thy

(limited to 'ex/Book/Ch1.thy')

diff --git a/ex/Book/Ch1.thy b/ex/Book/Ch1.thy
deleted file mode 100644
index dfb1879..0000000
--- a/ex/Book/Ch1.thy
+++ /dev/null
@@ -1,50 +0,0 @@
-(*
-Title:  ex/Book/Ch1.thy
-Author: Josh Chen
-Date:   2018
-
-A formalization of some content of Chapter 1 of the Homotopy Type Theory book.
-*)
-
-theory Ch1
-imports "../../HoTT"
-
-begin
-
-chapter \<open>HoTT Book, Chapter 1\<close>
-
-section \<open>1.6 Dependent pair types (\<Sum>-types)\<close>
-
-paragraph \<open>Propositional uniqueness principle.\<close>
-
-schematic_goal
-  assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x"
-  shows "?a: p =[\<Sum>x:A. B x] <fst p, snd p>"
-
-text \<open>Proof by induction on @{term "p: \<Sum>x:A. B x"}:\<close>
-
-proof (rule Sum_elim[where ?p=p])
-  text \<open>We prove the base case.\<close>
-  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 compute
-    show "x: A" and "y: B x" by (fact asm)+  \<comment> \<open>Hint the correct types.\<close>
-
-    text \<open>And now @{method derive} takes care of the rest.
-\<close>
-  qed (derive lems: assms asm)
-qed (derive lems: assms)
-
-
-section \<open>Exercises\<close>
-
-paragraph \<open>Exercise 1.13\<close>
-
-abbreviation "not" ("\<not>_") where "\<not>A \<equiv> A \<rightarrow> \<zero>"
-
-text "This proof requires the use of universe cumulativity."
-
-proposition assumes "A: U i" shows "\<^bold>\<lambda>f. f`(inr(\<^bold>\<lambda>a. f`(inl a))): \<not>(\<not>(A + \<not>A))"
-by (derive lems: assms)
-
-
-end
-- 
cgit v1.2.3