module Order.Diagram.Fixpoint {o } (P : Poset o ) where

Let be a poset, and be a monotone map. We say that has a least fixpoint if there exists some such that and for every other such that

record is-least-fixpoint (f : Posets.Hom P P) (x : Ob) : Type (o  ) where
    fixed : f .hom x  x
    least :  (y : Ob)  f .hom y  y  x  y

record Least-fixpoint (f : Posets.Hom P P) : Type (o  ) where
    fixpoint : Ob
    has-least-fixpoint : is-least-fixpoint f fixpoint
  open is-least-fixpoint has-least-fixpoint public

open is-least-fixpoint

Least fixed points are unique, so the type of least fixpoints of is a proposition.

  :  {f : Posets.Hom P P} {x y}
   is-least-fixpoint f x  is-least-fixpoint f y
   x  y
least-fixpoint-unique x-fix y-fix =
  ≤-antisym (x-fix .least _ (y-fix .fixed)) (y-fix .least _ (x-fix .fixed))

  :  {f : Posets.Hom P P} {x}
   is-prop (is-least-fixpoint f x)
is-least-fixpoint-is-prop {f = f} {x = x} p q i .fixed =
  Ob-is-set (f .hom x) x (p .fixed) (q .fixed) i
is-least-fixpoint-is-prop {f = f} {x = x} p q i .least y y-fix =
     i  ≤-thin)
    (p .least y y-fix) (q .least y y-fix) i

  :  {f : Posets.Hom P P}
   is-prop (Least-fixpoint f)
Least-fixpoint-is-prop {f = f} p q = p≡q where
  module p = Least-fixpoint p
  module q = Least-fixpoint q

  path : p.fixpoint  q.fixpoint
  path = least-fixpoint-unique p.has-least-fixpoint q.has-least-fixpoint

  p≡q : p  q
  p≡q i .Least-fixpoint.fixpoint = path i
  p≡q i .Least-fixpoint.has-least-fixpoint =
    is-prop→pathp  i  is-least-fixpoint-is-prop {x = path i})
      p.has-least-fixpoint q.has-least-fixpoint i