diff options
| author | Josh Chen | 2021-06-24 22:40:05 +0100 |
|---|---|---|
| committer | Josh Chen | 2021-06-24 22:40:05 +0100 |
| commit | f988d541364841cd208f4fd21ff8e5e2935fc7aa (patch) | |
| tree | 8ccc4d4e4cdde7572453ac0e250a224fe8db3da1 /hott/Identity.thy | |
| parent | 0085798a86a35e2430a97289e894724f688db435 (diff) | |
Bad practice huge commit:
1. Rudimentary prototype definitional package
2. Started univalence
3. Various compatibility fixes and new theory stubs
4. Updated ROOT file
Diffstat (limited to 'hott/Identity.thy')
| -rw-r--r-- | hott/Identity.thy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/hott/Identity.thy b/hott/Identity.thy index 9ae0894..ce0e0ec 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -259,16 +259,16 @@ section \<open>Transport\<close> Lemma (def) transport: assumes "A: U i" - "\<And>x. x: A \<Longrightarrow> P x: U i" "x: A" "y: A" "p: x = y" + "\<And>x. x: A \<Longrightarrow> P x: U i" shows "P x \<rightarrow> P y" by (eq p) intro definition transport_i ("transp") - where [implicit]: "transp P p \<equiv> transport {} P {} {} p" + where [implicit]: "transp P p \<equiv> transport {} {} {} p P" -translations "transp P p" \<leftharpoondown> "CONST transport A P x y p" +translations "transp P p" \<leftharpoondown> "CONST transport A x y p P" Lemma transport_comp [comp]: assumes |