diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-04-03 08:45:19 +0200 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-04-03 08:45:19 +0200 |
| commit | 20ff2bd915d116223e1ea9eda60647c60de98725 (patch) | |
| tree | 5ecf0303a025cc930292223779013d39cd4432af /GetTypes.agda | |
| parent | cb7f533f4119f044201df2f28838c96ee367b771 (diff) | |
| download | bidiragda-20ff2bd915d116223e1ea9eda60647c60de98725.tar.gz | |
drop PartialShapeVec
One can use PartialShapeShape instead, so there is limited utility for
this type. It is not used directly and there also is no PartialVecShape.
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 |