Skip to content

Instantly share code, notes, and snippets.

@clayrat
Last active June 13, 2024 13:16
Show Gist options
  • Save clayrat/818acc30a02338bad29690ef499955ec to your computer and use it in GitHub Desktop.
Save clayrat/818acc30a02338bad29690ef499955ec to your computer and use it in GitHub Desktop.
Examples from QuotientHaskell paper in Cubical Agda (+ cubical-mini)
{-# 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