Skip to content

Commit

Permalink
Extrusion raw bundles
Browse files Browse the repository at this point in the history 
Also naming simplifications
  • Loading branch information
@pthariensflame
pthariensflame committed Jun 7, 2024
1 parent 5eed4d4 commit e9c8f9f
Show file tree
Hide file tree
Showing 5 changed files with 304 additions and 27 deletions.
110 changes: 95 additions & 15 deletions src/Algebra/Fumula/Extrusion/Bundles.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ open import Algebra.Fumula.Bundles
open import Algebra.Fumula.Extrusion.Core
open import Algebra.Fumula.Extrusion.Definitions
open import Algebra.Fumula.Extrusion.Structures
open import Algebra.Fumula.Extrusion.Bundles.Raw public

private
variable
Expand All @@ -35,6 +36,13 @@ module _ (F : AlmostFumula f ℓf) where
setoid : Setoid x ℓx
setoid = record { isEquivalence = isEquivalence }

rawLeftAlmostFumulaExtrusion : RawLeftAlmostFumulaExtrusion F.rawAlmostFumula x ℓx
rawLeftAlmostFumulaExtrusion = record
{ Carrier = Carrier
; _≈_ = _≈_
; ❲_❳⤙_⤚_ = ❲_❳⤙_⤚_
}

record RightAlmostFumulaExtrusion (x ℓx : Level) : Set (f ⊔ suc x ⊔ ℓf ⊔ suc ℓx) where
infix 7 _⤙_⤚❲_❳
infix 4 _≈_
Expand All @@ -48,6 +56,13 @@ module _ (F : AlmostFumula f ℓf) where
setoid : Setoid x ℓx
setoid = record { isEquivalence = isEquivalence }

rawRightAlmostFumulaExtrusion : RawRightAlmostFumulaExtrusion F.rawAlmostFumula x ℓx
rawRightAlmostFumulaExtrusion = record
{ Carrier = Carrier
; _≈_ = _≈_
; _⤙_⤚❲_❳ = _⤙_⤚❲_❳
}

module _ (Fₗ : AlmostFumula fₗ ℓfₗ) (Fᵣ : AlmostFumula fᵣ ℓfᵣ) where
private
module Fₗ = AlmostFumula Fₗ
Expand All @@ -68,10 +83,20 @@ module _ (Fₗ : AlmostFumula fₗ ℓfₗ) (Fᵣ : AlmostFumula fᵣ ℓfᵣ) w
❲❳⤙⤚-leftAlmostFumulaExtrusion : LeftAlmostFumulaExtrusion Fₗ x ℓx
❲❳⤙⤚-leftAlmostFumulaExtrusion = record { isLeftAlmostFumulaExtrusion = ❲❳⤙⤚-isLeftAlmostFumulaExtrusion }
open LeftAlmostFumulaExtrusion ❲❳⤙⤚-leftAlmostFumulaExtrusion public
using (setoid)
using (setoid) renaming (rawLeftAlmostFumulaExtrusion to ❲❳⤙⤚-rawLeftAlmostFumulaExtrusion)

⤙⤚❲❳-rightAlmostFumulaExtrusion : RightAlmostFumulaExtrusion Fᵣ x ℓx
⤙⤚❲❳-rightAlmostFumulaExtrusion = record { isRightAlmostFumulaExtrusion = ⤙⤚❲❳-isRightAlmostFumulaExtrusion }
open RightAlmostFumulaExtrusion ⤙⤚❲❳-rightAlmostFumulaExtrusion public
using () renaming (rawRightAlmostFumulaExtrusion to ⤙⤚❲❳-rawRightAlmostFumulaExtrusion)

rawDoubleAlmostFumulaExtrusion : RawDoubleAlmostFumulaExtrusion Fₗ.rawAlmostFumula Fᵣ.rawAlmostFumula x ℓx
rawDoubleAlmostFumulaExtrusion = record
{ Carrier = Carrier
; _≈_ = _≈_
; ❲_❳⤙_⤚_ = ❲_❳⤙_⤚_
; _⤙_⤚❲_❳ = _⤙_⤚❲_❳
}

module _ (F : ReversibleAlmostFumula f ℓf) where
private
Expand All @@ -92,7 +117,17 @@ module _ (F : ReversibleAlmostFumula f ℓf) where
doubleAlmostFumulaExtrusion : DoubleAlmostFumulaExtrusion F.almostFumula F.almostFumula x ℓx
doubleAlmostFumulaExtrusion = record { isDoubleAlmostFumulaExtrusion = isDoubleAlmostFumulaExtrusion }
open DoubleAlmostFumulaExtrusion doubleAlmostFumulaExtrusion public
using (❲❳⤙⤚-leftAlmostFumulaExtrusion; ⤙⤚❲❳-rightAlmostFumulaExtrusion; setoid)
using (❲❳⤙⤚-leftAlmostFumulaExtrusion; ❲❳⤙⤚-rawLeftAlmostFumulaExtrusion;
⤙⤚❲❳-rightAlmostFumulaExtrusion; ⤙⤚❲❳-rawRightAlmostFumulaExtrusion;
rawDoubleAlmostFumulaExtrusion; setoid)

rawAlmostFumulaExtrusion : RawAlmostFumulaExtrusion F.rawAlmostFumula x ℓx
rawAlmostFumulaExtrusion = record
{ Carrier = Carrier
; _≈_ = _≈_
; ❲_❳⤙_⤚_ = ❲_❳⤙_⤚_
; _⤙_⤚❲_❳ = _⤙_⤚❲_❳
}

module _ (F : Fumula f ℓf) where
private
Expand All @@ -109,10 +144,18 @@ module _ (F : Fumula f ℓf) where
isLeftFumulaExtrusion : IsLeftFumulaExtrusion F _≈_ ❲_❳⤙_⤚_ ◆
open IsLeftFumulaExtrusion isLeftFumulaExtrusion public

❲❳⤙⤚-leftAlmostFumulaExtrusion : LeftAlmostFumulaExtrusion F.almostFumula x ℓx
❲❳⤙⤚-leftAlmostFumulaExtrusion = record { isLeftAlmostFumulaExtrusion = ❲❳⤙⤚-isLeftAlmostFumulaExtrusion }
open LeftAlmostFumulaExtrusion ❲❳⤙⤚-leftAlmostFumulaExtrusion public
using (setoid)
leftAlmostFumulaExtrusion : LeftAlmostFumulaExtrusion F.almostFumula x ℓx
leftAlmostFumulaExtrusion = record { isLeftAlmostFumulaExtrusion = isLeftAlmostFumulaExtrusion }
open LeftAlmostFumulaExtrusion leftAlmostFumulaExtrusion public
using (setoid; rawLeftAlmostFumulaExtrusion)

rawLeftFumulaExtrusion : RawLeftFumulaExtrusion F.rawFumula x ℓx
rawLeftFumulaExtrusion = record
{ Carrier = Carrier
; _≈_ = _≈_
; ❲_❳⤙_⤚_ = ❲_❳⤙_⤚_
; ◆ = ◆
}

record RightFumulaExtrusion (x ℓx : Level) : Set (f ⊔ suc x ⊔ ℓf ⊔ suc ℓx) where
infix 7 _⤙_⤚❲_❳
Expand All @@ -125,10 +168,18 @@ module _ (F : Fumula f ℓf) where
isRightFumulaExtrusion : IsRightFumulaExtrusion F _≈_ _⤙_⤚❲_❳ ◆
open IsRightFumulaExtrusion isRightFumulaExtrusion public

⤙⤚❲❳-rightAlmostFumulaExtrusion : RightAlmostFumulaExtrusion F.almostFumula x ℓx
⤙⤚❲❳-rightAlmostFumulaExtrusion = record { isRightAlmostFumulaExtrusion = ⤙⤚❲❳-isRightAlmostFumulaExtrusion }
open RightAlmostFumulaExtrusion ⤙⤚❲❳-rightAlmostFumulaExtrusion public
using (setoid)
rightAlmostFumulaExtrusion : RightAlmostFumulaExtrusion F.almostFumula x ℓx
rightAlmostFumulaExtrusion = record { isRightAlmostFumulaExtrusion = isRightAlmostFumulaExtrusion }
open RightAlmostFumulaExtrusion rightAlmostFumulaExtrusion public
using (setoid; rawRightAlmostFumulaExtrusion)

rawRightFumulaExtrusion : RawRightFumulaExtrusion F.rawFumula x ℓx
rawRightFumulaExtrusion = record
{ Carrier = Carrier
; _≈_ = _≈_
; _⤙_⤚❲_❳ = _⤙_⤚❲_❳
; ◆ = ◆
}

module _ (Fₗ : Fumula fₗ ℓfₗ) (Fᵣ : Fumula fᵣ ℓfᵣ) where
private
Expand All @@ -151,15 +202,30 @@ module _ (Fₗ : Fumula fₗ ℓfₗ) (Fᵣ : Fumula fᵣ ℓfᵣ) where
❲❳⤙⤚-leftFumulaExtrusion : LeftFumulaExtrusion Fₗ x ℓx
❲❳⤙⤚-leftFumulaExtrusion = record { isLeftFumulaExtrusion = ❲❳⤙⤚-isLeftFumulaExtrusion }
open LeftFumulaExtrusion ❲❳⤙⤚-leftFumulaExtrusion public
using (❲❳⤙⤚-leftAlmostFumulaExtrusion; setoid)
using (setoid) renaming (leftAlmostFumulaExtrusion to ❲❳⤙⤚-leftAlmostFumulaExtrusion;
rawLeftFumulaExtrusion to ❲❳⤙⤚-rawLeftFumulaExtrusion;
rawLeftAlmostFumulaExtrusion to ❲❳⤙⤚-rawLeftAlmostFumulaExtrusion)

⤙⤚❲❳-rightFumulaExtrusion : RightFumulaExtrusion Fᵣ x ℓx
⤙⤚❲❳-rightFumulaExtrusion = record { isRightFumulaExtrusion = ⤙⤚❲❳-isRightFumulaExtrusion }
open RightFumulaExtrusion ⤙⤚❲❳-rightFumulaExtrusion public
using (⤙⤚❲❳-rightAlmostFumulaExtrusion)
using () renaming (rightAlmostFumulaExtrusion to ⤙⤚❲❳-rightAlmostFumulaExtrusion;
rawRightFumulaExtrusion to ⤙⤚❲❳-rawRightFumulaExtrusion;
rawRightAlmostFumulaExtrusion to ⤙⤚❲❳-rawRightAlmostFumulaExtrusion)

doubleAlmostFumulaExtrusion : DoubleAlmostFumulaExtrusion Fₗ.almostFumula Fᵣ.almostFumula x ℓx
doubleAlmostFumulaExtrusion = record { isDoubleAlmostFumulaExtrusion = isDoubleAlmostFumulaExtrusion }
open DoubleAlmostFumulaExtrusion doubleAlmostFumulaExtrusion public
using (rawDoubleAlmostFumulaExtrusion)

rawDoubleFumulaExtrusion : RawDoubleFumulaExtrusion Fₗ.rawFumula Fᵣ.rawFumula x ℓx
rawDoubleFumulaExtrusion = record
{ Carrier = Carrier
; _≈_ = _≈_
; ❲_❳⤙_⤚_ = ❲_❳⤙_⤚_
; _⤙_⤚❲_❳ = _⤙_⤚❲_❳
; ◆ = ◆
}

module _ (F : ReversibleFumula f ℓf) where
private
Expand All @@ -181,9 +247,23 @@ module _ (F : ReversibleFumula f ℓf) where
doubleFumulaExtrusion : DoubleFumulaExtrusion F.fumula F.fumula x ℓx
doubleFumulaExtrusion = record { isDoubleFumulaExtrusion = isDoubleFumulaExtrusion }
open DoubleFumulaExtrusion doubleFumulaExtrusion public
using (❲❳⤙⤚-leftFumulaExtrusion; ⤙⤚❲❳-rightFumulaExtrusion;
❲❳⤙⤚-leftAlmostFumulaExtrusion; ⤙⤚❲❳-rightAlmostFumulaExtrusion;
doubleAlmostFumulaExtrusion)
using (❲❳⤙⤚-leftFumulaExtrusion; ❲❳⤙⤚-rawLeftFumulaExtrusion;
⤙⤚❲❳-rightFumulaExtrusion; ⤙⤚❲❳-rawRightFumulaExtrusion;
❲❳⤙⤚-leftAlmostFumulaExtrusion; ❲❳⤙⤚-rawLeftAlmostFumulaExtrusion;
⤙⤚❲❳-rightAlmostFumulaExtrusion; ⤙⤚❲❳-rawRightAlmostFumulaExtrusion;
doubleAlmostFumulaExtrusion; rawDoubleAlmostFumulaExtrusion;
rawDoubleFumulaExtrusion)

almostFumulaExtrusion : AlmostFumulaExtrusion F.reversibleAlmostFumula x ℓx
almostFumulaExtrusion = record { isAlmostFumulaExtrusion = isAlmostFumulaExtrusion }
open AlmostFumulaExtrusion almostFumulaExtrusion public
using (rawAlmostFumulaExtrusion)

rawFumulaExtrusion : RawFumulaExtrusion F.rawFumula x ℓx
rawFumulaExtrusion = record
{ Carrier = Carrier
; _≈_ = _≈_
; ❲_❳⤙_⤚_ = ❲_❳⤙_⤚_
; _⤙_⤚❲_❳ = _⤙_⤚❲_❳
; ◆ = ◆
}
197 changes: 197 additions & 0 deletions src/Algebra/Fumula/Extrusion/Bundles/Raw.agda
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,197 @@
------------------------------------------------------------------------
-- Raw bundles for fumula extrusions.
------------------------------------------------------------------------

-- The contents of this module should be accessed via `Algebra.Fumula.Extrusion`.

module Algebra.Fumula.Extrusion.Bundles.Raw where

open import Level using (Level; _⊔_; suc)
open import Relation.Binary.Core using (Rel)
open import Algebra.Fumula.Bundles.Raw
open import Algebra.Fumula.Extrusion.Core

private
variable
f ℓf fₗ ℓfₗ fᵣ ℓfᵣ : Level

module _ (F : RawAlmostFumula f ℓf) where
private
module F = RawAlmostFumula F

record RawLeftAlmostFumulaExtrusion (x ℓx : Level) : Set (f ⊔ suc x ⊔ ℓf ⊔ suc ℓx) where
infix 7 ❲_❳⤙_⤚_
infix 4 _≈_
field
Carrier : Set x
_≈_ : Rel Carrier ℓx
❲_❳⤙_⤚_ : Op₃ₗ F.Carrier Carrier

record RawRightAlmostFumulaExtrusion (x ℓx : Level) : Set (f ⊔ suc x ⊔ ℓf ⊔ suc ℓx) where
infix 7 _⤙_⤚❲_❳
infix 4 _≈_
field
Carrier : Set x
_≈_ : Rel Carrier ℓx
_⤙_⤚❲_❳ : Op₃ᵣ F.Carrier Carrier

module _ (Fₗ : RawAlmostFumula fₗ ℓfₗ) (Fᵣ : RawAlmostFumula fᵣ ℓfᵣ) where
private
module Fₗ = RawAlmostFumula Fₗ
module Fᵣ = RawAlmostFumula Fᵣ

record RawDoubleAlmostFumulaExtrusion (x ℓx : Level) : Set (fₗ ⊔ fᵣ ⊔ suc x ⊔ ℓfₗ ⊔ ℓfᵣ ⊔ suc ℓx) where
infix 7 ❲_❳⤙_⤚_
infix 7 _⤙_⤚❲_❳
infix 4 _≈_
field
Carrier : Set x
_≈_ : Rel Carrier ℓx
❲_❳⤙_⤚_ : Op₃ₗ Fₗ.Carrier Carrier
_⤙_⤚❲_❳ : Op₃ᵣ Fᵣ.Carrier Carrier

❲❳⤙⤚-rawLeftAlmostFumulaExtrusion : RawLeftAlmostFumulaExtrusion Fₗ x ℓx
❲❳⤙⤚-rawLeftAlmostFumulaExtrusion = record
{ Carrier = Carrier
; _≈_ = _≈_
; ❲_❳⤙_⤚_ = ❲_❳⤙_⤚_
}

⤙⤚❲❳-rawRightAlmostFumulaExtrusion : RawRightAlmostFumulaExtrusion Fᵣ x ℓx
⤙⤚❲❳-rawRightAlmostFumulaExtrusion = record
{ Carrier = Carrier
; _≈_ = _≈_
; _⤙_⤚❲_❳ = _⤙_⤚❲_❳
}

module _ (F : RawAlmostFumula f ℓf) where
private
module F = RawAlmostFumula F

record RawAlmostFumulaExtrusion (x ℓx : Level) : Set (f ⊔ suc x ⊔ ℓf ⊔ suc ℓx) where
infix 7 ❲_❳⤙_⤚_
infix 7 _⤙_⤚❲_❳
infix 4 _≈_
field
Carrier : Set x
_≈_ : Rel Carrier ℓx
❲_❳⤙_⤚_ : Op₃ₗ F.Carrier Carrier
_⤙_⤚❲_❳ : Op₃ᵣ F.Carrier Carrier

rawDoubleAlmostFumulaExtrusion : RawDoubleAlmostFumulaExtrusion F F x ℓx
rawDoubleAlmostFumulaExtrusion = record
{ Carrier = Carrier
; _≈_ = _≈_
; ❲_❳⤙_⤚_ = ❲_❳⤙_⤚_
; _⤙_⤚❲_❳ = _⤙_⤚❲_❳
}
open RawDoubleAlmostFumulaExtrusion rawDoubleAlmostFumulaExtrusion public
using (❲❳⤙⤚-rawLeftAlmostFumulaExtrusion; ⤙⤚❲❳-rawRightAlmostFumulaExtrusion)

module _ (F : RawFumula f ℓf) where
private
module F = RawFumula F

record RawLeftFumulaExtrusion (x ℓx : Level) : Set (f ⊔ suc x ⊔ ℓf ⊔ suc ℓx) where
infix 7 ❲_❳⤙_⤚_
infix 4 _≈_
field
Carrier : Set x
_≈_ : Rel Carrier ℓx
❲_❳⤙_⤚_ : Op₃ₗ F.Carrier Carrier
◆ : Carrier

rawLeftAlmostFumulaExtrusion : RawLeftAlmostFumulaExtrusion F.rawAlmostFumula x ℓx
rawLeftAlmostFumulaExtrusion = record
{ Carrier = Carrier
; _≈_ = _≈_
; ❲_❳⤙_⤚_ = ❲_❳⤙_⤚_
}

record RawRightFumulaExtrusion (x ℓx : Level) : Set (f ⊔ suc x ⊔ ℓf ⊔ suc ℓx) where
infix 7 _⤙_⤚❲_❳
infix 4 _≈_
field
Carrier : Set x
_≈_ : Rel Carrier ℓx
_⤙_⤚❲_❳ : Op₃ᵣ F.Carrier Carrier
◆ : Carrier

rawRightAlmostFumulaExtrusion : RawRightAlmostFumulaExtrusion F.rawAlmostFumula x ℓx
rawRightAlmostFumulaExtrusion = record
{ Carrier = Carrier
; _≈_ = _≈_
; _⤙_⤚❲_❳ = _⤙_⤚❲_❳
}

module _ (Fₗ : RawFumula fₗ ℓfₗ) (Fᵣ : RawFumula fᵣ ℓfᵣ) where
private
module Fₗ = RawFumula Fₗ
module Fᵣ = RawFumula Fᵣ

record RawDoubleFumulaExtrusion (x ℓx : Level) : Set (fₗ ⊔ fᵣ ⊔ suc x ⊔ ℓfₗ ⊔ ℓfᵣ ⊔ suc ℓx) where
infix 7 ❲_❳⤙_⤚_
infix 7 _⤙_⤚❲_❳
infix 4 _≈_
field
Carrier : Set x
_≈_ : Rel Carrier ℓx
❲_❳⤙_⤚_ : Op₃ₗ Fₗ.Carrier Carrier
_⤙_⤚❲_❳ : Op₃ᵣ Fᵣ.Carrier Carrier
◆ : Carrier

❲❳⤙⤚-rawLeftFumulaExtrusion : RawLeftFumulaExtrusion Fₗ x ℓx
❲❳⤙⤚-rawLeftFumulaExtrusion = record
{ Carrier = Carrier
; _≈_ = _≈_
; ❲_❳⤙_⤚_ = ❲_❳⤙_⤚_
; ◆ = ◆
}
open RawLeftFumulaExtrusion ❲❳⤙⤚-rawLeftFumulaExtrusion public
using () renaming (rawLeftAlmostFumulaExtrusion to ❲❳⤙⤚-rawLeftAlmostFumulaExtrusion)

⤙⤚❲❳-rawRightFumulaExtrusion : RawRightFumulaExtrusion Fᵣ x ℓx
⤙⤚❲❳-rawRightFumulaExtrusion = record
{ Carrier = Carrier
; _≈_ = _≈_
; _⤙_⤚❲_❳ = _⤙_⤚❲_❳
; ◆ = ◆
}
open RawRightFumulaExtrusion ⤙⤚❲❳-rawRightFumulaExtrusion public
using () renaming (rawRightAlmostFumulaExtrusion to ⤙⤚❲❳-rawRightAlmostFumulaExtrusion)

rawDoubleAlmostFumulaExtrusion : RawDoubleAlmostFumulaExtrusion Fₗ.rawAlmostFumula Fᵣ.rawAlmostFumula x ℓx
rawDoubleAlmostFumulaExtrusion = record
{ Carrier = Carrier
; _≈_ = _≈_
; ❲_❳⤙_⤚_ = ❲_❳⤙_⤚_
; _⤙_⤚❲_❳ = _⤙_⤚❲_❳
}

module _ (F : RawFumula f ℓf) where
private
module F = RawFumula F

record RawFumulaExtrusion (x ℓx : Level) : Set (f ⊔ suc x ⊔ ℓf ⊔ suc ℓx) where
infix 7 ❲_❳⤙_⤚_
infix 7 _⤙_⤚❲_❳
infix 4 _≈_
field
Carrier : Set x
_≈_ : Rel Carrier ℓx
❲_❳⤙_⤚_ : Op₃ₗ F.Carrier Carrier
_⤙_⤚❲_❳ : Op₃ᵣ F.Carrier Carrier
◆ : Carrier

rawDoubleFumulaExtrusion : RawDoubleFumulaExtrusion F F x ℓx
rawDoubleFumulaExtrusion = record
{ Carrier = Carrier
; _≈_ = _≈_
; ❲_❳⤙_⤚_ = ❲_❳⤙_⤚_
; _⤙_⤚❲_❳ = _⤙_⤚❲_❳
; ◆ = ◆
}
open RawDoubleFumulaExtrusion rawDoubleFumulaExtrusion public
using (❲❳⤙⤚-rawLeftFumulaExtrusion; ❲❳⤙⤚-rawLeftAlmostFumulaExtrusion;
⤙⤚❲❳-rawRightFumulaExtrusion; ⤙⤚❲❳-rawRightAlmostFumulaExtrusion;
rawDoubleAlmostFumulaExtrusion)
Loading

0 comments on commit e9c8f9f

Please sign in to comment.