codata

Author: aljungstrom

Cubical/Codata/Everything.agda

@@ -0,0 +1,18 @@
+{-# OPTIONS --guardedness #-}
+module Cubical.Codata.Everything where
+
+import Cubical.Codata.Conat
+import Cubical.Codata.Conat.Bounded
+import Cubical.Codata.M.Coalg
+import Cubical.Codata.M.Coalg.Base
+import Cubical.Codata.M.Container
+import Cubical.Codata.Containers.Coalgebras
+import Cubical.Codata.Containers.CoinductiveContainers
+import Cubical.Codata.M.MRecord
+import Cubical.Codata.M.M
+import Cubical.Codata.M.M.Base
+import Cubical.Codata.M.M.Properties
+import Cubical.Codata.M.helper
+import Cubical.Codata.M.itree
+import Cubical.Codata.M.stream
+import Cubical.Codata.Stream