------------------------------------------------------------------------ -- Containers, including a definition of bag equivalence ------------------------------------------------------------------------ {-# OPTIONS --without-K #-} module Container where open import Bag-equivalence using (Kind; bag) open import Equivalence hiding (id; _∘_; inverse) open import Equality.Propositional open import Prelude hiding (id; List; map; lookup) import Bijection open Bijection equality-with-J using (_↔_; module _↔_) private module Function-universe where import Function-universe open Function-universe equality-with-J public open Function-universe hiding (inverse; Kind) renaming (_∘_ to _⟨∘⟩_) import H-level.Closure open H-level.Closure equality-with-J ------------------------------------------------------------------------ -- Containers record Container c : Set (lsuc c) where constructor _▷_ field Shape : Set c Position : Shape → Set c open Container public -- Interpretation of containers. ⟦_⟧ : ∀ {c ℓ} → Container c → Set ℓ → Set _ ⟦ S ▷ P ⟧ A = ∃ λ (s : S) → (P s → A) ------------------------------------------------------------------------ -- Some projections -- The shape of something. shape : ∀ {a c} {A : Set a} {C : Container c} → ⟦ C ⟧ A → Shape C shape = proj₁ -- A lookup function. lookup : ∀ {a c} {A : Set a} {C : Container c} (xs : ⟦ C ⟧ A) → Position C (shape xs) → A lookup = proj₂ ------------------------------------------------------------------------ -- Map -- Containers are functors. map : ∀ {c x y} {C : Container c} {X : Set x} {Y : Set y} → (X → Y) → ⟦ C ⟧ X → ⟦ C ⟧ Y map f = Σ-map id (λ g → f ∘ g) module Map where identity : ∀ {c x} {C : Container c} {X : Set x} (xs : ⟦ C ⟧ X) → map id xs ≡ xs identity xs = refl composition : ∀ {c x y z} {C : Container c} {X : Set x} {Y : Set y} {Z : Set z} (f : Y → Z) (g : X → Y) (xs : ⟦ C ⟧ X) → map f (map g xs) ≡ map (f ∘ g) xs composition f g xs = refl -- Naturality. Natural : ∀ {c₁ c₂ a} {C₁ : Container c₁} {C₂ : Container c₂} → ({A : Set a} → ⟦ C₁ ⟧ A → ⟦ C₂ ⟧ A) → Set (c₁ ⊔ c₂ ⊔ lsuc a) Natural function = ∀ {A B} (f : A → B) xs → map f (function xs) ≡ function (map f xs) -- Natural transformations. infixr 4 _[_]⟶_ record _[_]⟶_ {c₁ c₂} (C₁ : Container c₁) ℓ (C₂ : Container c₂) : Set (c₁ ⊔ c₂ ⊔ lsuc ℓ) where field function : {A : Set ℓ} → ⟦ C₁ ⟧ A → ⟦ C₂ ⟧ A natural : Natural function -- Natural isomorphisms. record _[_]↔_ {c₁ c₂} (C₁ : Container c₁) ℓ (C₂ : Container c₂) : Set (c₁ ⊔ c₂ ⊔ lsuc ℓ) where field isomorphism : {A : Set ℓ} → ⟦ C₁ ⟧ A ↔ ⟦ C₂ ⟧ A natural : Natural (_↔_.to isomorphism) -- Natural isomorphisms are natural transformations. natural-transformation : C₁ [ ℓ ]⟶ C₂ natural-transformation = record { function = _↔_.to isomorphism ; natural = natural } -- Natural isomorphisms can be inverted. inverse : C₂ [ ℓ ]↔ C₁ inverse = record { isomorphism = Function-universe.inverse isomorphism ; natural = λ f xs → map f (from xs) ≡⟨ sym \$ left-inverse-of _ ⟩ from (to (map f (from xs))) ≡⟨ sym \$ cong from \$ natural f (from xs) ⟩ from (map f (to (from xs))) ≡⟨ cong (from ∘ map f) \$ right-inverse-of _ ⟩∎ from (map f xs) ∎ } where open module I {A : Set ℓ} = _↔_ (isomorphism {A = A}) open Function-universe using (inverse) ------------------------------------------------------------------------ -- Any, _∈_, bag equivalence and similar relations -- Definition of Any for containers. Any : ∀ {a c p} {A : Set a} {C : Container c} → (A → Set p) → (⟦ C ⟧ A → Set (c ⊔ p)) Any {C = S ▷ P} Q (s , f) = ∃ λ (p : P s) → Q (f p) -- Membership predicate. infix 4 _∈_ _∈_ : ∀ {a c} {A : Set a} {C : Container c} → A → ⟦ C ⟧ A → Set _ x ∈ xs = Any (λ y → x ≡ y) xs -- Bag equivalence etc. Note that the containers can be different as -- long as the elements they contain have equal types. infix 4 _∼[_]_ _∼[_]_ : ∀ {a c₁ c₂} {A : Set a} {C₁ : Container c₁} {C₂ : Container c₂} → ⟦ C₁ ⟧ A → Kind → ⟦ C₂ ⟧ A → Set _ xs ∼[ k ] ys = ∀ z → z ∈ xs ↝[ k ] z ∈ ys -- Bag equivalence. infix 4 _≈-bag_ _≈-bag_ : ∀ {a c₁ c₂} {A : Set a} {C₁ : Container c₁} {C₂ : Container c₂} → ⟦ C₁ ⟧ A → ⟦ C₂ ⟧ A → Set _ xs ≈-bag ys = xs ∼[ bag ] ys ------------------------------------------------------------------------ -- Various properties related to Any, _∈_ and _∼[_]_ -- Lemma relating Any to map. Any-map : ∀ {a b c p} {A : Set a} {B : Set b} {C : Container c} (P : B → Set p) (f : A → B) (xs : ⟦ C ⟧ A) → Any P (map f xs) ↔ Any (P ∘ f) xs Any-map P f xs = Any P (map f xs) □ -- Any can be expressed using _∈_. Any-∈ : ∀ {a c p} {A : Set a} {C : Container c} (P : A → Set p) (xs : ⟦ C ⟧ A) → Any P xs ↔ ∃ λ x → P x × x ∈ xs Any-∈ P (s , f) = (∃ λ p → P (f p)) ↔⟨ ∃-cong (λ p → ∃-intro P (f p)) ⟩ (∃ λ p → ∃ λ x → P x × x ≡ f p) ↔⟨ ∃-comm ⟩ (∃ λ x → ∃ λ p → P x × x ≡ f p) ↔⟨ ∃-cong (λ _ → ∃-comm) ⟩ (∃ λ x → P x × ∃ λ p → x ≡ f p) □ -- Using this property we can prove that Any and _⊎_ commute. Any-⊎ : ∀ {a c p q} {A : Set a} {C : Container c} (P : A → Set p) (Q : A → Set q) (xs : ⟦ C ⟧ A) → Any (λ x → P x ⊎ Q x) xs ↔ Any P xs ⊎ Any Q xs Any-⊎ P Q xs = Any (λ x → P x ⊎ Q x) xs ↔⟨ Any-∈ (λ x → P x ⊎ Q x) xs ⟩ (∃ λ x → (P x ⊎ Q x) × x ∈ xs) ↔⟨ ∃-cong (λ x → ×-⊎-distrib-right) ⟩ (∃ λ x → P x × x ∈ xs ⊎ Q x × x ∈ xs) ↔⟨ ∃-⊎-distrib-left ⟩ (∃ λ x → P x × x ∈ xs) ⊎ (∃ λ x → Q x × x ∈ xs) ↔⟨ inverse \$ Any-∈ P xs ⊎-cong Any-∈ Q xs ⟩ Any P xs ⊎ Any Q xs □ -- Any preserves functions of various kinds and respects bag -- equivalence and similar relations. Any-cong : ∀ {k a c d p q} {A : Set a} {C : Container c} {D : Container d} (P : A → Set p) (Q : A → Set q) (xs : ⟦ C ⟧ A) (ys : ⟦ D ⟧ A) → (∀ x → P x ↝[ k ] Q x) → xs ∼[ k ] ys → Any P xs ↝[ k ] Any Q ys Any-cong P Q xs ys P↔Q xs∼ys = Any P xs ↔⟨ Any-∈ P xs ⟩ (∃ λ z → P z × z ∈ xs) ↝⟨ ∃-cong (λ z → P↔Q z ×-cong xs∼ys z) ⟩ (∃ λ z → Q z × z ∈ ys) ↔⟨ inverse (Any-∈ Q ys) ⟩ Any Q ys □ -- Map preserves the relations. map-cong : ∀ {k a b c d} {A : Set a} {B : Set b} {C : Container c} {D : Container d} (f : A → B) (xs : ⟦ C ⟧ A) (ys : ⟦ D ⟧ A) → xs ∼[ k ] ys → map f xs ∼[ k ] map f ys map-cong f xs ys xs∼ys = λ z → z ∈ map f xs ↔⟨ Any-map (_≡_ z) f xs ⟩ Any (λ x → z ≡ f x) xs ↝⟨ Any-cong _ _ xs ys (λ x → z ≡ f x □) xs∼ys ⟩ Any (λ x → z ≡ f x) ys ↔⟨ inverse (Any-map (_≡_ z) f ys) ⟩ z ∈ map f ys □ -- Lemma relating Any to if_then_else_. Any-if : ∀ {a c p} {A : Set a} {C : Container c} (P : A → Set p) (xs ys : ⟦ C ⟧ A) b → Any P (if b then xs else ys) ↔ T b × Any P xs ⊎ T (not b) × Any P ys Any-if P xs ys = inverse ∘ if-lemma (λ b → Any P (if b then xs else ys)) id id -- One can reconstruct (up to natural isomorphism) the shape set and -- the position predicate from the interpretation and the Any -- predicate transformer. -- -- (The following lemmas were suggested by an anonymous reviewer.) Shape′ : ∀ {c} → (Set → Set c) → Set c Shape′ F = F ⊤ Shape-⟦⟧ : ∀ {c} (C : Container c) → Shape C ↔ Shape′ ⟦ C ⟧ Shape-⟦⟧ C = Shape C ↔⟨ inverse ×-right-identity ⟩ Shape C × ⊤ ↔⟨ ∃-cong (λ _ → inverse →-right-zero) ⟩ (∃ λ (s : Shape C) → Position C s → ⊤) □ Position′ : ∀ {c} (F : Set → Set c) → ({A : Set} → (A → Set) → (F A → Set c)) → Shape′ F → Set c Position′ _ Any = Any (λ (_ : ⊤) → ⊤) Position-Any : ∀ {c} {C : Container c} (s : Shape C) → Position C s ↔ Position′ ⟦ C ⟧ Any (_↔_.to (Shape-⟦⟧ C) s) Position-Any {C = C} s = Position C s ↔⟨ inverse ×-right-identity ⟩ Position C s × ⊤ □ expressed-in-terms-of-interpretation-and-Any : ∀ {c ℓ} (C : Container c) → C [ ℓ ]↔ (⟦ C ⟧ ⊤ ▷ Any (λ _ → ⊤)) expressed-in-terms-of-interpretation-and-Any C = record { isomorphism = λ {A} → (∃ λ (s : Shape C) → Position C s → A) ↔⟨ Σ-cong (Shape-⟦⟧ C) (λ _ → lemma) ⟩ (∃ λ (s : Shape′ ⟦ C ⟧) → Position′ ⟦ C ⟧ Any s → A) □ ; natural = λ _ _ → refl } where -- If equality of functions had been extensional, then the following -- lemma could have been replaced by a congruence lemma applied to -- Position-Any. lemma : ∀ {a b} {A : Set a} {B : Set b} → (B → A) ↔ (B × ⊤ → A) lemma = record { surjection = record { equivalence = record { to = λ { f (p , tt) → f p } ; from = λ f p → f (p , tt) } ; right-inverse-of = λ _ → refl } ; left-inverse-of = λ _ → refl } ------------------------------------------------------------------------ -- Alternative definition of bag equivalence -- Two things are bag equal if there is a bijection between their -- positions which relates equal things. infix 4 _≈-bag′_ _≈-bag′_ : ∀ {a c d} {A : Set a} {C : Container c} {D : Container d} → ⟦ C ⟧ A → ⟦ D ⟧ A → Set _ _≈-bag′_ {C = C} {D} (s , f) (s′ , f′) = ∃ λ (P↔P : Position C s ↔ Position D s′) → (∀ p → f p ≡ f′ (to-implication P↔P p)) -- The definition is equivalent to the one given above. The proof is -- very similar to the one given in Bag-equivalence. -- Membership can be expressed as "there is an index which points to -- the element". In fact, membership /is/ expressed in this way, so -- this proof is unnecessary. ∈-lookup : ∀ {a c} {A : Set a} {C : Container c} {z} (xs : ⟦ C ⟧ A) → z ∈ xs ↔ ∃ λ p → z ≡ lookup xs p ∈-lookup {z = z} xs = z ∈ xs □ -- The index which points to the element (not used below). index : ∀ {a c} {A : Set a} {C : Container c} {z} (xs : ⟦ C ⟧ A) → z ∈ xs → Position C (shape xs) index xs = proj₁ ∘ to-implication (∈-lookup xs) -- The positions for a given shape can be expressed in terms of the -- membership predicate. Position-shape : ∀ {a c} {A : Set a} {C : Container c} (xs : ⟦ C ⟧ A) → (∃ λ z → z ∈ xs) ↔ Position C (shape xs) Position-shape {C = C} (s , f) = (∃ λ z → ∃ λ p → z ≡ f p) ↔⟨ ∃-comm ⟩ (∃ λ p → ∃ λ z → z ≡ f p) ↔⟨⟩ (∃ λ p → Singleton (f p)) ↔⟨ ∃-cong (λ _ → contractible↔⊤ (singleton-contractible _)) ⟩ Position C s × ⊤ ↔⟨ ×-right-identity ⟩ Position C s □ -- Position _ ∘ shape respects the various relations. Position-shape-cong : ∀ {k a c d} {A : Set a} {C : Container c} {D : Container d} (xs : ⟦ C ⟧ A) (ys : ⟦ D ⟧ A) → xs ∼[ k ] ys → Position C (shape xs) ↝[ k ] Position D (shape ys) Position-shape-cong {C = C} {D} xs ys xs∼ys = Position C (shape xs) ↔⟨ inverse \$ Position-shape xs ⟩ ∃ (λ z → z ∈ xs) ↝⟨ ∃-cong xs∼ys ⟩ ∃ (λ z → z ∈ ys) ↔⟨ Position-shape ys ⟩ Position D (shape ys) □ -- Furthermore Position-shape-cong relates equal elements. Position-shape-cong-relates : ∀ {a c d} {A : Set a} {C : Container c} {D : Container d} (xs : ⟦ C ⟧ A) (ys : ⟦ D ⟧ A) (xs≈ys : xs ≈-bag ys) p → lookup xs p ≡ lookup ys (to-implication (Position-shape-cong xs ys xs≈ys) p) Position-shape-cong-relates xs ys xs≈ys p = lookup xs p ≡⟨ proj₂ \$ to-implication (xs≈ys (lookup xs p)) (p , refl) ⟩ lookup ys (proj₁ \$ to-implication (xs≈ys (lookup xs p)) (p , refl)) ≡⟨ refl ⟩ lookup ys (_↔_.to (Position-shape ys) \$ Σ-map id (λ {z} → to-implication (xs≈ys z)) \$ _↔_.from (Position-shape xs) \$ p) ≡⟨ refl ⟩ lookup ys (_↔_.to (Position-shape ys) \$ to-implication (∃-cong xs≈ys) \$ _↔_.from (Position-shape xs) \$ p) ≡⟨ refl ⟩ lookup ys (to-implication ((from-bijection (Position-shape ys) ⟨∘⟩ ∃-cong xs≈ys) ⟨∘⟩ from-bijection (inverse \$ Position-shape xs)) p) ≡⟨ refl ⟩∎ lookup ys (to-implication (Position-shape-cong xs ys xs≈ys) p) ∎ -- We get that the two definitions of bag equivalence are equivalent. ≈⇔≈′ : ∀ {a c d} {A : Set a} {C : Container c} {D : Container d} (xs : ⟦ C ⟧ A) (ys : ⟦ D ⟧ A) → xs ≈-bag ys ⇔ xs ≈-bag′ ys ≈⇔≈′ xs ys = record { to = λ xs≈ys → ( Position-shape-cong xs ys xs≈ys , Position-shape-cong-relates xs ys xs≈ys ) ; from = from } where equality-lemma : ∀ {k a} {A : Set a} {x y z : A} → x ≡ y → (z ≡ x) ↝[ k ] (z ≡ y) equality-lemma {y = y} {z} refl = z ≡ y □ from : xs ≈-bag′ ys → xs ≈-bag ys from (P↔P , related) = λ z → z ∈ xs ↔⟨⟩ ∃ (λ p → z ≡ lookup xs p) ↝⟨ Σ-cong P↔P (λ p → equality-lemma (related p)) ⟩ ∃ (λ p → z ≡ lookup ys p) ↔⟨⟩ z ∈ ys □ ------------------------------------------------------------------------ -- Another alternative definition of bag equivalence -- A higher-order variant of _∼[_]_. Note that this definition is -- large (due to the quantification over predicates). infix 4 _∼[_]″_ _∼[_]″_ : ∀ {a c d} {A : Set a} {C : Container c} {D : Container d} → ⟦ C ⟧ A → Kind → ⟦ D ⟧ A → Set (lsuc a ⊔ c ⊔ d) _∼[_]″_ {a} {A = A} xs k ys = (P : A → Set a) → Any P xs ↝[ k ] Any P ys -- This definition is equivalent to _∼[_]_. ∼⇔∼″ : ∀ {k a c d} {A : Set a} {C : Container c} {D : Container d} (xs : ⟦ C ⟧ A) (ys : ⟦ D ⟧ A) → xs ∼[ k ] ys ⇔ xs ∼[ k ]″ ys ∼⇔∼″ xs ys = record { to = λ xs∼ys P → Any-cong P P xs ys (λ _ → id) xs∼ys ; from = λ Any-xs↝Any-ys z → Any-xs↝Any-ys (λ x → z ≡ x) }