Implementing univalence

1 files changed, 5 insertions, 0 deletions

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