From f988d541364841cd208f4fd21ff8e5e2935fc7aa Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 24 Jun 2021 22:40:05 +0100
Subject: Bad practice huge commit: 1. Rudimentary prototype definitional
 package 2. Started univalence 3. Various compatibility fixes and new theory
 stubs 4. Updated ROOT file

---
 hott/Identity.thy | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'hott/Identity.thy')

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
-- 
cgit v1.2.3