agda
Filters - alternative to the base of Domain theory
This work aims to be an alternative to the base of domain theory (#2809). There were a lot of discussions about the decisions, and talking with @TOTBWF, a good alternative would be using filters. So, we introduced a generalised way.
Added
- Up and Down directness.
- Up and Down closure.
- IsFilter
- IsIdeal (Dual of Filter)
- Two facts about filters in relation to lattices.
Structure
I know the current implementation does not follow the stdlib patterns, but some of the facts and definitions I was not sure about were to be put.
@gabriellisboaconegero and I have had some offline discussions about using a homomorphism-based definition that seems to be the One True Way. The idea is that we can define a setoidal analog of the order on propositions by defining a poset whose carrier is Set κ, where equivalence is bi-implication and P ≤ Q as P → Q, as in the following code.
module Cool where
open import Level
open import Data.Product
open import Function.Base
open import Relation.Binary.Structures
open import Relation.Binary.Bundles
open IsPreorder
open IsPartialOrder
record _↔_ {ℓ ℓ'} (P : Set ℓ) (Q : Set ℓ') : Set (ℓ ⊔ ℓ') where
field
to : P → Q
from : Q → P
open _↔_
private variable
ℓ : Level
P Q R : Set ℓ
id↔ : P ↔ P
id↔ .to = id
id↔ .from = id
_∙↔_ : P ↔ Q → Q ↔ R → P ↔ R
(f ∙↔ g) .to = g .to ∘ f .to
(f ∙↔ g) .from = f .from ∘ g .from
_↔⁻¹ : P ↔ Q → Q ↔ P
(f ↔⁻¹) .to = f .from
(f ↔⁻¹) .from = f .to
BiImplicationIsEquivalence : ∀ {ℓ} → IsEquivalence (_↔_ {ℓ})
BiImplicationIsEquivalence .IsEquivalence.refl = id↔
BiImplicationIsEquivalence .IsEquivalence.sym = _↔⁻¹
BiImplicationIsEquivalence .IsEquivalence.trans = _∙↔_
Omega : ∀ (κ : Level) → Poset (suc κ) κ κ
Omega κ .Poset.Carrier = Set κ
Omega κ .Poset._≈_ P Q = P ↔ Q
Omega κ .Poset._≤_ P Q = P → Q
Omega κ .Poset.isPartialOrder .isPreorder .isEquivalence = BiImplicationIsEquivalence
Omega κ .Poset.isPartialOrder .isPreorder .reflexive p↔q = p↔q .to
Omega κ .Poset.isPartialOrder .isPreorder .trans p→q q→r = q→r ∘ p→q
Omega κ .Poset.isPartialOrder .antisym p→q q→r .to = p→q
Omega κ .Poset.isPartialOrder .antisym p→q q→r .from = q→r
This removes the need for upwards and downwards closure, as a homomorphism P → Omega κ is exactly an upwards closed subset (and likewise for Opposite P → Omega κ and downwards closure).
Next, we can define the order-theoretic analog of the category of elements. This transforms a monotone map F : P → Omega κ into an order Restrict F whose carrier is Σ (p : P.Carrier) (F p), where the order and equivalence are given purely by the p component. In other words, this lets us restrict an order to an upwards closed subset.
Finally, we can define a filter as a monotone map F : P → Omega κ such that Restrict F is downwards directed. This seems like a nice point in the design space, as we get to re-use a lot of pre-existing notions. Moreover, this is a direct decategorification of the definition of a [flat](flat functor), which is always a good sign.
EDIT: It was pointed out on zulip that this equivalence relation already exists as https://agda.github.io/agda-stdlib/master/Function.Properties.Equivalence.html#1935, so it should be really easy to assemble this from kit that we already have.
