open import Cat.Instances.OFE
open import Cat.Prelude

module Cat.Instances.OFE.Discrete where


Discrete OFEsπ

Given a set we can make it into a discrete OFE by equipping it with the relation that takes one step to approximate equality: is trivial, but is defined to be no matter what is.

Discrete-OFE : β {β} (A : Type β) β is-set A β OFE-on β A
Discrete-OFE A A-set .within zero x y = Lift _ β€
Discrete-OFE A A-set .within (suc n) x y = x β‘ y
Discrete-OFE A A-set .has-is-ofe .has-is-prop zero _ _ _ _ _ = _
Discrete-OFE A A-set .has-is-ofe .has-is-prop (suc n) = A-set

Discrete-OFE A A-set .has-is-ofe .β-refl zero = _
Discrete-OFE A A-set .has-is-ofe .β-refl (suc n) = refl

Discrete-OFE A A-set .has-is-ofe .β-sym zero = _
Discrete-OFE A A-set .has-is-ofe .β-sym (suc n) p = sym p

Discrete-OFE A A-set .has-is-ofe .β-trans zero = _
Discrete-OFE A A-set .has-is-ofe .β-trans (suc n) p q = q β p

Discrete-OFE A A-set .has-is-ofe .bounded = _
Discrete-OFE A A-set .has-is-ofe .step zero = _
Discrete-OFE A A-set .has-is-ofe .step (suc n) x y p = p
Discrete-OFE A A-set .has-is-ofe .limit x y Ξ± = Ξ± 1