From 85fc133fa0d64c61c380fcecada8f8358ad4b773 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 1 Mar 2019 15:45:10 +0100
Subject: transport and homotopy

---
 Prod.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Prod.thy')

diff --git a/Prod.thy b/Prod.thy
index 0bd037d..2cb62e4 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -24,8 +24,8 @@ syntax
   "_lam"   :: "[idt, t, t] \<Rightarrow> t"  ("(2\<lambda>'(_: _')./ _)" 30)
   "_lam'"  :: "[idt, t, t] \<Rightarrow> t"  ("(2\<lambda>_: _./ _)" 30)
 translations
-  "\<Prod>(x: A). B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)"
   "\<Prod>x: A. B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)"
+  "\<Prod>(x: A). B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)"
   "\<lambda>(x: A). b" \<rightleftharpoons> "(CONST lam) A (\<lambda>x. b)"
   "\<lambda>x: A. b" \<rightleftharpoons> "(CONST lam) A (\<lambda>x. b)"
 
-- 
cgit v1.2.3

