cfilter

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

Map a cfilter to an equivalent representation type.

cfilter.to_filter

The filter represented by a cfilter is the collection of supersets of elements of the filter base.

filter.realizer

A realizer for filter f is a cfilter which generates f.

filter.realizer.of_filter

A filter realizes itself.

filter.realizer.of_equiv

Transfer a filter realizer to another realizer on a different base type.

filter.realizer.principal

unit is a realizer for the principal filter

filter.realizer.top

unit is a realizer for the top filter

filter.realizer.bot

unit is a realizer for the bottom filter

filter.realizer.map

Construct a realizer for map m f given a realizer for f

filter.realizer.comap

Construct a realizer for comap m f given a realizer for f

filter.realizer.sup

Construct a realizer for the sup of two filters

filter.realizer.inf

Construct a realizer for the inf of two filters

filter.realizer.cofinite

Construct a realizer for the cofinite filter

filter.realizer.bind

Construct a realizer for filter bind

filter.realizer.Sup

Construct a realizer for indexed supremum

filter.realizer.prod

Construct a realizer for the product of filters