split cumulative hierarchy

agda · Oct 2, 2020 · 37c526c · 37c526c
1 parent 8097c1a
commit 37c526c
Show file tree

Hide file tree

Showing 4 changed files with 504 additions and 441 deletions.
diff --git a/Cubical/HITs/CumulativeHierarchy.agda b/Cubical/HITs/CumulativeHierarchy.agda
@@ -0,0 +1,6 @@
+{-# OPTIONS --cubical --no-import-sorts --safe #-}
+module Cubical.HITs.CumulativeHierarchy where
+
+open import Cubical.HITs.CumulativeHierarchy.Base public
+open import Cubical.HITs.CumulativeHierarchy.Properties public
+open import Cubical.HITs.CumulativeHierarchy.Constructions public