diff options
Diffstat (limited to '')
-rw-r--r-- | ProdProps.thy | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/ProdProps.thy b/ProdProps.thy new file mode 100644 index 0000000..7c2c658 --- /dev/null +++ b/ProdProps.thy @@ -0,0 +1,54 @@ +(* Title: HoTT/ProdProps.thy + Author: Josh Chen + Date: Aug 2018 + +Properties of the dependent product. +*) + +theory ProdProps + imports + HoTT_Methods + Prod +begin + + +section \<open>Composition\<close> + +text " + The following rule is admissible, but we cannot derive it only using the rules for the \<Pi>-type. +" + +lemma compose_comp': "\<lbrakk> + A: U(i); + \<And>x. x: A \<Longrightarrow> b(x): B; + \<And>x. x: B \<Longrightarrow> c(x): C(x) + \<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. c(x)) \<circ> (\<^bold>\<lambda>x. b(x)) \<equiv> \<^bold>\<lambda>x. c(b(x))" +oops + +text "However we can derive a variant with more explicit premises:" + +lemma compose_comp2: + assumes + "A: U(i)" "B: U(i)" and + "C: B \<longrightarrow> U(i)" and + "\<And>x. x: A \<Longrightarrow> b(x): B" and + "\<And>x. x: B \<Longrightarrow> c(x): C(x)" + shows "(\<^bold>\<lambda>x. c(x)) \<circ> (\<^bold>\<lambda>x. b(x)) \<equiv> \<^bold>\<lambda>x. c(b(x))" +proof (subst (0) comp) + show "\<^bold>\<lambda>x. (\<^bold>\<lambda>u. c(u))`((\<^bold>\<lambda>v. b(v))`x) \<equiv> \<^bold>\<lambda>x. c(b(x))" + proof (subst (0) comp) + show "\<^bold>\<lambda>x. c((\<^bold>\<lambda>v. b(v))`x) \<equiv> \<^bold>\<lambda>x. c(b(x))" + proof - + have *: "\<And>x. x: A \<Longrightarrow> (\<^bold>\<lambda>v. b(v))`x \<equiv> b(x)" by simple (rule assms) + show "\<^bold>\<lambda>x. c((\<^bold>\<lambda>v. b(v))`x) \<equiv> \<^bold>\<lambda>x. c(b(x))" + proof (subst *) + + +text "We can show associativity of composition in general." + +lemma compose_assoc: + "(f \<circ> g) \<circ> h \<equiv> f \<circ> (g \<circ> h)" +proof + + +end
\ No newline at end of file |