diff options
Diffstat (limited to 'GetTypes.agda')
| -rw-r--r-- | GetTypes.agda | 41 |
1 files changed, 4 insertions, 37 deletions
diff --git a/GetTypes.agda b/GetTypes.agda index 2812e2b..f23d154 100644 --- a/GetTypes.agda +++ b/GetTypes.agda @@ -52,39 +52,6 @@ VecVec-to-PartialVecVec G = record ; free-theorem = free-theorem } where open VecVec.Get G -module PartialShapeVec where - record Get : Set₁ where - field - Shape : Set - Container : Set → Shape → Set - ShapeT : Shaped Shape Container - - I : Setoid ℓ₀ ℓ₀ - gl₁ : I ↪ EqSetoid Shape - gl₂ : I ⟶ EqSetoid ℕ - - |I| = Setoid.Carrier I - |gl₁| = _⟨$⟩_ (to gl₁) - |gl₂| = _⟨$⟩_ gl₂ - - open Shaped ShapeT using (fmap) - - field - get : {A : Set} {i : |I|} → Container A (|gl₁| i) → Vec A (|gl₂| i) - free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ fmap f ≗ mapV f ∘ get - - open Shaped ShapeT public - -PartialVecVec-to-PartialShapeVec : PartialVecVec.Get → PartialShapeVec.Get -PartialVecVec-to-PartialShapeVec G = record - { ShapeT = VecShaped - ; I = I - ; gl₁ = gl₁ - ; gl₂ = gl₂ - ; get = get - ; free-theorem = free-theorem - } where open PartialVecVec.Get G - module PartialShapeShape where record Get : Set₁ where field @@ -114,13 +81,13 @@ module PartialShapeShape where open Shaped SourceShapeT public using () renaming (fmap to fmapS) open Shaped ViewShapeT public using () renaming (fmap to fmapV) -PartialShapeVec-to-PartialShapeShape : PartialShapeVec.Get → PartialShapeShape.Get -PartialShapeVec-to-PartialShapeShape G = record - { SourceShapeT = ShapeT +PartialVecVec-to-PartialShapeShape : PartialVecVec.Get → PartialShapeShape.Get +PartialVecVec-to-PartialShapeShape G = record + { SourceShapeT = VecShaped ; ViewShapeT = VecShaped ; I = I ; gl₁ = gl₁ ; gl₂ = gl₂ ; get = get ; free-theorem = free-theorem - } where open PartialShapeVec.Get G + } where open PartialVecVec.Get G |