diff options
| -rw-r--r-- | Coprod.thy | 2 | ||||
| -rw-r--r-- | EqualProps.thy | 4 | ||||
| -rw-r--r-- | ProdProps.thy | 2 | ||||
| -rw-r--r-- | Sum.thy | 2 | ||||
| -rw-r--r-- | Unit.thy | 2 | ||||
| -rw-r--r-- | Univalence.thy | 4 |
6 files changed, 9 insertions, 7 deletions
@@ -28,7 +28,7 @@ and \<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" + \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d u: C u" and Coprod_comp_inl: "\<lbrakk> C: A + B \<longrightarrow> U i; diff --git a/EqualProps.thy b/EqualProps.thy index 4cfe280..5db8487 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -278,6 +278,8 @@ section \<open>Transport\<close> definition transport :: "Term \<Rightarrow> Term" where "transport p \<equiv> ind\<^sub>= (\<lambda>x. (\<^bold>\<lambda>x. x)) p" +text "Note that \<open>transport\<close> is a polymorphic function in our formulation." + lemma transport_type: assumes "A: U i" "P: A \<longrightarrow> U i" @@ -292,7 +294,5 @@ lemma transport_comp: shows "transport (refl x) \<equiv> id" unfolding transport_def by (derive lems: assms) -text "Note that in our formulation, \<open>transport\<close> is a polymorphic function!" - end diff --git a/ProdProps.thy b/ProdProps.thy index 47e386b..a68f79b 100644 --- a/ProdProps.thy +++ b/ProdProps.thy @@ -14,7 +14,7 @@ begin section \<open>Composition\<close> text " - The proof of associativity needs some guidance; it involves telling Isabelle to use the correct rule for \<Pi>-type definitional equality, and the correct substitutions in the subgoals thereafter. + The proof of associativity needs some guidance; it involves telling Isabelle to use the correct rule for \<Prod>-type definitional equality, and the correct substitutions in the subgoals thereafter. " lemma compose_assoc: @@ -47,7 +47,7 @@ and 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); + 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" @@ -16,7 +16,7 @@ axiomatization pt :: Term ("\<star>") and indUnit :: "[Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<one>)") where - Unit_form: "\<one>: U(O)" + Unit_form: "\<one>: U O" and Unit_intro: "\<star>: \<one>" and diff --git a/Univalence.thy b/Univalence.thy index 80325f3..8599ba7 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -15,6 +15,8 @@ begin section \<open>Homotopy and equivalence\<close> +text "We define polymorphic constants implementing the definitions of homotopy and equivalence." + axiomatization homotopic :: "[Term, Term] \<Rightarrow> Term" (infix "~" 100) where homotopic_def: "\<lbrakk> f: \<Prod>x:A. B x; @@ -166,7 +168,7 @@ proof qed -text "The univalence axiom:" +text "The univalence axiom." axiomatization univalence :: Term where ua: "univalence: isequiv idtoeqv" |