{-
  Definition of function fixpoint and Kraus' lemma
-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Functions.Fixpoint where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Path

private
  variable
     : Level
    A : Type 

Fixpoint : (A  A)  Type _
Fixpoint {A = A} f = Σ A  x  f x  x)

fixpoint : {f : A  A}  Fixpoint f  A
fixpoint = fst

fixpointPath : {f : A  A}  (p : Fixpoint f)  f (fixpoint p)  fixpoint p
fixpointPath = snd

-- Kraus' lemma
-- a version not using cubical features can be found at
-- https://www.cs.bham.ac.uk/~mhe/GeneralizedHedberg/html/GeneralizedHedberg.html#21576
2-Constant→isPropFixpoint : (f : A  A)  2-Constant f  isProp (Fixpoint f)
2-Constant→isPropFixpoint f fconst (x , p) (y , q) i = s i , t i where
  noose :  x y  f x  f y
  noose x y = sym (fconst x x)  fconst x y
  -- the main idea is that for any path p, cong f p does not depend on p
  -- but only on its endpoints and the structure of 2-Constant f
  KrausInsight :  {x y}  (p : x  y)  noose x y  cong f p
  KrausInsight {x} = J  y p  noose x y  cong f p) (lCancel (fconst x x))
  -- Need to solve for a path s : x ≡ y, such that:
  -- transport (λ i → cong f s i ≡ s i) p ≡ q
  s : x  y
  s = sym p ∙∙ noose x y ∙∙ q
  t' : PathP  i  noose x y i  s i) p q
  t' i j = doubleCompPath-filler (sym p) (noose x y) q j i
  t : PathP  i  cong f s i  s i) p q
  t = subst  kraus  PathP  i  kraus i  s i) p q) (KrausInsight s) t'