diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-09-27 13:55:29 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-09-27 13:55:29 +0200 |
| commit | caeae59c7e6ae461a066ac008160035dbff9122b (patch) | |
| tree | 4f2f3fc1de45d64006c570ac96499b1ceb7cdb76 /LiftGet.agda | |
| parent | 1428e4192d61533864a8f163c86272eef4b891cf (diff) | |
| download | bidiragda-caeae59c7e6ae461a066ac008160035dbff9122b.tar.gz | |
remove getVec-getlen in favour of plain subst
Diffstat (limited to 'LiftGet.agda')
| -rw-r--r-- | LiftGet.agda | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/LiftGet.agda b/LiftGet.agda index 4c335c9..c4f1acd 100644 --- a/LiftGet.agda +++ b/LiftGet.agda @@ -141,10 +141,7 @@ get-trafo-2-getlen getlen get n = begin ≡⟨ cong getlen (length-replicate n) ⟩ getlen n ∎ -getVec-getlen : {getlen₁ getlen₂ : ℕ → ℕ} → (get : getV-type getlen₁) → getlen₁ ≗ getlen₂ → getV-type getlen₂ -getVec-getlen get p {B} {n} v = subst (Vec B) (p n) (get v) - -get-trafo-2-get : (getlen : ℕ → ℕ) → (get : getV-type getlen) → {B : Set} {n : ℕ} → proj₂ (getList-to-getVec (getVec-to-getList get)) {B} {n} ≗ getVec-getlen get (sym ∘ (get-trafo-2-getlen getlen get)) +get-trafo-2-get : (getlen : ℕ → ℕ) → (get : getV-type getlen) → {B : Set} {n : ℕ} → proj₂ (getList-to-getVec (getVec-to-getList get)) ≗ subst (Vec B) (sym (get-trafo-2-getlen getlen get n)) ∘ get get-trafo-2-get getlen get {B} {n} v = begin proj₂ (getList-to-getVec (getVec-to-getList get)) v ≡⟨ refl ⟩ @@ -160,9 +157,7 @@ get-trafo-2-get getlen get {B} {n} v = begin ≡⟨ subst-subst (Vec B) (cong getlen (sym (length-toList v))) (trans p' p) (get v) ⟩ subst (Vec B) (trans (cong getlen (sym (length-toList v))) (trans p' p)) (get v) ≡⟨ cong (flip (subst (Vec B)) (get v)) (proof-irrelevance (trans (cong getlen (sym (length-toList v))) (trans p' p)) p'') ⟩ - subst (Vec B) p'' (get v) - ≡⟨ refl ⟩ - getVec-getlen get (sym ∘ (get-trafo-2-getlen getlen get)) v ∎ + subst (Vec B) p'' (get v) ∎ where n' : ℕ n' = length (toList (get (fromList (replicate n tt)))) p : length (toList (get (fromList (toList v)))) ≡ n' |