From 637ee546f3eb9a927d83bd19ae0bee09031bd7d5 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 11 Sep 2018 10:20:26 +0200
Subject: Implementing univalence

---
 Prod.thy | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'Prod.thy')

diff --git a/Prod.thy b/Prod.thy
index 35d6b07..a7968b6 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -81,4 +81,9 @@ syntax "_COMPOSE" :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<circ>" 110)
 translations "g \<circ> f" \<rightleftharpoons> "g o f"
 
 
+section \<open>Polymorphic identity function\<close>
+
+abbreviation id :: Term where "id \<equiv> \<^bold>\<lambda>x. x"
+
+
 end
-- 
cgit v1.2.3