diff options
Diffstat (limited to 'GetTypes.agda')
| -rw-r--r-- | GetTypes.agda | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/GetTypes.agda b/GetTypes.agda index 0db3f31..2812e2b 100644 --- a/GetTypes.agda +++ b/GetTypes.agda @@ -84,3 +84,43 @@ PartialVecVec-to-PartialShapeVec G = record ; get = get ; free-theorem = free-theorem } where open PartialVecVec.Get G + +module PartialShapeShape where + record Get : Set₁ where + field + SourceShape : Set + SourceContainer : Set → SourceShape → Set + SourceShapeT : Shaped SourceShape SourceContainer + + ViewShape : Set + ViewContainer : Set → ViewShape → Set + ViewShapeT : Shaped ViewShape ViewContainer + + I : Setoid ℓ₀ ℓ₀ + gl₁ : I ↪ EqSetoid SourceShape + gl₂ : I ⟶ EqSetoid ViewShape + + |I| = Setoid.Carrier I + |gl₁| = _⟨$⟩_ (to gl₁) + |gl₂| = _⟨$⟩_ gl₂ + + open Shaped SourceShapeT using () renaming (fmap to fmapS) + open Shaped ViewShapeT using () renaming (fmap to fmapV) + + field + get : {A : Set} {i : |I|} → SourceContainer A (|gl₁| i) → ViewContainer A (|gl₂| i) + free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ fmapS f ≗ fmapV f ∘ get + + 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 + ; ViewShapeT = VecShaped + ; I = I + ; gl₁ = gl₁ + ; gl₂ = gl₂ + ; get = get + ; free-theorem = free-theorem + } where open PartialShapeVec.Get G |