diff options
Diffstat (limited to 'Sum.thy')
| -rw-r--r-- | Sum.thy | 62 |
1 files changed, 26 insertions, 36 deletions
@@ -1,69 +1,59 @@ -(* 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 :: "[Term, Typefam] \<Rightarrow> Term" and - pair :: "[Term, Term] \<Rightarrow> Term" ("(1<_,/ _>)") and - indSum :: "[[Term, Term] \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<Sum>)") + 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, Term, Term] \<Rightarrow> Term" ("(3\<Sum>_:_./ _)" 20) - "_SUM_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(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 :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) +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_form [form] lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_elim +lemmas Sum_comp [comp] end |