This file provides infrastructure to compute with filters.
CFilter (Set α) σ
A CFilter α σ is a realization of a filter (base) on α,
represented by a type σ together with operations for the top element and
the binary inf operation.
CFilter α σ
Map a CFilter to an equivalent representation type.
The filter represented by a CFilter is the collection of supersets of
elements of the filter base.
A realizer for filter f is a cfilter which generates f.
A CFilter realizes the filter it generates.
Transfer a realizer along an equality of filter. This has better definitional equalities than
the Eq.rec proof.
A filter realizes itself.
Transfer a filter realizer to another realizer on a different base type.
Unit is a realizer for the principal filter
Unit is a realizer for the top filter
Unit is a realizer for the bottom filter
Construct a realizer for map m f given a realizer for f
map m f
Construct a realizer for comap m f given a realizer for f
comap m f
Construct a realizer for the sup of two filters
Construct a realizer for the inf of two filters
Construct a realizer for the cofinite filter
Construct a realizer for filter bind
Construct a realizer for indexed supremum
Construct a realizer for the product of filters