From 76ac8ed82317f3f62f26ecc88f412c61004bcffa Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 17 Sep 2018 13:13:55 +0200
Subject: Reorganizing theories

---
 Sum.thy | 57 +++++++++++++++++++++++----------------------------------
 1 file changed, 23 insertions(+), 34 deletions(-)

(limited to 'Sum.thy')

diff --git a/Sum.thy b/Sum.thy
index 92375b9..422e01b 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -1,69 +1,58 @@
-(*  Title:  HoTT/Sum.thy
-    Author: Josh Chen
+(*
+Title:  Sum.thy
+Author: Joshua Chen
+Date:   2018
 
 Dependent sum type
 *)
 
 theory Sum
-  imports HoTT_Base
-begin
+imports HoTT_Base
 
+begin
 
-section \<open>Constants and syntax\<close>
 
 axiomatization
-  Sum :: "[t, Typefam] \<Rightarrow> t" and
-  pair :: "[t, t] \<Rightarrow> t"  ("(1<_,/ _>)") and
+  Sum    :: "[t, tf] \<Rightarrow> t" and
+  pair   :: "[t, t] \<Rightarrow> t"  ("(1<_,/ _>)") and
   indSum :: "[[t, t] \<Rightarrow> t, t] \<Rightarrow> t"  ("(1ind\<^sub>\<Sum>)")
 
 syntax
-  "_SUM" :: "[idt, t, t] \<Rightarrow> t"        ("(3\<Sum>_:_./ _)" 20)
-  "_SUM_ASCII" :: "[idt, t, t] \<Rightarrow> t"  ("(3SUM _:_./ _)" 20)
+  "_sum" :: "[idt, t, t] \<Rightarrow> t"        ("(3\<Sum>_:_./ _)" 20)
+  "_sum_ascii" :: "[idt, t, t] \<Rightarrow> t"  ("(3SUM _:_./ _)" 20)
 
 translations
   "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)"
   "SUM x:A. B" \<rightharpoonup> "CONST Sum A (\<lambda>x. B)"
 
-text "Nondependent pair."
-
 abbreviation Pair :: "[t, t] \<Rightarrow> t"  (infixr "\<times>" 50)
   where "A \<times> B \<equiv> \<Sum>_:A. B"
 
+axiomatization where
+\<comment> \<open>Type rules\<close>
 
-section \<open>Type rules\<close>
+  Sum_form: "\<lbrakk>A: U i; B: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x: U i" and
+
+  Sum_intro: "\<lbrakk>B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> <a,b>: \<Sum>x:A. B x" and
 
-axiomatization where
-  Sum_form: "\<lbrakk>A: U i; B: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x: U i"
-and
-  Sum_intro: "\<lbrakk>B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> <a,b>: \<Sum>x:A. B x"
-and
   Sum_elim: "\<lbrakk>
     p: \<Sum>x:A. B x;
-    \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x,y>;
-    C: \<Sum>x:A. B x \<longrightarrow> U i
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> f p: C p"  (* What does writing \<lambda>x y. f(x, y) change? *)
-and
+    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> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> (\<lambda>x y. f x y) p: C p" and
+
   Sum_comp: "\<lbrakk>
     a: A;
     b: B a;
-    \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f x y: C <x,y>;
     B: A \<longrightarrow> U i;
-    C: \<Sum>x:A. B x \<longrightarrow> U i
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> f <a,b> \<equiv> f a b"
-
-text "Admissible inference rules for sum formation:"
-
-axiomatization where
-  Sum_wellform1: "(\<Sum>x:A. B x: U i) \<Longrightarrow> A: U i"
-and
-  Sum_wellform2: "(\<Sum>x:A. B x: U i) \<Longrightarrow> 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> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> (\<lambda>x y. f x y) <a,b> \<equiv> f a b" and
 
+\<comment> \<open>Congruence rules\<close>
 
-text "Rule attribute declarations:"
+  Sum_form_eq: "\<lbrakk>A: U i; B: A \<longrightarrow> U i; C: A \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> B x \<equiv> C x\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x \<equiv> \<Sum>x:A. C x"
 
-lemmas Sum_comp [comp]
-lemmas Sum_wellform [wellform] = Sum_wellform1 Sum_wellform2
 lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_elim
+lemmas Sum_comp [comp]
 
 
 end
-- 
cgit v1.2.3