From 012916d1ad08edcb68b8be6251ba457c0c0783f0 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 7 Jun 2018 19:37:07 +0200
Subject: But also looser than Pair

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

diff --git a/HoTT.thy b/HoTT.thy
index c1c6e72..44f55e9 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -57,7 +57,7 @@ translations
   "%%x:A. b" \<rightharpoonup> "CONST lambda A (\<lambda>x. b)"
   (* The above syntax translations bind the x in the expressions B, b. *)
 
-abbreviation Function :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<rightarrow>" 80)
+abbreviation Function :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<rightarrow>" 40)
   where "A\<rightarrow>B \<equiv> \<Prod>_:A. B"
 
 axiomatization
-- 
cgit v1.2.3