From 80edbd08e13200d2c080ac281d19948bbbcd92e0 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 25 May 2020 17:09:54 +0200
Subject: Reorganize theory structure. In particular, the identity type moves
 out from under Spartan to HoTT. Spartan now only has Pi and Sigma.

---
 hott/Base.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'hott/Base.thy')

diff --git a/hott/Base.thy b/hott/Base.thy
index 2a4ff9c..610a373 100644
--- a/hott/Base.thy
+++ b/hott/Base.thy
@@ -1,5 +1,5 @@
 theory Base
-imports Spartan.Equivalence
+imports Equivalence
 
 begin
 
-- 
cgit v1.2.3