aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--hott/Equivalence.thy4
-rw-r--r--hott/Identity.thy77
-rw-r--r--hott/List_HoTT.thy2
3 files changed, 38 insertions, 45 deletions
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index 9fe11a7..745bc67 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -400,8 +400,8 @@ Lemma
by (eq p) (rule equivalence_refl)
text \<open>
- The following proof is wordy because (1) the typechecker doesn't normalize,
- and (2) we don't yet have universe level inference.
+ The following proof is wordy because (1) typechecker normalization is still
+ rudimentary, and (2) we don't yet have universe level inference.
\<close>
Lemma (def) equiv_if_equal:
diff --git a/hott/Identity.thy b/hott/Identity.thy
index caab2e3..0531b74 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -6,7 +6,7 @@ text \<open>
\<close>
theory Identity
-imports Spartan
+imports MLTT
begin
@@ -109,7 +109,7 @@ method pathcomp for p q :: o = rule pathcomp[where ?p=p and ?q=q]
section \<open>Notation\<close>
definition Id_i (infix "=" 110)
- where [implicit]: "Id_i x y \<equiv> x =\<^bsub>{}\<^esub> y"
+ where [implicit]: "x = y \<equiv> x =\<^bsub>{}\<^esub> y"
definition pathinv_i ("_\<inverse>" [1000])
where [implicit]: "pathinv_i p \<equiv> pathinv {} {} {} p"
@@ -532,47 +532,40 @@ method right_whisker = (rule right_whisker)
section \<open>Horizontal path-composition\<close>
-locale horiz_pathcomposable =
-\<comment> \<open>Conditions under which horizontal path-composition is defined.\<close>
-fixes
- i A a b c p q r s
-assumes [type]:
- "A: U i" "a: A" "b: A" "c: A"
- "p: a =\<^bsub>A\<^esub> b" "q: a =\<^bsub>A\<^esub> b"
- "r: b =\<^bsub>A\<^esub> c" "s: b =\<^bsub>A\<^esub> c"
+locale horiz_pathcomposable = \<comment> \<open>Conditions under which horizontal path-composition is defined.\<close>
+fixes i A a b c p q r s
+assumes [type]: "A: U i" "a: A" "b: A" "c: A"
+ "p: a =\<^bsub>A\<^esub> b" "q: a =\<^bsub>A\<^esub> b" "r: b =\<^bsub>A\<^esub> c" "s: b =\<^bsub>A\<^esub> c"
begin
-
-Lemma (def) horiz_pathcomp:
- assumes "\<alpha>: p = q" "\<beta>: r = s"
- shows "p \<bullet> r = q \<bullet> s"
-proof (rule pathcomp)
- show "p \<bullet> r = q \<bullet> r" by right_whisker fact
- show ".. = q \<bullet> s" by left_whisker fact
-qed typechk
-
-text \<open>A second horizontal composition:\<close>
-
-Lemma (def) horiz_pathcomp':
- assumes "\<alpha>: p = q" "\<beta>: r = s"
- shows "p \<bullet> r = q \<bullet> s"
-proof (rule pathcomp)
- show "p \<bullet> r = p \<bullet> s" by left_whisker fact
- show ".. = q \<bullet> s" by right_whisker fact
-qed typechk
-
-notation horiz_pathcomp (infix "\<star>" 121)
-notation horiz_pathcomp' (infix "\<star>''" 121)
-
-Lemma (def) horiz_pathcomp_eq_horiz_pathcomp':
- assumes "\<alpha>: p = q" "\<beta>: r = s"
- shows "\<alpha> \<star> \<beta> = \<alpha> \<star>' \<beta>"
- unfolding horiz_pathcomp_def horiz_pathcomp'_def
- apply (eq \<alpha>, eq \<beta>)
- focus vars p apply (eq p)
- focus vars a _ _ _ r by (eq r) (compute, refl)
- done
- done
-
+ Lemma (def) horiz_pathcomp:
+ assumes "\<alpha>: p = q" "\<beta>: r = s" shows "p \<bullet> r = q \<bullet> s"
+ proof (rule pathcomp)
+ show "p \<bullet> r = q \<bullet> r" by right_whisker fact
+ show ".. = q \<bullet> s" by left_whisker fact
+ qed typechk
+
+ Lemma (def) horiz_pathcomp':
+ assumes "\<alpha>: p = q" "\<beta>: r = s" shows "p \<bullet> r = q \<bullet> s"
+ proof (rule pathcomp)
+ show "p \<bullet> r = p \<bullet> s" by left_whisker fact
+ show ".. = q \<bullet> s" by right_whisker fact
+ qed typechk
+
+ notation horiz_pathcomp (infix "\<star>" 121)
+ notation horiz_pathcomp' (infix "\<star>''" 121)
+
+ Lemma (def) horiz_pathcomp_eq_horiz_pathcomp':
+ assumes "\<alpha>: p = q" "\<beta>: r = s" shows "\<alpha> \<star> \<beta> = \<alpha> \<star>' \<beta>"
+ unfolding horiz_pathcomp_def horiz_pathcomp'_def
+ proof (eq \<alpha>, eq \<beta>)
+ fix p q assuming "p: a = b" "q: b = c"
+ show "refl p \<bullet>\<^sub>r q \<bullet> (p \<bullet>\<^sub>l refl q) = p \<bullet>\<^sub>l refl q \<bullet> (refl p \<bullet>\<^sub>r q)"
+ proof (eq p)
+ fix a r assuming "a: A" "r: a = c"
+ show "refl (refl a) \<bullet>\<^sub>r r \<bullet> (refl a \<bullet>\<^sub>l refl r) = refl a \<bullet>\<^sub>l refl r \<bullet> (refl (refl a) \<bullet>\<^sub>r r)"
+ by (eq r) (compute, refl)
+ qed
+ qed
end
diff --git a/hott/List_HoTT.thy b/hott/List_HoTT.thy
index 9bd1517..d866f59 100644
--- a/hott/List_HoTT.thy
+++ b/hott/List_HoTT.thy
@@ -1,6 +1,6 @@
theory List_HoTT
imports
- Spartan.List
+ MLTT.List
Nat
begin