diff options
author | Josh Chen | 2018-09-18 11:39:40 +0200 |
---|---|---|
committer | Josh Chen | 2018-09-18 11:39:40 +0200 |
commit | a9588dfbd929fbc1b53a5c9b4f41fc5eb4ed4e46 (patch) | |
tree | ef21f4328214618f98ee465e92fb3308dfb786da /Coprod.thy | |
parent | a2bb39ee8002eccc04b0cdaa82143840e6ec2565 (diff) | |
parent | 6857e783fa5cb91f058be322a18fb9ea583f2aad (diff) |
Merge branch 'develop', ready for release 0.1.0
Diffstat (limited to '')
-rw-r--r-- | Coprod.thy | 67 |
1 files changed, 26 insertions, 41 deletions
@@ -1,65 +1,50 @@ -(* Title: HoTT/Coprod.thy - Author: Josh Chen +(* +Title: Coprod.thy +Author: Joshua Chen +Date: 2018 Coproduct type *) theory Coprod - imports HoTT_Base -begin +imports HoTT_Base +begin -section \<open>Constants and type rules\<close> axiomatization - Coprod :: "[Term, Term] \<Rightarrow> Term" (infixr "+" 50) and - inl :: "Term \<Rightarrow> Term" and - inr :: "Term \<Rightarrow> Term" and - indCoprod :: "[Term \<Rightarrow> Term, Term \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>+)") + Coprod :: "[t, t] \<Rightarrow> t" (infixr "+" 50) and + inl :: "t \<Rightarrow> t" and + inr :: "t \<Rightarrow> t" and + indCoprod :: "[t \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t" ("(1ind\<^sub>+)") where - Coprod_form: "\<lbrakk>A: U i; B: U i\<rbrakk> \<Longrightarrow> A + B: U i" -and - Coprod_intro_inl: "\<lbrakk>a: A; B: U i\<rbrakk> \<Longrightarrow> inl a: A + B" -and - Coprod_intro_inr: "\<lbrakk>b: B; A: U i\<rbrakk> \<Longrightarrow> inr b: A + B" -and + Coprod_form: "\<lbrakk>A: U i; B: U i\<rbrakk> \<Longrightarrow> A + B: U i" and + + Coprod_intro_inl: "\<lbrakk>a: A; B: U i\<rbrakk> \<Longrightarrow> inl a: A + B" and + + Coprod_intro_inr: "\<lbrakk>b: B; A: U i\<rbrakk> \<Longrightarrow> inr b: A + B" and + Coprod_elim: "\<lbrakk> + u: A + B; C: A + B \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> c x: C (inl x); - \<And>y. y: B \<Longrightarrow> d y: C (inr y); - u: A + B - \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d u: C u" -and + \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda> x. c x) (\<lambda>y. d y) u: C u" and + Coprod_comp_inl: "\<lbrakk> + a: A; C: A + B \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> c x: C (inl x); - \<And>y. y: B \<Longrightarrow> d y: C (inr y); - a: A - \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inl a) \<equiv> c a" -and + \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda>x. c x) (\<lambda>y. d y) (inl a) \<equiv> c a" and + Coprod_comp_inr: "\<lbrakk> + b: B; C: A + B \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> c x: C (inl x); - \<And>y. y: B \<Longrightarrow> d y: C (inr y); - b: B - \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inr b) \<equiv> d b" - - -text "Admissible formation inference rules:" - -axiomatization where - Coprod_wellform1: "A + B: U i \<Longrightarrow> A: U i" -and - Coprod_wellform2: "A + B: U i \<Longrightarrow> B: U i" - - -text "Rule attribute declarations:" - -lemmas Coprod_intro = Coprod_intro_inl Coprod_intro_inr + \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda>x. c x) (\<lambda>y. d y) (inr b) \<equiv> d b" +lemmas Coprod_form [form] +lemmas Coprod_routine [intro] = Coprod_form Coprod_intro_inl Coprod_intro_inr Coprod_elim lemmas Coprod_comp [comp] = Coprod_comp_inl Coprod_comp_inr -lemmas Coprod_wellform [wellform] = Coprod_wellform1 Coprod_wellform2 -lemmas Coprod_routine [intro] = Coprod_form Coprod_intro Coprod_elim end |