add Displayed.Section

agda · Sep 10, 2024 · d2ddec2 · d2ddec2
1 parent 6c10ddc
commit d2ddec2
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Cubical/Categories/Displayed/Section.agda b/Cubical/Categories/Displayed/Section.agda
@@ -0,0 +1,4 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Displayed.Section where
+
+open import Cubical.Categories.Displayed.Section.Base public