@@ -35,10 +35,8 @@ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
3535open import Data.Sum.Function.Propositional using (_⊎-cong_)
3636open import Effect.Monad
3737open import Function.Base
38- open import Function.Equality using (_⟨$⟩_)
39- open import Function.Equivalence using (_⇔_; equivalence; Equivalence)
40- open import Function.Inverse as Inv using (_↔_; inverse; Inverse)
41- open import Function.Related as Related using (Kind; Related; SK-sym)
38+ open import Function.Bundles
39+ open import Function.Related.Propositional as Related using (Kind; Related)
4240open import Level using (Level)
4341open import Relation.Binary as B hiding (_⇔_)
4442open import Relation.Binary.PropositionalEquality as P
@@ -55,9 +53,7 @@ private
5553private
5654 variable
5755 a b c p q r ℓ : Level
58- A : Set a
59- B : Set b
60- C : Set c
56+ A B C : Set a
6157 P Q R : Pred A p
6258 x y : A
6359 xs ys : List A
@@ -89,8 +85,8 @@ Any-cong : ∀ {k : Kind} → (∀ x → Related k (P x) (Q x)) →
8985 (∀ {z} → Related k (z ∈ xs) (z ∈ ys)) →
9086 Related k (Any P xs) (Any Q ys)
9187Any-cong {P = P} {Q = Q} {xs = xs} {ys} P↔Q xs≈ys =
92- Any P xs ↔⟨ SK-sym Any↔ ⟩
93- (∃ λ x → x ∈ xs × P x) ∼⟨ Σ.cong Inv.id (xs≈ys ×-cong P↔Q _) ⟩
88+ Any P xs ↔⟨ Related. SK-sym Any↔ ⟩
89+ (∃ λ x → x ∈ xs × P x) ∼⟨ {!!} ⟩ -- Σ.cong ? ? ⟩ -- (xs≈ys ×-cong P↔Q _) ⟩ -- Inv.id
9490 (∃ λ x → x ∈ ys × Q x) ↔⟨ Any↔ ⟩
9591 Any Q ys ∎
9692 where open Related.EquationalReasoning
@@ -146,38 +142,38 @@ swap-invol (there pxys) =
146142
147143swap↔ : ∀ {P : A → B → Set ℓ} →
148144 Any (λ x → Any (P x) ys) xs ↔ Any (λ y → Any (flip P y) xs) ys
149- swap↔ = inverse swap swap swap-invol swap-invol
145+ swap↔ = mk↔′ swap swap swap-invol swap-invol
150146
151147------------------------------------------------------------------------
152148-- Lemmas relating Any to ⊥
153149
154150⊥↔Any⊥ : ⊥ ↔ Any (const ⊥) xs
155- ⊥↔Any⊥ = inverse (λ ()) (λ p → from p) (λ ()) ( λ p → from p)
151+ ⊥↔Any⊥ = mk↔′ (λ ()) (λ p → from p) (λ p → from p) ( λ () )
156152 where
157153 from : Any (const ⊥) xs → B
158154 from (there p) = from p
159155
160156⊥↔Any[] : ⊥ ↔ Any P []
161- ⊥↔Any[] = inverse (λ ()) (λ ()) (λ ()) (λ ())
157+ ⊥↔Any[] = mk↔′ (λ ()) (λ ()) (λ ()) (λ ())
162158
163159------------------------------------------------------------------------
164160-- Lemmas relating Any to ⊤
165161
166162-- These introduction and elimination rules are not inverses, though.
167163
168164any⁺ : ∀ (p : A → Bool) → Any (T ∘ p) xs → T (any p xs)
169- any⁺ p (here px) = Equivalence.from T-∨ ⟨$⟩ inj₁ px
165+ any⁺ p (here px) = Equivalence.from T-∨ ( inj₁ px)
170166any⁺ p (there {x = x} pxs) with p x
171167... | true = _
172168... | false = any⁺ p pxs
173169
174170any⁻ : ∀ (p : A → Bool) xs → T (any p xs) → Any (T ∘ p) xs
175171any⁻ p (x ∷ xs) px∷xs with p x | inspect p x
176- ... | true | P.[ eq ] = here (Equivalence.from T-≡ ⟨$⟩ eq)
172+ ... | true | P.[ eq ] = here (Equivalence.from T-≡ eq)
177173... | false | _ = there (any⁻ p xs px∷xs)
178174
179175any⇔ : ∀ {p : A → Bool} → Any (T ∘ p) xs ⇔ T (any p xs)
180- any⇔ = equivalence (any⁺ _) (any⁻ _ _)
176+ any⇔ = mk⇔ (any⁺ _) (any⁻ _ _)
181177
182178------------------------------------------------------------------------
183179-- Sums commute with Any
@@ -191,7 +187,7 @@ Any-⊎⁻ (here (inj₂ q)) = inj₂ (here q)
191187Any-⊎⁻ (there p) = Sum.map there there (Any-⊎⁻ p)
192188
193189⊎↔ : (Any P xs ⊎ Any Q xs) ↔ Any (λ x → P x ⊎ Q x) xs
194- ⊎↔ {P = P} {Q = Q} = inverse Any-⊎⁺ Any-⊎⁻ from∘to to ∘from
190+ ⊎↔ {P = P} {Q = Q} = mk↔′ Any-⊎⁺ Any-⊎⁻ to ∘from from∘to
195191 where
196192 from∘to : (p : Any P xs ⊎ Any Q xs) → Any-⊎⁻ (Any-⊎⁺ p) ≡ p
197193 from∘to (inj₁ (here p)) = refl
@@ -203,8 +199,8 @@ Any-⊎⁻ (there p) = Sum.map there there (Any-⊎⁻ p)
203199 to∘from (here (inj₁ p)) = refl
204200 to∘from (here (inj₂ q)) = refl
205201 to∘from (there p) with Any-⊎⁻ p | to∘from p
206- to∘from (there .(Any.map inj₁ p)) | inj₁ p | refl = refl
207- to∘from (there .(Any.map inj₂ q)) | inj₂ q | refl = refl
202+ ... | inj₁ p | refl = refl
203+ ... | inj₂ q | refl = refl
208204
209205------------------------------------------------------------------------
210206-- Products "commute" with Any.
@@ -219,7 +215,7 @@ Any-×⁻ pq with Prod.map₂ (Prod.map₂ find) (find pq)
219215
220216×↔ : ∀ {xs ys} →
221217 (Any P xs × Any Q ys) ↔ Any (λ x → Any (λ y → P x × Q y) ys) xs
222- ×↔ {P = P} {Q = Q} {xs} {ys} = inverse Any-×⁺ Any-×⁻ from∘to to ∘from
218+ ×↔ {P = P} {Q = Q} {xs} {ys} = mk↔′ Any-×⁺ Any-×⁻ to ∘from from∘to
223219 where
224220 open P.≡-Reasoning
225221
@@ -258,8 +254,7 @@ Any-×⁻ pq with Prod.map₂ (Prod.map₂ find) (find pq)
258254
259255
260256 to∘from : ∀ pq → Any-×⁺ {xs = xs} (Any-×⁻ pq) ≡ pq
261- to∘from pq
262- with find pq
257+ to∘from pq with find pq
263258 | (λ (f : (proj₁ (find pq) ≡_) ⋐ _) → map∘find pq {f})
264259 ... | (x , x∈xs , pq′) | lem₁
265260 with find pq′
@@ -327,7 +322,7 @@ module _ {f : A → B} where
327322 map⁻∘map⁺ P (there p) = P.cong there (map⁻∘map⁺ P p)
328323
329324 map↔ : Any (P ∘ f) xs ↔ Any P (List.map f xs)
330- map↔ = inverse map⁺ map⁻ (map⁻∘map⁺ _) map⁺∘map⁻
325+ map↔ = mk↔′ map⁺ map⁻ map⁺∘map⁻ (map⁻∘map⁺ _)
331326
332327 gmap : P ⋐ Q ∘ f → Any P ⋐ Any Q ∘ map f
333328 gmap g = map⁺ ∘ Any.map g
@@ -376,7 +371,7 @@ module _ {P : A → Set p} where
376371 ++⁻∘++⁺ (x ∷ xs) (inj₂ p) rewrite ++⁻∘++⁺ xs (inj₂ p) = refl
377372
378373 ++↔ : ∀ {xs ys} → (Any P xs ⊎ Any P ys) ↔ Any P (xs ++ ys)
379- ++↔ {xs = xs} = inverse [ ++⁺ˡ , ++⁺ʳ xs ]′ (++⁻ xs) (++⁻ ∘++⁺ xs) (++⁺ ∘++⁻ xs)
374+ ++↔ {xs = xs} = mk↔′ [ ++⁺ˡ , ++⁺ʳ xs ]′ (++⁻ xs) (++⁺ ∘++⁻ xs) (++⁻ ∘++⁺ xs)
380375
381376 ++-comm : ∀ xs ys → Any P (xs ++ ys) → Any P (ys ++ xs)
382377 ++-comm xs ys = [ ++⁺ʳ ys , ++⁺ˡ ]′ ∘ ++⁻ xs
@@ -398,8 +393,8 @@ module _ {P : A → Set p} where
398393 | ++⁻∘++⁺ ys {ys = x ∷ xs} (inj₁ p) = refl
399394
400395 ++↔++ : ∀ xs ys → Any P (xs ++ ys) ↔ Any P (ys ++ xs)
401- ++↔++ xs ys = inverse (++-comm xs ys) (++-comm ys xs)
402- (++-comm∘++-comm xs ) (++-comm∘++-comm ys)
396+ ++↔++ xs ys = mk↔′ (++-comm xs ys) (++-comm ys xs)
397+ (++-comm∘++-comm ys ) (++-comm∘++-comm xs)
403398
404399 ++-insert : ∀ xs {ys} → P x → Any P (xs ++ [ x ] ++ ys)
405400 ++-insert xs Px = ++⁺ʳ xs (++⁺ˡ (singleton⁺ Px))
@@ -446,7 +441,7 @@ module _ {P : A → Set p} where
446441 P.cong there $ concat⁻∘concat⁺ p
447442
448443 concat↔ : ∀ {xss} → Any (Any P) xss ↔ Any P (concat xss)
449- concat↔ {xss} = inverse concat⁺ (concat⁻ xss) concat⁻∘concat⁺ (concat⁺∘concat⁻ xss)
444+ concat↔ {xss} = mk↔′ concat⁺ (concat⁻ xss) (concat⁺∘concat⁻ xss) concat⁻∘concat⁺
450445
451446------------------------------------------------------------------------
452447-- cartesianProductWith
@@ -496,18 +491,16 @@ applyUpTo⁻ f {suc n} (there p) with applyUpTo⁻ (f ∘ suc) p
496491------------------------------------------------------------------------
497492-- applyDownFrom
498493
499- module _ {P : A → Set p} where
500-
501- applyDownFrom⁺ : ∀ f {i n} → P (f i) → i < n → Any P (applyDownFrom f n)
502- applyDownFrom⁺ f {i} {suc n} p (s≤s i≤n) with i ≟ n
503- ... | yes P.refl = here p
504- ... | no i≢n = there (applyDownFrom⁺ f p (≤∧≢⇒< i≤n i≢n))
494+ applyDownFrom⁺ : ∀ f {i n} → P (f i) → i < n → Any P (applyDownFrom f n)
495+ applyDownFrom⁺ f {i} {suc n} p (s≤s i≤n) with i ≟ n
496+ ... | yes P.refl = here p
497+ ... | no i≢n = there (applyDownFrom⁺ f p (≤∧≢⇒< i≤n i≢n))
505498
506- applyDownFrom⁻ : ∀ f {n} → Any P (applyDownFrom f n) →
507- ∃ λ i → i < n × P (f i)
508- applyDownFrom⁻ f {suc n} (here p) = n , ≤-refl , p
509- applyDownFrom⁻ f {suc n} (there p) with applyDownFrom⁻ f p
510- ... | i , i<n , pf = i , m<n⇒m<1+n i<n , pf
499+ applyDownFrom⁻ : ∀ f {n} → Any P (applyDownFrom f n) →
500+ ∃ λ i → i < n × P (f i)
501+ applyDownFrom⁻ f {suc n} (here p) = n , ≤-refl , p
502+ applyDownFrom⁻ f {suc n} (there p) with applyDownFrom⁻ f p
503+ ... | i , i<n , pf = i , m<n⇒m<1+n i<n , pf
511504
512505------------------------------------------------------------------------
513506-- tabulate
@@ -601,7 +594,7 @@ module _ {P : B → Set p} where
601594
602595 mapWith∈↔ : ∀ {xs : List A} {f : ∀ {x} → x ∈ xs → B} →
603596 (∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) ↔ Any P (mapWith∈ xs f)
604- mapWith∈↔ = inverse (mapWith∈⁺ _) (mapWith∈⁻ _ _) (from∘to _ ) (to∘ from _ _)
597+ mapWith∈↔ = mk↔′ (mapWith∈⁺ _) (mapWith∈⁻ _ _) (to∘from _ _ ) (from∘to _)
605598 where
606599 from∘to : ∀ {xs : List A} (f : ∀ {x} → x ∈ xs → B)
607600 (p : ∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) →
@@ -644,34 +637,30 @@ reverse⁻ ps with reverseAcc⁻ [] _ ps
644637------------------------------------------------------------------------
645638-- pure
646639
647- module _ {P : A → Set p} where
648-
649- pure⁺ : P x → Any P (pure x)
650- pure⁺ = here
640+ pure⁺ : P x → Any P (pure x)
641+ pure⁺ = here
651642
652- pure⁻ : Any P (pure x) → P x
653- pure⁻ (here p) = p
643+ pure⁻ : Any P (pure x) → P x
644+ pure⁻ (here p) = p
654645
655- pure⁺∘pure⁻ : (p : Any P (pure x)) → pure⁺ (pure⁻ p) ≡ p
656- pure⁺∘pure⁻ (here p) = refl
646+ pure⁺∘pure⁻ : (p : Any P (pure x)) → pure⁺ (pure⁻ p) ≡ p
647+ pure⁺∘pure⁻ (here p) = refl
657648
658- pure⁻∘pure⁺ : (p : P x) → pure⁻ (pure⁺ p) ≡ p
659- pure⁻∘pure⁺ p = refl
649+ pure⁻∘pure⁺ : (p : P x) → pure⁻ {P = P} (pure⁺ p) ≡ p
650+ pure⁻∘pure⁺ p = refl
660651
661- pure↔ : P x ↔ Any P (pure x)
662- pure↔ = inverse pure⁺ pure⁻ pure⁻ ∘pure⁺ pure⁺ ∘pure⁻
652+ pure↔ : P x ↔ Any P (pure x)
653+ pure↔ {P = P} = mk↔′ pure⁺ pure⁻ pure⁺ ∘pure⁻ ( pure⁻ ∘pure⁺ {P = P})
663654
664655------------------------------------------------------------------------
665656-- _∷_
666657
667- module _ (P : Pred A p) where
668-
669- ∷↔ : (P x ⊎ Any P xs) ↔ Any P (x ∷ xs)
670- ∷↔ {x = x} {xs} =
671- (P x ⊎ Any P xs) ↔⟨ pure↔ {P = P} ⊎-cong (Any P xs ∎) ⟩
672- (Any P [ x ] ⊎ Any P xs) ↔⟨ ++↔ {P = P} {xs = [ x ]} ⟩
673- Any P (x ∷ xs) ∎
674- where open Related.EquationalReasoning
658+ ∷↔ : (P : Pred A p) → (P x ⊎ Any P xs) ↔ Any P (x ∷ xs)
659+ ∷↔ {x = x} {xs} P =
660+ (P x ⊎ Any P xs) ↔⟨ pure↔ ⊎-cong (Any P xs ∎) ⟩
661+ (Any P [ x ] ⊎ Any P xs) ↔⟨ ++↔ ⟩
662+ Any P (x ∷ xs) ∎
663+ where open Related.EquationalReasoning
675664
676665------------------------------------------------------------------------
677666-- _>>=_
@@ -695,16 +684,15 @@ module _ {A B : Set ℓ} {P : B → Set p} {f : A → List B} where
695684 Any (λ f → Any (Any P ∘ pure ∘ f) xs) fs ↔⟨ Any-cong (λ _ → >>=↔ ) (_ ∎) ⟩
696685 Any (λ f → Any P (xs >>= pure ∘ f)) fs ↔⟨ >>=↔ ⟩
697686 Any P (fs >>= λ f → xs >>= λ x → pure (f x)) ≡˘⟨ P.cong (Any P) (Listₑ.Applicative.unfold-⊛ fs xs) ⟩
698- Any P (fs ⊛ xs) ∎
687+ Any P (fs ⊛ xs) ∎
699688 where open Related.EquationalReasoning
700689
690+
701691-- An alternative introduction rule for _⊛_
702692
703- ⊛⁺′ : ∀ {P : A → Set ℓ} {Q : B → Set ℓ} {fs : List (A → B)} {xs} →
693+ ⊛⁺′ : ∀ {P : Pred A ℓ} {Q : Pred B ℓ} {fs : List (A → B)} {xs} →
704694 Any (P ⟨→⟩ Q) fs → Any P xs → Any Q (fs ⊛ xs)
705- ⊛⁺′ pq p =
706- Inverse.to ⊛↔ ⟨$⟩
707- Any.map (λ pq → Any.map (λ {x} → pq {x}) p) pq
695+ ⊛⁺′ pq p = Inverse.to ⊛↔ (Any.map (λ pq → Any.map (λ {x} → pq {x}) p) pq)
708696
709697------------------------------------------------------------------------
710698-- _⊗_
0 commit comments