diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-04 10:52:49 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-04 10:52:49 +0100 |
| commit | 20c176d383e59a0345f7425c5f14679906159a59 (patch) | |
| tree | a2874cac4922670c6d8e8229c24b56a725c11dda /GetTypes.agda | |
| parent | 257665f2910296c6e87113d2f7a418e1f83b33f6 (diff) | |
| download | bidiragda-20c176d383e59a0345f7425c5f14679906159a59.tar.gz | |
add convenience members to PartialVecVec.Get
Diffstat (limited to 'GetTypes.agda')
| -rw-r--r-- | GetTypes.agda | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/GetTypes.agda b/GetTypes.agda index a52ec24..eb72cea 100644 --- a/GetTypes.agda +++ b/GetTypes.agda @@ -32,8 +32,14 @@ module PartialVecVec where I : Setoid ℓ₀ ℓ₀ gl₁ : I ↪ EqSetoid ℕ gl₂ : I ⟶ EqSetoid ℕ - get : {A : Set} {i : Setoid.Carrier I} → Vec A (to gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i) - free-theorem : {α β : Set} → (f : α → β) → {i : Setoid.Carrier I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get + + |I| = Setoid.Carrier I + |gl₁| = _⟨$⟩_ (to gl₁) + |gl₂| = _⟨$⟩_ gl₂ + + field + get : {A : Set} {i : |I|} → Vec A (|gl₁| i) → Vec A (|gl₂| i) + free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get VecVec-to-PartialVecVec G = record |