diff options
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 |