aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Coprod.thy2
-rw-r--r--EqualProps.thy4
-rw-r--r--ProdProps.thy2
-rw-r--r--Sum.thy2
-rw-r--r--Unit.thy2
-rw-r--r--Univalence.thy4
6 files changed, 9 insertions, 7 deletions
diff --git a/Coprod.thy b/Coprod.thy
index b87958a..1ff7361 100644
--- a/Coprod.thy
+++ b/Coprod.thy
@@ -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:
diff --git a/Sum.thy b/Sum.thy
index 6de20fd..aac81f7 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -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"
diff --git a/Unit.thy b/Unit.thy
index 9b86739..6760f27 100644
--- a/Unit.thy
+++ b/Unit.thy
@@ -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"