From 2f63e165d696688f0fcc721289889a8baa00cc02 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 25 May 2020 16:27:37 +0200
Subject: slightly nicer homotopy proofs with calculations

---
 spartan/theories/Identity.thy | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'spartan/theories/Identity.thy')

diff --git a/spartan/theories/Identity.thy b/spartan/theories/Identity.thy
index 01bea46..3a982f6 100644
--- a/spartan/theories/Identity.thy
+++ b/spartan/theories/Identity.thy
@@ -41,7 +41,8 @@ axiomatization where
 lemmas
   [intros] = IdF IdI and
   [elims "?p" "?a" "?b"] = IdE and
-  [comps] = Id_comp
+  [comps] = Id_comp and
+  [refl] = IdI
 
 
 section \<open>Path induction\<close>
-- 
cgit v1.2.3