Last active
June 13, 2024 13:16
-
-
Save clayrat/818acc30a02338bad29690ef499955ec to your computer and use it in GitHub Desktop.
Examples from QuotientHaskell paper in Cubical Agda (+ cubical-mini)
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# OPTIONS --safe #-} | |
| module qh where | |
| -- https://www.cs.nott.ac.uk/~pszgmh/quotient-haskell.pdf | |
| open import Prelude | |
| open import Meta.Prelude | |
| open import Data.Bool | |
| open import Data.Empty | |
| open import Data.Nat | |
| open import Data.List | |
| open import Data.Tree.Binary | |
| open import Data.Quotient.Set as SetQ | |
| module part2 where | |
| private variable | |
| A B : 𝒰 | |
| data Mobile (A : 𝒰) : 𝒰 where | |
| leaf : Mobile A | |
| node : A → Mobile A → Mobile A → Mobile A | |
| swap : (x : A) (l r : Mobile A) → node x l r ＝ node x r l | |
| sum : Mobile ℕ → ℕ | |
| sum leaf = 0 | |
| sum (node x l r) = x + sum l + sum r | |
| sum (swap x l r i) = +-assoc-comm x (sum l) (sum r) i | |
| mapM : (A → B) → Mobile A → Mobile B | |
| mapM f leaf = leaf | |
| mapM f (node x l r) = node (f x) (mapM f l) (mapM f r) | |
| mapM f (swap x l r i) = swap (f x) (mapM f l) (mapM f r) i | |
| fold : (f : A → B → B → B) | |
| → ((x : A) → (l r : B) → f x l r ＝ f x r l) | |
| → B → Mobile A → B | |
| fold f fp z leaf = z | |
| fold f fp z (node x l r) = f x (fold f fp z l) (fold f fp z r) | |
| fold f fp z (swap x l r i) = fp x (fold f fp z l) (fold f fp z r) i | |
| add3 : ℕ → ℕ → ℕ → ℕ | |
| add3 a b c = a + b + c | |
| sum′ : Mobile ℕ → ℕ | |
| sum′ = fold add3 +-assoc-comm 0 | |
| module part3 where | |
| private variable | |
| ℓ ℓ′ : Level | |
| A B : 𝒰 ℓ | |
| sum : Tree ℕ → ℕ | |
| sum empty = 0 | |
| sum (leaf x) = x | |
| sum (node l r) = sum l + sum r | |
| mapt : (A → B) → Tree A → Tree B | |
| mapt f empty = empty | |
| mapt f (leaf a) = leaf (f a) | |
| mapt f (node l r) = node (mapt f l) (mapt f r) | |
| filtert : (A → Bool) → Tree A → Tree A | |
| filtert f empty = empty | |
| filtert f (leaf x) = if f x then leaf x else empty | |
| filtert f (node l r) = node (filtert f l) (filtert f r) | |
| concat-map : (A → Tree B) → Tree A → Tree B | |
| concat-map f empty = empty | |
| concat-map f (leaf a) = f a | |
| concat-map f (node l r) = node (concat-map f l) (concat-map f r) | |
| count : (A → Bool) → Tree A → ℕ | |
| count p empty = 0 | |
| count p (leaf a) = if p a then 1 else 0 | |
| count p (node x y) = count p x + count p y | |
| has : (A → Bool) → Tree A → Bool | |
| has f empty = false | |
| has f (leaf x) = f x | |
| has f (node l r) = has f l or has f r | |
| -- lists | |
| private variable | |
| t x y z w : Tree A | |
| data _~_ {A : 𝒰 ℓ} : Tree A → Tree A → 𝒰 ℓ where | |
| eqt : x ~ x | |
| symt : x ~ y → y ~ x | |
| transt : x ~ y → y ~ z → x ~ z | |
| congr : x ~ y → z ~ w → node x z ~ node y w | |
| idl : node empty t ~ t | |
| idr : node t empty ~ t | |
| assoc : node (node x y) z ~ node x (node y z) | |
| prop : (p q : x ~ y) → p ＝ q | |
| instance | |
| H-Level-~ : {n : ℕ} → H-Level (suc n) (x ~ y) | |
| H-Level-~ = hlevel-prop-instance prop | |
| from-cat-rel : (l r : List A) | |
| → list→tree (l ++ r) | |
| ~ node (list→tree l) (list→tree r) | |
| from-cat-rel [] r = symt idl | |
| from-cat-rel (x ∷ l) r = transt (congr eqt (from-cat-rel l r)) (symt assoc) | |
| from-to-rel : (t : Tree A) → list→tree (tree→list t) ~ t | |
| from-to-rel empty = eqt | |
| from-to-rel (leaf x) = idr | |
| from-to-rel (node l r) = | |
| transt (from-cat-rel (tree→list l) (tree→list r)) | |
| (congr (from-to-rel l) (from-to-rel r)) | |
| ListQ : 𝒰 ℓ → 𝒰 ℓ | |
| ListQ A = Tree A / _~_ | |
| nilₗ : ListQ A | |
| nilₗ = ⦋ empty ⦌ | |
| consₗ : A → ListQ A → ListQ A | |
| consₗ x = SetQ.rec (hlevel 2) (⦋_⦌ ∘ node (leaf x)) λ a b r → glue/ _ _ (congr eqt r) | |
| concatₗ : ListQ A → ListQ A → ListQ A | |
| concatₗ = SetQ.rec² (hlevel 2) | |
| (λ lt rt → ⦋ node lt rt ⦌) | |
| (λ x y b r → glue/ _ _ (congr r eqt)) | |
| (λ a x y r → glue/ _ _ (congr eqt r)) | |
| concatₗ-id-l : (r : ListQ A) → concatₗ nilₗ r ＝ r | |
| concatₗ-id-l = elim! λ t → glue/ _ _ idl | |
| concatₗ-id-r : (l : ListQ A) → concatₗ l nilₗ ＝ l | |
| concatₗ-id-r = elim! λ t → glue/ _ _ idr | |
| concatₗ-assoc : (x y z : ListQ A) → concatₗ (concatₗ x y) z ＝ concatₗ x (concatₗ y z) | |
| concatₗ-assoc = elim! λ a b c → glue/ _ _ assoc | |
| list→treeₗ : List A → ListQ A | |
| list→treeₗ = ⦋_⦌ ∘ list→tree | |
| tree→list-rel : {A : Set ℓ} → (a b : Tree ⌞ A ⌟) → a ~ b → tree→list a ＝ tree→list b | |
| tree→list-rel a .a eqt = refl | |
| tree→list-rel {A} a b (symt x) = | |
| sym (tree→list-rel {A = A} b a x) | |
| tree→list-rel {A} a b (transt {y} l r) = | |
| tree→list-rel {A = A} a y l ∙ tree→list-rel {A = A} y b r | |
| tree→list-rel {A} .(node x z) .(node y w) (congr {x} {y} {z} {w} l r) = | |
| ap (λ q → q ++ tree→list z) (tree→list-rel {A = A} x y l) | |
| ∙ ap (λ q → tree→list y ++ q) (tree→list-rel {A = A} z w r) | |
| tree→list-rel .(node empty l) l idl = refl | |
| tree→list-rel .(node l empty) l idr = ++-id-r _ | |
| tree→list-rel .(node (node x y) z) .(node x (node y z)) (assoc {x} {y} {z}) = | |
| ++-assoc (tree→list x) (tree→list y) (tree→list z) | |
| tree→list-rel {A} x y (prop {x} {y} p q i) = | |
| list-is-of-hlevel 0 (n-Type.carrier-is-tr A) _ _ | |
| (tree→list-rel {A = A} x y p) (tree→list-rel {A = A} x y q) i | |
| tree→listₗ : {A : Set ℓ} → ListQ ⌞ A ⌟ → List ⌞ A ⌟ | |
| tree→listₗ {A} = SetQ.rec (hlevel 2) tree→list (tree→list-rel {A = A}) | |
| ListQ-eqv : {A : Set ℓ} → ListQ ⌞ A ⌟ ≃ List ⌞ A ⌟ | |
| ListQ-eqv {A} = ≅→≃ $ tree→listₗ , iso list→treeₗ list→tree→list li | |
| where | |
| li : list→treeₗ is-left-inverse-of (tree→listₗ {A = A}) | |
| li = elim! λ x → glue/ _ _ (from-to-rel x) | |
| ℕ-rel : (f : Tree A → ℕ) → | |
| (f empty ＝ 0) → | |
| (∀ x y → f (node x y) ＝ f x + f y) → | |
| (x y : Tree A) → x ~ y → f x ＝ f y | |
| ℕ-rel f fe fd a .a eqt = refl | |
| ℕ-rel f fe fd a b (symt r) = sym (ℕ-rel f fe fd b a r) | |
| ℕ-rel f fe fd a b (transt {y} l r) = | |
| ℕ-rel f fe fd a y l ∙ ℕ-rel f fe fd y b r | |
| ℕ-rel f fe fd .(node x z) .(node y w) (congr {x} {y} {z} {w} l r) = | |
| fd x z | |
| ∙ ap (λ q → q + f z) (ℕ-rel f fe fd x y l) | |
| ∙ ap (λ q → f y + q) (ℕ-rel f fe fd z w r) | |
| ∙ sym (fd y w) | |
| ℕ-rel f fe fd .(node empty b) b idl = | |
| fd empty b ∙ ap (λ q → q + f b) fe | |
| ℕ-rel f fe fd .(node b empty) b idr = | |
| fd b empty ∙ ap (λ q → f b + q) fe ∙ +-zero-r (f b) | |
| ℕ-rel f fe fd .(node (node x y) z) .(node x (node y z)) (assoc {x} {y} {z}) = | |
| fd (node x y) z | |
| ∙ ap (λ q → q + f z) (fd x y) | |
| ∙ sym (+-assoc (f x) (f y) (f z)) | |
| ∙ ap (λ q → f x + q) (sym $ fd y z) | |
| ∙ sym (fd x (node y z)) | |
| ℕ-rel f fe fd x y (prop {x} {y} p q i) = | |
| hlevel 2 _ _ (ℕ-rel f fe fd x y p) (ℕ-rel f fe fd x y q) i | |
| sumₗ : ListQ ℕ → ℕ | |
| sumₗ = SetQ.rec (hlevel 2) sum (ℕ-rel _ refl (λ x y → refl)) | |
| countₗ : (A → Bool) → ListQ A → ℕ | |
| countₗ f = SetQ.rec (hlevel 2) (count f) (ℕ-rel _ refl (λ x y → refl)) | |
| Bool-rel : (f : Tree A → Bool) → | |
| (f empty ＝ false) → | |
| (∀ x y → f (node x y) ＝ f x or f y) → | |
| (x y : Tree A) → x ~ y → f x ＝ f y | |
| Bool-rel f fe fd a .a eqt = refl | |
| Bool-rel f fe fd a b (symt r) = | |
| sym (Bool-rel f fe fd b a r) | |
| Bool-rel f fe fd a b (transt {y} l r) = | |
| Bool-rel f fe fd a y l ∙ Bool-rel f fe fd y b r | |
| Bool-rel f fe fd .(node x z) .(node y w) (congr {x} {y} {z} {w} l r) = | |
| fd x z | |
| ∙ ap (λ q → q or f z) (Bool-rel f fe fd x y l) | |
| ∙ ap (λ q → f y or q) (Bool-rel f fe fd z w r) | |
| ∙ sym (fd y w) | |
| Bool-rel f fe fd .(node empty b) b idl = | |
| fd empty b ∙ ap (λ q → q or f b) fe | |
| Bool-rel f fe fd .(node b empty) b idr = | |
| fd b empty ∙ ap (λ q → f b or q) fe ∙ or-id-r (f b) | |
| Bool-rel f fe fd .(node (node x y) z) .(node x (node y z)) (assoc {x} {y} {z}) = | |
| fd (node x y) z | |
| ∙ ap (λ q → q or f z) (fd x y) | |
| ∙ or-assoc (f x) (f y) (f z) | |
| ∙ ap (λ q → f x or q) (sym $ fd y z) | |
| ∙ sym (fd x (node y z)) | |
| Bool-rel f fe fd x y (prop {x} {y} p q i) = | |
| hlevel 2 _ _ (Bool-rel f fe fd x y p) (Bool-rel f fe fd x y q) i | |
| hasₗ : (A → Bool) → ListQ A → Bool | |
| hasₗ f = SetQ.rec (hlevel 2) (has f) (Bool-rel _ refl (λ x y → refl)) | |
| fun-rel : (f : Tree A → Tree B) → | |
| (f empty ＝ empty) → | |
| (∀ x y → f (node x y) ＝ node (f x) (f y)) → | |
| (x y : Tree A) → x ~ y → f x ~ f y | |
| fun-rel f fe fd a .a eqt = eqt | |
| fun-rel f fe fd a b (symt r) = | |
| symt (fun-rel f fe fd b a r) | |
| fun-rel f fe fd a b (transt {y} l r) = | |
| transt (fun-rel f fe fd a y l) (fun-rel f fe fd y b r) | |
| fun-rel f fe fd .(node x z) .(node y w) (congr {x} {y} {z} {w} l r) = | |
| transport | |
| (sym $ ap (λ q → f (node x z) ~ q) (fd y w) ∙ ap (λ q → q ~ node (f y) (f w)) (fd x z)) | |
| (congr (fun-rel f fe fd x y l) (fun-rel f fe fd z w r)) | |
| fun-rel f fe fd .(node empty b) b idl = | |
| transport | |
| (sym $ ap (λ q → q ~ f b) (fd empty b ∙ ap (λ q → node q (f b)) fe)) | |
| idl | |
| fun-rel f fe fd .(node b empty) b idr = | |
| transport | |
| (sym $ ap (λ q → q ~ f b) (fd b empty ∙ ap (node (f b)) fe)) | |
| idr | |
| fun-rel f fe fd .(node (node x y) z) .(node x (node y z)) (assoc {x} {y} {z}) = | |
| transport | |
| (sym $ ap (λ q → q ~ f (node x (node y z))) (fd (node x y) z ∙ ap (λ q → node q (f z)) (fd x y)) | |
| ∙ ap (λ q → node (node (f x) (f y)) (f z) ~ q) (fd x (node y z) ∙ ap (node (f x)) (fd y z))) | |
| assoc | |
| fun-rel f fe fd x y (prop {x} {y} p q i) = | |
| prop (fun-rel f fe fd x y p) (fun-rel f fe fd x y q) i | |
| mapₗ : (A → B) → ListQ A → ListQ B | |
| mapₗ f = SetQ.rec (hlevel 2) (⦋_⦌ ∘ mapt f) (λ a b r → glue/ _ _ (fun-rel (mapt f) refl (λ x y → refl) a b r)) | |
| filterₗ : (A → Bool) → ListQ A → ListQ A | |
| filterₗ f = SetQ.rec (hlevel 2) (⦋_⦌ ∘ filtert f) (λ a b r → glue/ _ _ (fun-rel (filtert f) refl (λ x y → refl) a b r)) | |
| concat-mapt : (A → ListQ B) → Tree A → ListQ B | |
| concat-mapt f empty = nilₗ | |
| concat-mapt f (leaf x) = f x | |
| concat-mapt f (node l r) = concatₗ (concat-mapt f l) (concat-mapt f r) | |
| concat-mapt-rel : {f : A → ListQ B} → (a b : Tree A) → a ~ b → concat-mapt f a ＝ concat-mapt f b | |
| concat-mapt-rel a .a eqt = refl | |
| concat-mapt-rel a b (symt r) = | |
| sym (concat-mapt-rel b a r) | |
| concat-mapt-rel a b (transt {y} l r) = | |
| concat-mapt-rel a y l ∙ concat-mapt-rel y b r | |
| concat-mapt-rel {f} .(node x z) .(node y w) (congr {x} {y} {z} {w} l r) = | |
| ap (concatₗ (concat-mapt f x)) (concat-mapt-rel z w r) | |
| ∙ ap (λ q → concatₗ q (concat-mapt f w)) (concat-mapt-rel x y l) | |
| concat-mapt-rel {f} .(node empty b) b idl = | |
| concatₗ-id-l (concat-mapt f b) | |
| concat-mapt-rel {f} .(node b empty) b idr = | |
| concatₗ-id-r (concat-mapt f b) | |
| concat-mapt-rel {f} .(node (node x y) z) .(node x (node y z)) (assoc {x} {y} {z}) = | |
| concatₗ-assoc (concat-mapt f x) (concat-mapt f y) (concat-mapt f z) | |
| concat-mapt-rel {f} x y (prop {x} {y} p q i) = | |
| hlevel 2 _ _ (concat-mapt-rel x y p) (concat-mapt-rel x y q) i | |
| concat-mapₗ : (A → ListQ B) → ListQ A → ListQ B | |
| concat-mapₗ f = SetQ.rec (hlevel 2) (concat-mapt f) concat-mapt-rel | |
| -- bags | |
| data _~ₐ_ {A : 𝒰 ℓ} : ListQ A → ListQ A → 𝒰 ℓ where | |
| eqtₐ : {x : ListQ A} | |
| → x ~ₐ x | |
| symtₐ : {x y : ListQ A} | |
| → x ~ₐ y → y ~ₐ x | |
| transtₐ : {x y z : ListQ A} | |
| → x ~ₐ y → y ~ₐ z → x ~ₐ z | |
| congrₐ : ⦋ x ⦌ ~ₐ ⦋ y ⦌ → ⦋ z ⦌ ~ₐ ⦋ w ⦌ → ⦋ node x z ⦌ ~ₐ ⦋ node y w ⦌ | |
| comm : ⦋ node x y ⦌ ~ₐ ⦋ node y x ⦌ | |
| propₐ : {x y : ListQ A} → (p q : x ~ₐ y) → p ＝ q | |
| instance | |
| H-Level-~ₐ : {A : 𝒰 ℓ} {n : ℕ} {x y : ListQ A} → H-Level (suc n) (x ~ₐ y) | |
| H-Level-~ₐ = hlevel-prop-instance propₐ | |
| BagQ : 𝒰 ℓ → 𝒰 ℓ | |
| BagQ A = ListQ A / _~ₐ_ | |
| concatₗ-rel-l : (x y z : ListQ A) → x ~ₐ y → concatₗ x z ~ₐ concatₗ y z | |
| concatₗ-rel-l = elim! λ a b c r → congrₐ r eqtₐ | |
| concatₗ-rel-r : (x y z : ListQ A) → y ~ₐ z → concatₗ x y ~ₐ concatₗ x z | |
| concatₗ-rel-r = elim! λ a b c r → congrₐ eqtₐ r | |
| concatₐ : BagQ A → BagQ A → BagQ A | |
| concatₐ = rec² (hlevel 2) | |
| (λ x y → ⦋ concatₗ x y ⦌) | |
| (λ x y z r → glue/ (concatₗ x z) (concatₗ y z) (concatₗ-rel-l x y z r)) | |
| (λ x y z r → glue/ (concatₗ x y) (concatₗ x z) (concatₗ-rel-r x y z r)) | |
| countₐ-rel : (f : A → Bool) → (a b : ListQ A) → a ~ₐ b → countₗ f a ＝ countₗ f b | |
| countₐ-rel f a .a eqtₐ = refl | |
| countₐ-rel f a b (symtₐ r) = sym (countₐ-rel f b a r) | |
| countₐ-rel f a b (transtₐ {y} l r) = | |
| countₐ-rel f a y l ∙ countₐ-rel f y b r | |
| countₐ-rel f .(⦋ node x z ⦌) .(⦋ node y w ⦌) (congrₐ {x} {y} {z} {w} l r) = | |
| ap (λ q → q + count f z) (countₐ-rel f ⦋ x ⦌ ⦋ y ⦌ l) | |
| ∙ ap (λ q → count f y + q) (countₐ-rel f ⦋ z ⦌ ⦋ w ⦌ r) | |
| countₐ-rel f .(⦋ node x y ⦌) .(⦋ node y x ⦌) (comm {x} {y}) = +-comm (count f x) (count f y) | |
| countₐ-rel f x y (propₐ {x} {y} p q i) = | |
| hlevel 2 _ _ (countₐ-rel f x y p) (countₐ-rel f x y q) i | |
| countₐ : (A → Bool) → BagQ A → ℕ | |
| countₐ f = SetQ.rec (hlevel 2) (countₗ f) (countₐ-rel _) | |
| hasₐ-rel : (f : A → Bool) → (a b : ListQ A) → a ~ₐ b → hasₗ f a ＝ hasₗ f b | |
| hasₐ-rel f a .a eqtₐ = refl | |
| hasₐ-rel f a b (symtₐ r) = sym (hasₐ-rel f b a r) | |
| hasₐ-rel f a b (transtₐ {y} l r) = | |
| hasₐ-rel f a y l ∙ hasₐ-rel f y b r | |
| hasₐ-rel f .(⦋ node x z ⦌) .(⦋ node y w ⦌) (congrₐ {x} {y} {z} {w} l r) = | |
| ap (λ q → q or has f z) (hasₐ-rel f ⦋ x ⦌ ⦋ y ⦌ l) | |
| ∙ ap (λ q → has f y or q) (hasₐ-rel f ⦋ z ⦌ ⦋ w ⦌ r) | |
| hasₐ-rel f .(⦋ node x y ⦌) .(⦋ node y x ⦌) (comm {x} {y}) = or-comm (has f x) (has f y) | |
| hasₐ-rel f x y (propₐ {x} {y} p q i) = | |
| hlevel 2 _ _ (hasₐ-rel f x y p) (hasₐ-rel f x y q) i | |
| hasₐ : (A → Bool) → BagQ A → Bool | |
| hasₐ f = SetQ.rec (hlevel 2) (hasₗ f) (hasₐ-rel _) | |
| -- can't easily abstract these because we rely on definitional behaviour in congr: | |
| -- f ⦋ x ⦌ := ⦋ ft x ⦌ | |
| mapₐ-rel : (f : A → B) → (a b : ListQ A) → a ~ₐ b → mapₗ f a ~ₐ mapₗ f b | |
| mapₐ-rel f a .a eqtₐ = eqtₐ | |
| mapₐ-rel f a b (symtₐ r) = symtₐ (mapₐ-rel f b a r) | |
| mapₐ-rel f a b (transtₐ {y} l r) = | |
| transtₐ (mapₐ-rel f a y l) (mapₐ-rel f y b r) | |
| mapₐ-rel f .(⦋ node x z ⦌) .(⦋ node y w ⦌) (congrₐ {x} {y} {z} {w} l r) = | |
| congrₐ (mapₐ-rel f ⦋ x ⦌ ⦋ y ⦌ l) (mapₐ-rel f ⦋ z ⦌ ⦋ w ⦌ r) | |
| mapₐ-rel f .(⦋ node _ _ ⦌) .(⦋ node _ _ ⦌) comm = comm | |
| mapₐ-rel f x y (propₐ {x} {y} p q i) = | |
| propₐ (mapₐ-rel f x y p) (mapₐ-rel f x y q) i | |
| mapₐ : (A → B) → BagQ A → BagQ B | |
| mapₐ f = SetQ.rec (hlevel 2) (⦋_⦌ ∘ mapₗ f) (λ a b r → glue/ (mapₗ f a) (mapₗ f b) (mapₐ-rel f a b r)) | |
| filterₐ-rel : (f : A → Bool) → (a b : ListQ A) → a ~ₐ b → filterₗ f a ~ₐ filterₗ f b | |
| filterₐ-rel f a .a eqtₐ = eqtₐ | |
| filterₐ-rel f a b (symtₐ r) = symtₐ (filterₐ-rel f b a r) | |
| filterₐ-rel f a b (transtₐ {y} l r) = | |
| transtₐ (filterₐ-rel f a y l) (filterₐ-rel f y b r) | |
| filterₐ-rel f .(⦋ node x z ⦌) .(⦋ node y w ⦌) (congrₐ {x} {y} {z} {w} l r) = | |
| congrₐ (filterₐ-rel f ⦋ x ⦌ ⦋ y ⦌ l) (filterₐ-rel f ⦋ z ⦌ ⦋ w ⦌ r) | |
| filterₐ-rel f .(⦋ node _ _ ⦌) .(⦋ node _ _ ⦌) comm = comm | |
| filterₐ-rel f x y (propₐ {x} {y} p q i) = | |
| propₐ (filterₐ-rel f x y p) (filterₐ-rel f x y q) i | |
| filterₐ : (A → Bool) → BagQ A → BagQ A | |
| filterₐ f = SetQ.rec (hlevel 2) (⦋_⦌ ∘ filterₗ f) (λ a b r → glue/ (filterₗ f a) (filterₗ f b) (filterₐ-rel f a b r)) | |
| -- sets | |
| data _~ₛ_ {A : 𝒰 ℓ} : BagQ A → BagQ A → 𝒰 ℓ where | |
| eqtₛ : {x : BagQ A} | |
| → x ~ₛ x | |
| symtₛ : {x y : BagQ A} | |
| → x ~ₛ y → y ~ₛ x | |
| transtₛ : {x y z : BagQ A} | |
| → x ~ₛ y → y ~ₛ z → x ~ₛ z | |
| congrₛ : ⦋ ⦋ x ⦌ ⦌ ~ₛ ⦋ ⦋ y ⦌ ⦌ → ⦋ ⦋ z ⦌ ⦌ ~ₛ ⦋ ⦋ w ⦌ ⦌ → ⦋ ⦋ node x z ⦌ ⦌ ~ₛ ⦋ ⦋ node y w ⦌ ⦌ | |
| idem : ⦋ ⦋ node x x ⦌ ⦌ ~ₛ ⦋ ⦋ x ⦌ ⦌ | |
| propₛ : {x y : BagQ A} → (p q : x ~ₛ y) → p ＝ q | |
| FSetQ : 𝒰 ℓ → 𝒰 ℓ | |
| FSetQ A = BagQ A / _~ₛ_ | |
| hasₛ-rel : (f : A → Bool) → (a b : BagQ A) → a ~ₛ b → hasₐ f a ＝ hasₐ f b | |
| hasₛ-rel f a .a eqtₛ = refl | |
| hasₛ-rel f a b (symtₛ r) = sym (hasₛ-rel f b a r) | |
| hasₛ-rel f a b (transtₛ {y} l r) = | |
| hasₛ-rel f a y l ∙ hasₛ-rel f y b r | |
| hasₛ-rel f .(⦋ ⦋ node x z ⦌ ⦌) .(⦋ ⦋ node y w ⦌ ⦌) (congrₛ {x} {y} {z} {w} l r) = | |
| ap (λ q → q or has f z) (hasₛ-rel f ⦋ ⦋ x ⦌ ⦌ ⦋ ⦋ y ⦌ ⦌ l) | |
| ∙ ap (λ q → has f y or q) (hasₛ-rel f ⦋ ⦋ z ⦌ ⦌ ⦋ ⦋ w ⦌ ⦌ r) | |
| hasₛ-rel f .(⦋ ⦋ node x x ⦌ ⦌) .(⦋ ⦋ x ⦌ ⦌) (idem {x}) = or-idem (has f x) | |
| hasₛ-rel f x y (propₛ {x} {y} l r i) = | |
| hlevel 2 _ _ (hasₛ-rel f x y l) (hasₛ-rel f x y r) i | |
| hasₛ : (A → Bool) → FSetQ A → Bool | |
| hasₛ f = SetQ.rec (hlevel 2) (hasₐ f) (hasₛ-rel _) | |
| filterₛ-rel : (f : A → Bool) → (a b : BagQ A) → a ~ₛ b → filterₐ f a ~ₛ filterₐ f b | |
| filterₛ-rel f a .a eqtₛ = eqtₛ | |
| filterₛ-rel f a b (symtₛ r) = symtₛ (filterₛ-rel f b a r) | |
| filterₛ-rel f a b (transtₛ {y} l r) = | |
| transtₛ (filterₛ-rel f a y l) (filterₛ-rel f y b r) | |
| filterₛ-rel f .(⦋ ⦋ node x z ⦌ ⦌) .(⦋ ⦋ node y w ⦌ ⦌) (congrₛ {x} {y} {z} {w} l r) = | |
| congrₛ (filterₛ-rel f ⦋ ⦋ x ⦌ ⦌ ⦋ ⦋ y ⦌ ⦌ l) (filterₛ-rel f ⦋ ⦋ z ⦌ ⦌ ⦋ ⦋ w ⦌ ⦌ r) | |
| filterₛ-rel f .(⦋ ⦋ node x x ⦌ ⦌) .(⦋ ⦋ x ⦌ ⦌) (idem {x}) = idem {x = filtert f x} | |
| filterₛ-rel f x y (propₛ {x} {y} p q i) = | |
| propₛ (filterₛ-rel f x y p) (filterₛ-rel f x y q) i | |
| filterₛ : (A → Bool) → FSetQ A → FSetQ A | |
| filterₛ f = SetQ.rec (hlevel 2) (⦋_⦌ ∘ filterₐ f) (λ a b r → glue/ (filterₐ f a) (filterₐ f b) (filterₛ-rel f a b r)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment