From d8ed3c5d8bb02c626b3d263ed9d6a4bcb5836ae0 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 9 Jun 2015 16:33:31 +0200 Subject: drop barred members from GetTypes These became duplicates of their non-barred counterparts. --- BFF.agda | 14 +++++++------- BFFPlug.agda | 8 ++++---- Bidir.agda | 30 +++++++++++++++--------------- GetTypes.agda | 18 ++++-------------- Precond.agda | 20 ++++++++++---------- 5 files changed, 40 insertions(+), 50 deletions(-) diff --git a/BFF.agda b/BFF.agda index 26d1d5e..e9b459a 100644 --- a/BFF.agda +++ b/BFF.agda @@ -36,18 +36,18 @@ module PartialShapeBFF (A : DecSetoid ℓ₀ ℓ₀) where denumerate : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {α : Set} {s : S} → (c : C α s) → Fin (Shaped.arity ShapeT s) → α denumerate ShapeT c = flip lookupV (Shaped.content ShapeT c) - bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Get.SourceContainer G Carrier (Get.|gl₁| G i) → Get.ViewContainer G Carrier (Get.|gl₂| G j) → Maybe (Get.SourceContainer G (Maybe Carrier) (Get.|gl₁| G j)) - bff G {i} j s v = let s′ = enumerate SourceShapeT (|gl₁| i) + bff : (G : Get) → {i : Get.I G} → (j : Get.I G) → Get.SourceContainer G Carrier (Get.gl₁ G i) → Get.ViewContainer G Carrier (Get.gl₂ G j) → Maybe (Get.SourceContainer G (Maybe Carrier) (Get.gl₁ G j)) + bff G {i} j s v = let s′ = enumerate SourceShapeT (gl₁ i) t′ = get s′ g = fromFunc (denumerate SourceShapeT s) g′ = delete-many (Shaped.content ViewShapeT t′) g - t = enumerate SourceShapeT (|gl₁| j) + t = enumerate SourceShapeT (gl₁ j) h = assoc (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT v) - h′ = (flip union (reshape g′ (Shaped.arity SourceShapeT (|gl₁| j)))) <$> h + h′ = (flip union (reshape g′ (Shaped.arity SourceShapeT (gl₁ j)))) <$> h in ((λ f → fmapS f t) ∘ flip lookupM) <$> h′ where open Get G - sbff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Get.SourceContainer G Carrier (Get.|gl₁| G i) → Get.ViewContainer G Carrier (Get.|gl₂| G j) → Maybe (Get.SourceContainer G Carrier (Get.|gl₁| G j)) + sbff : (G : Get) → {i : Get.I G} → (j : Get.I G) → Get.SourceContainer G Carrier (Get.gl₁ G i) → Get.ViewContainer G Carrier (Get.gl₂ G j) → Maybe (Get.SourceContainer G Carrier (Get.gl₁ G j)) sbff G j s v = bff G j s v >>= Shaped.sequence (Get.SourceShapeT G) module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where @@ -66,10 +66,10 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier denumerate = PartialShapeBFF.denumerate A VecShaped - bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec (Maybe Carrier) (Get.|gl₁| G j)) + bff : (G : Get) → {i : Get.I G} → (j : Get.I G) → Vec Carrier (Get.gl₁ G i) → Vec Carrier (Get.gl₂ G j) → Maybe (Vec (Maybe Carrier) (Get.gl₁ G j)) bff G j s v = PartialShapeBFF.bff A (PartialVecVec-to-PartialShapeShape G) j s v - sbff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec Carrier (Get.|gl₁| G j)) + sbff : (G : Get) → {i : Get.I G} → (j : Get.I G) → Vec Carrier (Get.gl₁ G i) → Vec Carrier (Get.gl₂ G j) → Maybe (Vec Carrier (Get.gl₁ G j)) sbff G j s v = PartialShapeBFF.sbff A (PartialVecVec-to-PartialShapeShape G) j s v module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where diff --git a/BFFPlug.agda b/BFFPlug.agda index a31d1bb..0d69723 100644 --- a/BFFPlug.agda +++ b/BFFPlug.agda @@ -24,13 +24,13 @@ open DecSetoid A using (Carrier) open GetTypes.PartialVecVec public using (Get) open BFF.PartialVecBFF A public using (sbff ; bff) -bffsameshape : (G : Get) → {i : Get.|I| G} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G i) → Maybe (Vec Carrier (Get.|gl₁| G i)) +bffsameshape : (G : Get) → {i : Get.I G} → Vec Carrier (Get.gl₁ G i) → Vec Carrier (Get.gl₂ G i) → Maybe (Vec Carrier (Get.gl₁ G i)) bffsameshape G {i} = sbff G i -bffplug : (G : Get) → (Get.|I| G → ℕ → Maybe (Get.|I| G)) → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (∃ λ j → Vec (Maybe Carrier) (Get.|gl₁| G j)) +bffplug : (G : Get) → (Get.I G → ℕ → Maybe (Get.I G)) → {i : Get.I G} → {m : ℕ} → Vec Carrier (Get.gl₁ G i) → Vec Carrier m → Maybe (∃ λ j → Vec (Maybe Carrier) (Get.gl₁ G j)) bffplug G sput {i} {m} s v with sput i m ... | nothing = nothing -... | just j with Get.|gl₂| G j ≟ m +... | just j with Get.gl₂ G j ≟ m ... | no gl₂j≢m = nothing bffplug G sput {i} s v | just j | yes refl with bff G j s v ... | nothing = nothing @@ -39,7 +39,7 @@ bffplug G sput {i} s v | just j | yes refl with bff G j s v _SimpleRightInvOf_ : {A B : Set} → (A → B) → (B → A) → Set f SimpleRightInvOf g = ≡-to-Π f RightInverseOf ≡-to-Π g -bffinv : (G : Get) → (nelteg : ℕ → Get.I G) → nelteg SimpleRightInvOf Get.gl₂ G → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (Get.|gl₁| G (nelteg m))) +bffinv : (G : Get) → (nelteg : ℕ → Get.I G) → nelteg SimpleRightInvOf Get.gl₂ G → {i : Get.I G} → {m : ℕ} → Vec Carrier (Get.gl₁ G i) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (Get.gl₁ G (nelteg m))) bffinv G nelteg inv {m = m} s v = bff G (nelteg m) s (subst (Vec Carrier) (sym (inv m)) v) module InvExamples where diff --git a/Bidir.agda b/Bidir.agda index 3c0ebea..9b60461 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -108,7 +108,7 @@ lemma-fmap-denumerate-enumerate {S} {C} ShapeT {s = s} c = begin open Shaped ShapeT -theorem-1 : (G : Get) → {i : Get.|I| G} → (s : Get.SourceContainer G Carrier (Get.|gl₁| G i)) → bff G i s (Get.get G s) ≡ just (Get.fmapS G just s) +theorem-1 : (G : Get) → {i : Get.I G} → (s : Get.SourceContainer G Carrier (Get.gl₁ G i)) → bff G i s (Get.get G s) ≡ just (Get.fmapS G just s) theorem-1 G {i} s = begin bff G i s (get s) ≡⟨ cong (bff G i s ∘ get) (sym (lemma-fmap-denumerate-enumerate SourceShapeT s)) ⟩ @@ -122,25 +122,25 @@ theorem-1 G {i} s = begin ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′) (lemma-1 f (Shaped.content ViewShapeT (get t))) ⟩ (Maybe.just ∘ h′↦r ∘ h↦h′) (restrict f (Shaped.content ViewShapeT (get t))) ≡⟨ cong just (begin - h′↦r (union (restrict f (Shaped.content ViewShapeT (get t))) (reshape g′ (Shaped.arity SourceShapeT (|gl₁| i)))) + h′↦r (union (restrict f (Shaped.content ViewShapeT (get t))) (reshape g′ (Shaped.arity SourceShapeT (gl₁ i)))) ≡⟨ cong (h′↦r ∘ union (restrict f (Shaped.content ViewShapeT (get t)))) (lemma-reshape-id g′) ⟩ h′↦r (union (restrict f (Shaped.content ViewShapeT (get t))) g′) ≡⟨ cong h′↦r (lemma-disjoint-union f (Shaped.content ViewShapeT (get t))) ⟩ h′↦r (fromFunc f) ≡⟨ refl ⟩ fmapS (flip lookupM (fromFunc f)) t - ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (|gl₁| i)) (lemma-lookupM-fromFunc f) t ⟩ + ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lemma-lookupM-fromFunc f) t ⟩ fmapS (Maybe.just ∘ f) t - ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (|gl₁| i)) just f t ⟩ + ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (gl₁ i)) just f t ⟩ fmapS just (fmapS f t) ≡⟨ cong (fmapS just) (lemma-fmap-denumerate-enumerate SourceShapeT s) ⟩ fmapS just s ∎) ⟩ _ ∎ where open ≡-Reasoning open Get G - t = enumerate SourceShapeT (|gl₁| i) + t = enumerate SourceShapeT (gl₁ i) f = denumerate SourceShapeT s g′ = delete-many (Shaped.content ViewShapeT (get t)) (fromFunc f) - h↦h′ = flip union (reshape g′ (Shaped.arity SourceShapeT (|gl₁| i))) + h↦h′ = flip union (reshape g′ (Shaped.arity SourceShapeT (gl₁ i))) h′↦r = (λ f′ → fmapS f′ t) ∘ flip lookupM @@ -214,7 +214,7 @@ lemma-sequence-successful ShapeT {s = s} c {r} p = just-injective (sym (begin open Shaped ShapeT wp = lemma-<$>-just (sequenceV (content c)) p -lemma-get-sequence : {A : Set} → (G : Get) → {i : Get.|I| G} {v : Get.SourceContainer G (Maybe A) (Get.|gl₁| G i)} {r : Get.SourceContainer G A (Get.|gl₁| G i)} → Shaped.sequence (Get.SourceShapeT G) v ≡ just r → Get.get G <$> Shaped.sequence (Get.SourceShapeT G) v ≡ Shaped.sequence (Get.ViewShapeT G) (Get.get G v) +lemma-get-sequence : {A : Set} → (G : Get) → {i : Get.I G} {v : Get.SourceContainer G (Maybe A) (Get.gl₁ G i)} {r : Get.SourceContainer G A (Get.gl₁ G i)} → Shaped.sequence (Get.SourceShapeT G) v ≡ just r → Get.get G <$> Shaped.sequence (Get.SourceShapeT G) v ≡ Shaped.sequence (Get.ViewShapeT G) (Get.get G v) lemma-get-sequence G {v = v} {r = r} p = begin get <$> Shaped.sequence SourceShapeT v ≡⟨ cong (_<$>_ get ∘ Shaped.sequence SourceShapeT) (lemma-sequence-successful SourceShapeT v p) ⟩ @@ -253,9 +253,9 @@ sequence-cong ShapeT α {s} (shape≈ , content≈) | .(just x) | .(just y) | ju open Shaped ShapeT sequence-cong ShapeT α (shape≈ , content≈) | .nothing | .nothing | nothing = nothing -theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.SourceContainer G Carrier (Get.|gl₁| G i)) → (v : Get.ViewContainer G Carrier (Get.|gl₂| G j)) → (u : Get.SourceContainer G (Maybe Carrier) (Get.|gl₁| G j)) → bff G j s v ≡ just u → ShapedISetoid (EqSetoid _) (Get.ViewShapeT G) (MaybeSetoid A.setoid) at _ ∋ Get.get G u ≈ Get.fmapV G just v -theorem-2 G {i} j s v u p with (lemma-<$>-just ((flip union (reshape (delete-many (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.|gl₁| G i)))) (fromFunc (denumerate (Get.SourceShapeT G) s))) (Shaped.arity (Get.SourceShapeT G) (Get.|gl₁| G j)))) <$> (assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.|gl₁| G j)))) (Shaped.content (Get.ViewShapeT G) v))) p) -theorem-2 G {i} j s v u p | h′ , ph′ with (lemma-<$>-just (assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.|gl₁| G j)))) (Shaped.content (Get.ViewShapeT G) v)) ph′) +theorem-2 : (G : Get) → {i : Get.I G} → (j : Get.I G) → (s : Get.SourceContainer G Carrier (Get.gl₁ G i)) → (v : Get.ViewContainer G Carrier (Get.gl₂ G j)) → (u : Get.SourceContainer G (Maybe Carrier) (Get.gl₁ G j)) → bff G j s v ≡ just u → ShapedISetoid (EqSetoid _) (Get.ViewShapeT G) (MaybeSetoid A.setoid) at _ ∋ Get.get G u ≈ Get.fmapV G just v +theorem-2 G {i} j s v u p with (lemma-<$>-just ((flip union (reshape (delete-many (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.gl₁ G i)))) (fromFunc (denumerate (Get.SourceShapeT G) s))) (Shaped.arity (Get.SourceShapeT G) (Get.gl₁ G j)))) <$> (assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.gl₁ G j)))) (Shaped.content (Get.ViewShapeT G) v))) p) +theorem-2 G {i} j s v u p | h′ , ph′ with (lemma-<$>-just (assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.gl₁ G j)))) (Shaped.content (Get.ViewShapeT G) v)) ph′) theorem-2 G {i} j s v u p | h′ , ph′ | h , ph = refl , (begin content (get u) ≡⟨ cong content (just-injective (trans (cong (_<$>_ get) (sym p)) @@ -267,7 +267,7 @@ theorem-2 G {i} j s v u p | h′ , ph′ | h , ph = refl , (begin content (fmapV (flip lookupM (h↦h′ h)) (get t)) ≡⟨ Shaped.fmap-content ViewShapeT (flip lookupM (h↦h′ h)) (get t) ⟩ map (flip lookupM (h↦h′ h)) (content (get t)) - ≡⟨ lemma-union-not-used h (reshape g′ (Shaped.arity SourceShapeT (|gl₁| j))) (content (get t)) (lemma-assoc-domain (content (get t)) (content v) ph) ⟩ + ≡⟨ lemma-union-not-used h (reshape g′ (Shaped.arity SourceShapeT (gl₁ j))) (content (get t)) (lemma-assoc-domain (content (get t)) (content v) ph) ⟩ map (flip lookupM h) (content (get t)) ≈⟨ lemma-2 (content (get t)) (content v) h ph ⟩ map just (content v) @@ -276,14 +276,14 @@ theorem-2 G {i} j s v u p | h′ , ph′ | h , ph = refl , (begin where open EqR (VecISetoid (MaybeSetoid A.setoid) at _) open Get G open Shaped ViewShapeT using (content) - s′ = enumerate SourceShapeT (|gl₁| i) + s′ = enumerate SourceShapeT (gl₁ i) g = fromFunc (denumerate SourceShapeT s) g′ = delete-many (Shaped.content ViewShapeT (get s′)) g - t = enumerate SourceShapeT (|gl₁| j) - h↦h′ = flip union (reshape g′ (Shaped.arity SourceShapeT (|gl₁| j))) + t = enumerate SourceShapeT (gl₁ j) + h↦h′ = flip union (reshape g′ (Shaped.arity SourceShapeT (gl₁ j))) h′↦r = (λ f → fmapS f t) ∘ flip lookupM -theorem-2′ : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.SourceContainer G Carrier (Get.|gl₁| G i)) → (v : Get.ViewContainer G Carrier (Get.|gl₂| G j)) → (u : Get.SourceContainer G Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just (Get.fmapS G just u) → ShapedISetoid (EqSetoid _) (Get.ViewShapeT G) A.setoid at _ ∋ Get.get G u ≈ v +theorem-2′ : (G : Get) → {i : Get.I G} → (j : Get.I G) → (s : Get.SourceContainer G Carrier (Get.gl₁ G i)) → (v : Get.ViewContainer G Carrier (Get.gl₂ G j)) → (u : Get.SourceContainer G Carrier (Get.gl₁ G j)) → bff G j s v ≡ just (Get.fmapS G just u) → ShapedISetoid (EqSetoid _) (Get.ViewShapeT G) A.setoid at _ ∋ Get.get G u ≈ v theorem-2′ G j s v u p = drop-just (begin get <$> just u ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence SourceShapeT u)) ⟩ diff --git a/GetTypes.agda b/GetTypes.agda index 286b9aa..83f6845 100644 --- a/GetTypes.agda +++ b/GetTypes.agda @@ -29,14 +29,8 @@ module PartialVecVec where I : Set gl₁ : I → ℕ gl₂ : I → ℕ - - |I| = I - |gl₁| = 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 + 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 @@ -62,16 +56,12 @@ module PartialShapeShape where gl₁ : I → SourceShape gl₂ : I → ViewShape - |I| = I - |gl₁| = 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 + 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) diff --git a/Precond.agda b/Precond.agda index 852480d..e39397c 100644 --- a/Precond.agda +++ b/Precond.agda @@ -63,31 +63,31 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.A maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup i h) ∎ inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (fromFunc g)) f≢i) -assoc-enough : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Get.SourceContainer G Carrier (Get.|gl₁| G i)) → (v : Get.ViewContainer G Carrier (Get.|gl₂| G j)) → ∃ (λ h → assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.|gl₁| G j)))) (Shaped.content (Get.ViewShapeT G) v) ≡ just h) → ∃ λ u → bff G j s v ≡ just u -assoc-enough G {i} j s v (h , p) = _ , cong (_<$>_ ((λ f → fmapS f t) ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Shaped.arity SourceShapeT (|gl₁| j))))) p +assoc-enough : (G : Get) → {i : Get.I G} → (j : Get.I G) → (s : Get.SourceContainer G Carrier (Get.gl₁ G i)) → (v : Get.ViewContainer G Carrier (Get.gl₂ G j)) → ∃ (λ h → assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.gl₁ G j)))) (Shaped.content (Get.ViewShapeT G) v) ≡ just h) → ∃ λ u → bff G j s v ≡ just u +assoc-enough G {i} j s v (h , p) = _ , cong (_<$>_ ((λ f → fmapS f t) ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Shaped.arity SourceShapeT (gl₁ j))))) p where open Get G - g′ = delete-many (Shaped.content ViewShapeT (get (enumerate SourceShapeT (|gl₁| i)))) (fromFunc (denumerate SourceShapeT s)) - t = enumerate SourceShapeT (|gl₁| j) + g′ = delete-many (Shaped.content ViewShapeT (get (enumerate SourceShapeT (gl₁ i)))) (fromFunc (denumerate SourceShapeT s)) + t = enumerate SourceShapeT (gl₁ j) -assoc-enough′ : (G : Get) → {i : Get.|I| G} → (s : Get.SourceContainer G Carrier (Get.|gl₁| G i)) → (v : Get.ViewContainer G Carrier (Get.|gl₂| G i)) → ∃ (λ h → assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.|gl₁| G i)))) (Shaped.content (Get.ViewShapeT G) v) ≡ just h) → ∃ λ u → bff G i s v ≡ just (Get.fmapS G just u) +assoc-enough′ : (G : Get) → {i : Get.I G} → (s : Get.SourceContainer G Carrier (Get.gl₁ G i)) → (v : Get.ViewContainer G Carrier (Get.gl₂ G i)) → ∃ (λ h → assoc (Shaped.content (Get.ViewShapeT G) (Get.get G (enumerate (Get.SourceShapeT G) (Get.gl₁ G i)))) (Shaped.content (Get.ViewShapeT G) v) ≡ just h) → ∃ λ u → bff G i s v ≡ just (Get.fmapS G just u) assoc-enough′ G {i} s v (h , p) = _ , (begin bff G i s v ≡⟨ proj₂ (assoc-enough G i s v (h , p)) ⟩ - just (fmapS (flip lookupM (union h (reshape g′ (Shaped.arity SourceShapeT (|gl₁| i))))) t) + just (fmapS (flip lookupM (union h (reshape g′ (Shaped.arity SourceShapeT (gl₁ i))))) t) ≡⟨ cong just (begin _ ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩ fmapS (flip lookupM (union h g′)) t ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM) (proj₂ wp) ⟩ fmapS (flip lookupM (fromFunc (proj₁ wp))) t - ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (|gl₁| i)) (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩ + ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩ fmapS (Maybe.just ∘ proj₁ wp) t - ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (|gl₁| i)) just (proj₁ wp) t ⟩ + ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (gl₁ i)) just (proj₁ wp) t ⟩ fmapS Maybe.just (fmapS (proj₁ wp) t) ∎) ⟩ _ ∎) where open Get G - s′ = enumerate SourceShapeT (|gl₁| i) + s′ = enumerate SourceShapeT (gl₁ i) g = fromFunc (denumerate SourceShapeT s) g′ = delete-many (Shaped.content ViewShapeT (get s′)) g - t = enumerate SourceShapeT (|gl₁| i) + t = enumerate SourceShapeT (gl₁ i) wp = lemma-union-delete-fromFunc (lemma-assoc-domain (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT v) p) data All-different {A : Set} : List A → Set where -- cgit v1.2.3