{-
  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'