Filters - alternative to the base of Domain theory

[gabriellisboaconegero]

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.

[jamesmckinna]

[DRY]
This is redundant, as an instance of Relation.Binary.Definitions._Respects_... noting that the use of of _×_ again involves redundant currying/uncurrying.

[jamesmckinna]

I suppose that the thing which makes me uneasy about such a definition is that it fuses two aspects of the definition, in the interest of avoiding some of the difficulties that Reed alludes to in #2814 , namely:

• the 'subset' implicitly defined by the predicate F
• the abstract property of a relation, here '_≤_ restricted to the subset defined by F', as being directed

I think as far as stdlib is concerned, it would be (more) helpful to isolate the second one, as for example in #2813 (where it would make sense simply to cherry-pick the definition, and perhaps some of its properties, and leave the Pointed extension construction to a separate PR), and as to the first, perhaps introduce a/the construction, analogous to Function.Base._on_, corresponding to the first one?

Not sure whether we should continue the discussion here, or else on #2814 though.

[TOTBWF]

@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.