Partway through changing function application syntax style.

7 files changed, 206 insertions, 138 deletions

diff --git a/HoTT.thy b/HoTT.thy
index fa50f61..ce77ec7 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -12,9 +12,11 @@ HoTT_Base
 HoTT_Methods
 
 (* Types *)
-Equal
 Prod
 Sum
+Equal
+Coprod
+Nat
 
 (* Additional properties *)
 EqualProps
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index cf71813..c2bb092 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -9,6 +9,10 @@ theory HoTT_Base
   imports Pure
 begin
 
+text "Use the syntax \<open>f(x)\<close> instead of \<open>f x\<close> for function application."
+
+setup Pure_Thy.old_appl_syntax_setup
+
 
 section \<open>Foundational definitions\<close>
 
@@ -20,12 +24,12 @@ typedecl Term
 section \<open>Judgments\<close>
 
 text "
-  Formalize the typing judgment \<open>a : A\<close>.
+  Formalize the typing judgment \<open>a: A\<close>.
   For judgmental/definitional equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it.
 "
 
 consts
-  has_type :: "[Term, Term] \<Rightarrow> prop"  ("(1_ : _)" [0, 0] 1000)
+  has_type :: "[Term, Term] \<Rightarrow> prop"  ("(1_: _)" [0, 0] 1000)
 
 
 section \<open>Universe hierarchy\<close>
@@ -39,11 +43,11 @@ axiomatization
   S :: "Ord \<Rightarrow> Ord"  ("S_" [0] 1000) and
   lt :: "[Ord, Ord] \<Rightarrow> prop"  (infix "<-" 999)
 where
-  Ord_lt_min: "\<And>n. O <- S n"
+  Ord_min: "\<And>n. O <- S(n)"
 and
-  Ord_lt_trans: "\<And>m n. m <- n \<Longrightarrow> S m <- S n"
+  Ord_monotone: "\<And>m n. m <- n \<Longrightarrow> S(m) <- S(n)"
 
-lemmas Ord_rules [intro] = Ord_lt_min Ord_lt_trans
+lemmas Ord_rules [intro] = Ord_min Ord_monotone
   \<comment> \<open>Enables \<open>standard\<close> to automatically solve inequalities.\<close>
 
 text "Define the universe types."
@@ -51,12 +55,11 @@ text "Define the universe types."
 axiomatization
   U :: "Ord \<Rightarrow> Term"
 where
-  U_hierarchy: "\<And>i j. i <- j \<Longrightarrow> U(i) : U(j)"
+  U_hierarchy: "\<And>i j. i <- j \<Longrightarrow> U(i): U(j)"
 and
-  U_cumulative: "\<And>A i j. \<lbrakk>A : U(i); i <- j\<rbrakk> \<Longrightarrow> A : U(j)"
+  U_cumulative: "\<And>A i j. \<lbrakk>A: U(i); i <- j\<rbrakk> \<Longrightarrow> A: U(j)"
     \<comment> \<open>WARNING: \<open>rule Universe_cumulative\<close> can result in an infinite rewrite loop!\<close>
 
-
 section \<open>Type families\<close>
 
 text "
@@ -64,7 +67,7 @@ text "
 "
 
 abbreviation (input) constrained :: "[Term \<Rightarrow> Term, Term, Term] \<Rightarrow> prop"  ("(1_: _ \<longrightarrow> _)")
-  where "f: A \<longrightarrow> B \<equiv> (\<And>x. x : A \<Longrightarrow> f x : B)"
+  where "f: A \<longrightarrow> B \<equiv> (\<And>x. x : A \<Longrightarrow> f(x): B)"
 
 text "
   The above is used to define type families, which are constrained meta-lambdas \<open>P: A \<longrightarrow> B\<close> where \<open>A\<close> and \<open>B\<close> are small types.
diff --git a/Nat.thy b/Nat.thy
new file mode 100644
index 0000000..93b7a2e
--- /dev/null
+++ b/Nat.thy
@@ -0,0 +1,49 @@
+(*  Title:  HoTT/Nat.thy
+    Author: Josh Chen
+    Date:   Aug 2018
+
+Natural numbers.
+*)
+
+theory Nat
+  imports HoTT_Base
+begin
+
+
+axiomatization
+  Nat :: Term   ("\<nat>") and
+  zero :: Term  ("0") and
+  succ :: "Term \<Rightarrow> Term" and
+  indNat :: "[Typefam, [Term, Term] \<Rightarrow> Term, Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>\<nat>)")
+where
+  Nat_form: "\<nat> : U(O)"
+and
+  Nat_intro1: "0 : \<nat>"
+and
+  Nat_intro2: "\<And>n. n : \<nat> \<Longrightarrow> succ n : \<nat>"
+and
+  Nat_elim: "\<And>i C f a n. \<lbrakk>
+    C: \<nat> \<longrightarrow> U(i);
+    \<And>n c. \<lbrakk>n : \<nat>; c : C n\<rbrakk> \<Longrightarrow> f n c : C (succ n);
+    a : C 0;
+    n : \<nat>
+    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> C f a n : C n"
+and
+  Nat_comp1: "\<And>i C f a. \<lbrakk>
+    C: \<nat> \<longrightarrow> U(i);
+    \<And>n c. \<lbrakk>n : \<nat>; c : C n\<rbrakk> \<Longrightarrow> f n c : C (succ n);
+    a : C 0
+    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> C f a 0 \<equiv> a"
+and
+  Nat_comp2: "\<And> i C f a n. \<lbrakk>
+    C: \<nat> \<longrightarrow> U(i);
+    \<And>n c. \<lbrakk>n : \<nat>; c : C n\<rbrakk> \<Longrightarrow> f n c : C (succ n);
+    a : C 0;
+    n : \<nat>
+    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> C f a (succ n) \<equiv> f n (ind\<^sub>\<nat> C f a n)"
+
+lemmas Nat_rules [intro] = Nat_form Nat_intro1 Nat_intro2 Nat_elim Nat_comp1 Nat_comp2
+lemmas Nat_comps [comp] = Nat_comp1 Nat_comp2
+
+
+end
\ No newline at end of file
diff --git a/Prod.thy b/Prod.thy
index 8fa73f3..e4e7091 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -15,7 +15,7 @@ section \<open>Constants and syntax\<close>
 axiomatization
   Prod :: "[Term, Typefam] \<Rightarrow> Term" and
   lambda :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and
-  appl :: "[Term, Term] \<Rightarrow> Term"  (infixl "`" 60)
+  appl :: "[Term, Term] \<Rightarrow> Term"  ("(1_`_)" [61, 60] 60)
     \<comment> \<open>Application binds tighter than abstraction.\<close>
 
 syntax
@@ -27,48 +27,48 @@ syntax
 text "The translations below bind the variable \<open>x\<close> in the expressions \<open>B\<close> and \<open>b\<close>."
 
 translations
-  "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)"
-  "\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda A (\<lambda>x. b)"
-  "PROD x:A. B" \<rightharpoonup> "CONST Prod A (\<lambda>x. B)"
-  "%%x:A. b" \<rightharpoonup> "CONST lambda A (\<lambda>x. b)"
+  "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod(A, \<lambda>x. B)"
+  "\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda(A, \<lambda>x. b)"
+  "PROD x:A. B" \<rightharpoonup> "CONST Prod(A, \<lambda>x. B)"
+  "%%x:A. b" \<rightharpoonup> "CONST lambda(A, \<lambda>x. b)"
 
 text "Nondependent functions are a special case."
 
 abbreviation Function :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<rightarrow>" 40)
-  where "A \<rightarrow> B \<equiv> \<Prod>_:A. B"
+  where "A \<rightarrow> B \<equiv> \<Prod>_: A. B"
 
 
 section \<open>Type rules\<close>
 
 axiomatization where
-  Prod_form: "\<And>i A B. \<lbrakk>A : U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x : U(i)"
+  Prod_form: "\<And>i A B. \<lbrakk>A: U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x): U(i)"
 and
-  Prod_intro: "\<And>i A B b. \<lbrakk>A : U(i); \<And>x. x : A \<Longrightarrow> b x : B x\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x:A. b x : \<Prod>x:A. B x"
+  Prod_intro: "\<And>i A B b. \<lbrakk>A: U(i); B: A \<longrightarrow> U(i); \<And>x. x: A \<Longrightarrow> b(x): B(x)\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x:A. b(x): \<Prod>x:A. B(x)"
 and
-  Prod_elim: "\<And>A B f a. \<lbrakk>f : \<Prod>x:A. B x; a : A\<rbrakk> \<Longrightarrow> f`a : B a"
+  Prod_elim: "\<And>A B f a. \<lbrakk>f: \<Prod>x:A. B(x); a: A\<rbrakk> \<Longrightarrow> f`a: B(a)"
 and
-  Prod_comp: "\<And>A B b a. \<lbrakk>\<And>x. x : A \<Longrightarrow> b x : B x; a : A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> b a"
+  Prod_comp: "\<And>i A B b a. \<lbrakk>A: U(i); B: A \<longrightarrow> U(i); \<And>x. x: A \<Longrightarrow> b(x): B(x); a: A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b(x))`a \<equiv> b(a)"
 and
-  Prod_uniq: "\<And>A B f. f : \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
+  Prod_uniq: "\<And>A B f. f : \<Prod>x:A. B(x) \<Longrightarrow> \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
 
 text "
   Note that the syntax \<open>\<^bold>\<lambda>\<close> (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation).
 "
 
 text "
-  In addition to the usual type rules, it is a meta-theorem (*PROVE THIS!*) that whenever \<open>\<Prod>x:A. B x : U(i)\<close> is derivable from some set of premises \<Gamma>, then so are \<open>A : U(i)\<close> and \<open>B: A \<longrightarrow> U(i)\<close>.
+  In addition to the usual type rules, it is a meta-theorem (*PROVE THIS!*) that whenever \<open>\<Prod>x:A. B x: U(i)\<close> is derivable from some set of premises \<Gamma>, then so are \<open>A: U(i)\<close> and \<open>B: A \<longrightarrow> U(i)\<close>.
   
   That is to say, the following inference rules are admissible, and it simplifies proofs greatly to axiomatize them directly.
 "
 
 axiomatization where
-  Prod_form_cond1: "\<And>i A B. (\<Prod>x:A. B x : U(i)) \<Longrightarrow> A : U(i)"
+  Prod_form_cond1: "\<And>i A B. (\<Prod>x:A. B(x): U(i)) \<Longrightarrow> A: U(i)"
 and
-  Prod_form_cond2: "\<And>i A B. (\<Prod>x:A. B x : U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)"
+  Prod_form_cond2: "\<And>i A B. (\<Prod>x:A. B(x): U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)"
 
 text "Set up the standard reasoner to use the type rules:"
 
-lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq
+lemmas Prod_rules = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq
 lemmas Prod_form_conds [intro (*elim, wellform*)] = Prod_form_cond1 Prod_form_cond2
 lemmas Prod_comps [comp] = Prod_comp Prod_uniq
 
@@ -84,9 +84,9 @@ where
 and
   Unit_intro: "\<star> : \<one>"
 and
-  Unit_elim: "\<And>i C c a. \<lbrakk>C: \<one> \<longrightarrow> U(i); c : C \<star>; a : \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> C c a : C a"
+  Unit_elim: "\<And>i C c a. \<lbrakk>C: \<one> \<longrightarrow> U(i); c : C(\<star>); a : \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(C, c, a) : C(a)"
 and
-  Unit_comp: "\<And>i C c. \<lbrakk>C: \<one> \<longrightarrow> U(i); c : C \<star>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> C c \<star> \<equiv> c"
+  Unit_comp: "\<And>i C c. \<lbrakk>C: \<one> \<longrightarrow> U(i); c : C(\<star>)\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(C, c, \<star>) \<equiv> c"
 
 lemmas Unit_rules [intro] = Unit_form Unit_intro Unit_elim Unit_comp
 lemmas Unit_comps [comp] = Unit_comp
diff --git a/Proj.thy b/Proj.thy
index bcef939..e6ed0bb 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -52,6 +52,7 @@ unfolding fst_dep_def
 proof
   show "lambda (Sum A B) (ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x)) : (\<Sum>x:A. B x) \<rightarrow> A"
   proof
+    show "A : U(i)" using assms(1) ..
     show "Sum A B : U(i)" by (rule assms)
     show "\<And>p. p : Sum A B \<Longrightarrow> ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x) p : A"
     proof
@@ -66,11 +67,11 @@ lemma fst_dep_comp:
   shows "fst[A,B]`(a,b) \<equiv> a"
 unfolding fst_dep_def
 proof (subst comp)
+  show "Sum A B : U(i)" using assms(1-2) ..
   show "\<And>x. x : Sum A B \<Longrightarrow> ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x) x : A" by (standard, rule assms(1), assumption+)
-  show "(a,b) : Sum A B" using assms(2-4) ..
-  show "ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x) (a, b) \<equiv> a"
-  proof
-    oops
+  show "(a,b) : Sum A B" using assms ..
+  show "ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x) (a, b) \<equiv> a" by (standard, (rule assms|assumption)+)
+qed (rule assms)
 
 \<comment> \<open> (* Old proof *)
 proof -
@@ -101,8 +102,23 @@ qed
 lemma snd_dep_type:
   assumes "\<Sum>x:A. B x : U(i)" and "p : \<Sum>x:A. B x"
   shows "snd[A,B]`p : B (fst[A,B]`p)"
-  unfolding fst_dep_def snd_dep_def
-  by (simplify lems: assms)
+unfolding fst_dep_def snd_dep_def
+proof (subst (3) comp)
+  show "Sum A B : U(i)" by (rule assms)
+  show "\<And>x. x : Sum A B \<Longrightarrow> ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x) x : A"
+  proof
+    show "A : U(i)" using assms(1) ..
+  qed
+  show "A : U(i)" using assms(1) ..
+  show "p : Sum A B" by (rule assms(2))
+  show "lambda
+          (Sum A B)
+          (ind\<^sub>\<Sum>[A, B] (\<lambda>q. B (lambda (Sum A B) (ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x))`q)) (\<lambda>x y. y))
+        ` p : B (ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x) p)"
+  proof (subst (2) comp)
+    show "Sum A B : U(i)" by (rule assms)
+    show "
+  
 
 \<comment> \<open> (* Old proof *)
 proof (derive lems: assms unfolds: snd_dep_def)
diff --git a/Sum.thy b/Sum.thy
index 80f8a9c..18d4186 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -36,7 +36,7 @@ section \<open>Type rules\<close>
 axiomatization where
   Sum_form: "\<And>i A B. \<lbrakk>A : U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x : U(i)"
 and
-  Sum_intro: "\<And>i A B a b. \<lbrakk>B: A \<longrightarrow> U(i); a : A; b : B a\<rbrakk> \<Longrightarrow> (a,b) : \<Sum>x:A. B x"
+  Sum_intro: "\<And>i A B a b. \<lbrakk>A : U(i); B: A \<longrightarrow> U(i); a : A; b : B a\<rbrakk> \<Longrightarrow> (a,b) : \<Sum>x:A. B x"
 and
   Sum_elim: "\<And>i A B C f p. \<lbrakk>
     C: \<Sum>x:A. B x \<longrightarrow> U(i);
@@ -45,6 +45,8 @@ and
     \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>[A,B] C f p : C p"
 and
   Sum_comp: "\<And>i A B C f a b. \<lbrakk>
+    A : U(i);
+    B: A \<longrightarrow> U(i);
     C: \<Sum>x:A. B x \<longrightarrow> U(i);
     \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> f x y : C (x,y);
     a : A;
@@ -63,17 +65,17 @@ lemmas Sum_form_conds [intro (*elim, wellform*)] = Sum_form_cond1 Sum_form_cond2
 lemmas Sum_comps [comp] = Sum_comp
 
 
-section \<open>Null type\<close>
+section \<open>Empty type\<close>
 
 axiomatization
-  Null :: Term  ("\<zero>") and
-  indNull :: "[Typefam, Term] \<Rightarrow> Term"  ("(1ind\<^sub>\<zero>)")
+  Empty :: Term  ("\<zero>") and
+  indEmpty :: "[Typefam, Term] \<Rightarrow> Term"  ("(1ind\<^sub>\<zero>)")
 where
-  Null_form: "\<zero> : U(O)"
+  Empty_form: "\<zero> : U(O)"
 and
-  Null_elim: "\<And>i C z. \<lbrakk>C: \<zero> \<longrightarrow> U(i); z : \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> C z : C z"
+  Empty_elim: "\<And>i C z. \<lbrakk>C: \<zero> \<longrightarrow> U(i); z : \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> C z : C z"
 
-lemmas Null_rules [intro] = Null_form Null_elim
+lemmas Empty_rules [intro] = Empty_form Empty_elim
 
 
 end
\ No newline at end of file
diff --git a/scratch.thy b/scratch.thy
index ae1bdb5..b88a8fc 100644
--- a/scratch.thy
+++ b/scratch.thy
@@ -3,108 +3,104 @@ theory scratch
 
 begin
 
-(* Typechecking *)
-schematic_goal "\<lbrakk>A : U(i); B : U(i); a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : ?A"
-  by derive
-
-lemma "\<zero> : U(S S S 0)"
-  by derive
-
-
-(* Simplification *)
-
-notepad begin
-
-assume asm:
-  "f`a \<equiv> g"
-  "g`b \<equiv> \<^bold>\<lambda>x:A. d"
-  "c : A"
-  "d : B"
-
-have "f`a`b`c \<equiv> d" by (simplify lems: asm)
-
-end
-
-lemma "\<lbrakk>A : U(i); a : A\<rbrakk> \<Longrightarrow> indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a) \<equiv> refl(a)"
-  by simplify
-
-lemma "\<lbrakk>a : A; \<And>x. x : A \<Longrightarrow> b x : X\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> b a"
-  by simplify
-
-schematic_goal "\<lbrakk>a : A; b: A \<longrightarrow> X\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> ?x"
-  by rsimplify
-
-lemma
-  assumes "a : A" and "\<And>x. x : A \<Longrightarrow> b x : B x"
-  shows "(\<^bold>\<lambda>x:A. b x)`a \<equiv> b a"
-  by (simplify lems: assms)
-
-lemma "\<lbrakk>a : A; b : B a; B: A \<longrightarrow> U(i); \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y\<rbrakk>
-  \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b"
-  by (simplify)
-
-lemma
-  assumes
-    "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a \<equiv> \<^bold>\<lambda>y:B a. c a y"
-    "(\<^bold>\<lambda>y:B a. c a y)`b \<equiv> c a b"
-  shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b"
-by (simplify lems: assms)
-
-lemma
-assumes
-  "a : A"
-  "b : B a"
-  "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y"
-shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b"
-by (simplify lems: assms)
-
-lemma
-assumes
-  "a : A"
-  "b : B a"
-  "c : C a b"
-  "\<And>x y z. \<lbrakk>x : A; y : B x; z : C x y\<rbrakk> \<Longrightarrow> d x y z : D x y z"
-shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. \<^bold>\<lambda>z:C x y. d x y z)`a`b`c \<equiv> d a b c"
-by (simplify lems: assms)
-
-(* Polymorphic identity function *)
+abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n:\<nat>. (ind\<^sub>\<nat> (\<lambda>n. \<nat>) (\<lambda>n c. n) 0 n)"
+
+schematic_goal "?a : (pred`0) =\<^sub>\<nat> 0"
+apply (subst comp)
+apply (rule Nat_form)
+prefer 4 apply (subst comp)
+apply (rule Nat_form)
+apply assumption
+apply (rule Nat_intro1)
+apply (rule Equal_intro)
+apply (rule Nat_intro1)
+prefer 2 apply (rule Nat_elim)
+apply (rule Nat_form)
+apply assumption
+apply (rule Nat_intro1)
+apply assumption
+apply (rule Nat_form)
+done
+
+schematic_goal "?a : \<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n"
+apply (rule Prod_intro)
+apply (rule Nat_form)
+apply (subst comp)
+apply (rule Nat_form)
+prefer 2 apply (rule Nat_elim)
+apply (rule Nat_form)
+apply assumption
+apply (rule Nat_intro1)
+apply assumption
+apply (rule Nat_form)
+apply (rule Nat_intro2, assumption)
+apply (rule Equal_form)
+apply (rule Nat_form)
+apply (rule Nat_elim)
+apply (rule Nat_form)
+apply assumption
+apply (rule Nat_rules)+
+apply assumption+
+apply (subst comp)
+apply (rule Nat_form)
+prefer 2 apply (rule Nat_elim)
+defer
+apply (assumption | rule Nat_form Nat_intro1 Nat_intro2)+
+apply (subst Nat_comps)
+apply (assumption | rule Nat_form Nat_intro1 Nat_intro2)+
+apply (rule Equal_intro)
+apply assumption
+apply (rule Nat_form)
+done
+
+schematic_goal "?a : \<Sum>p:\<nat>\<rightarrow>\<nat>. \<Prod>n:\<nat>. (p`(succ n)) =\<^sub>\<nat> n"
+apply (rule Sum_intro)
+apply (rule Prod_form)
+apply (rule Nat_form)+
+apply (rule Prod_form)
+apply (rule Nat_form)
+apply (rule Equal_form)
+apply (rule Nat_form)
+apply (rule Prod_elim)
+apply assumption
+apply (elim Nat_intro2)
+apply assumption
+prefer 2 apply (rule Prod_intro)
+apply (rule Nat_form)
+prefer 3 apply (rule Prod_intro)
+apply (rule Nat_form)+
+prefer 3 apply (rule Nat_elim)
+back
+oops
 
-definition Id :: "Numeral \<Rightarrow> Term" where "Id n \<equiv> \<^bold>\<lambda>A:U(n). \<^bold>\<lambda>x:A. x"
 
-lemma assumes "A : U 0" and "x:A" shows "(Id 0)`A`x \<equiv> x" unfolding Id_def by (simplify lems: assms)
+(* Now try to derive pred directly *)
+schematic_goal "?a : \<Sum>pred:?A . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)"
+(* At some point need to perform induction *)
+apply (rule Sum_intro)
+defer
+apply (rule Sum_form)
+apply (rule Equal_form)
+apply (rule Nat_form)
+apply (rule Prod_elim)
+defer
+apply (rule Nat_intro1)+
+prefer 5 apply assumption
+prefer 4 apply (rule Prod_form)
+apply (rule Nat_form)+
+apply (rule Prod_form)
+apply (rule Nat_form)
+apply (rule Equal_form)
+apply (rule Nat_form)
+apply (rule Prod_elim)
+apply assumption
+apply (rule Nat_intro2)
+apply assumption+
+(* Now begins the hard part *)
+prefer 2 apply (rule Sum_rules)
+prefer 2 apply (rule Prod_rules)
 
 
-(* See if we can find path inverse *)
-schematic_goal "\<lbrakk>A : U(i); x : A; y : A\<rbrakk> \<Longrightarrow> ?x : x =\<^sub>A y \<rightarrow> y =\<^sub>A x"
-  apply (rule Prod_intro)
-  apply (rule Equal_elim)
-  back
-  back
-  back
-  back
-  back
-  back
-  back
-  defer
-  back
-  back
-  back
-  back
-  back
-  back
-  back
-  back
-  back
-  apply (rule Equal_form)
-  apply assumption+
-  defer
-  defer
-  apply assumption
-  defer
-  defer
-  apply (rule Equal_intro)
-  apply assumption+
-oops
 
 
 end
\ No newline at end of file