Construction of extrusions

pthariensflame · May 6, 2024 · 925cd58 · 925cd58
1 parent 8c73dfd
commit 925cd58
Show file tree

Hide file tree

Showing 3 changed files with 466 additions and 4 deletions.
diff --git a/src/Algebra/Fumula/Construct.agda b/src/Algebra/Fumula/Construct.agda
@@ -9,7 +9,6 @@ open import Data.Product.Relation.Binary.Pointwise.NonDependent using (Pointwise
 open import Algebra.Fumula.Core
 open import Algebra.Fumula.Definitions
 open import Algebra.Fumula.Structures
-open import Algebra.Fumula.Bundles.Raw
 open import Algebra.Fumula.Bundles
 
 module Terminal {c ℓ} where
@@ -61,7 +60,7 @@ module Initial {c ℓ} where
     _≈_ : Rel Carrier ℓ
     _≈_ ()
 
-    infixl 7 _⤙_⤚_
+    infix 7 _⤙_⤚_
     _⤙_⤚_ : Op₃ Carrier
     _⤙_⤚_ ()
 
@@ -98,7 +97,9 @@ module Initial {c ℓ} where
   reversibleAlmostFumula = record { isReversibleAlmostFumula = isReversibleAlmostFumula }
 
   open Terminal {c} {ℓ} public
-    hiding (rawAlmostFumula; isEquivalence; isAlmostFumula; almostFumula; isReversibleAlmostFumula; reversibleAlmostFumula)
+    hiding (module 𝕆ne; rawAlmostFumula; isEquivalence;
+           isAlmostFumula; almostFumula;
+           isReversibleAlmostFumula; reversibleAlmostFumula)
 
 module Reverse where
 

diff --git a/src/Algebra/Fumula/Extrusion.agda b/src/Algebra/Fumula/Extrusion.agda
@@ -9,7 +9,7 @@ open import Algebra.Fumula.Extrusion.Definitions public
 open import Algebra.Fumula.Extrusion.Structures public
 open import Algebra.Fumula.Extrusion.Bundles public
 open import Algebra.Fumula.Extrusion.Properties public
--- open import Algebra.Fumula.Extrusion.Construct public
+open import Algebra.Fumula.Extrusion.Construct public
 -- open import Algebra.Fumula.Extrusion.Morphism public
 -- open import Algebra.Fumula.Extrusion.Morphism.Construct public
 open import Algebra.Fumula.Extrusion.Convert public