2012. NK.

\begin{code} 

module KrausLemma where

open import mini-library

Type = Set

hprop : Type  Type
hprop X = (x y : X)  x  y

constant : {X Y : Type}  (f : X  Y)  Type
constant {X} {Y} f = (x y : X)  f x  f y

collapsible : Type  Type
collapsible X = Σ \(f : X  X)  constant f

fix : {X : Type}  (f : X  X)  Type
fix f = Σ \x  x  f x

key-insight-generalized : {X Y : Type} (f : X  Y) (g : constant f) {x y : X} (p : x  y) 
                        cong f p  (g x x)⁻¹  (g x y) 
key-insight-generalized f g {x} {y} = 
  J  {x} {y} p  cong f p  (g x x)⁻¹  (g x y))  {x}  sym-is-inverse(g x x))

key-insight : {X Y : Type} (f : X  Y)  constant f  {x : X} (p : x  x)  cong f p  refl
key-insight f g p = (key-insight-generalized f g p)  ((sym-is-inverse(g _ _))⁻¹) 

transport-paths-along-paths : {X Y : Type} {x y : X} (p : x  y) (h k : X  Y) (q : h x  k x) 
                            subst p q  (cong h p)⁻¹  q  (cong k p)
transport-paths-along-paths {X} {Y} {x} p h k q = 
 J' x  p  subst p q  ((cong h p)⁻¹)  q  (cong k p)) (refl-is-right-id q) p

transport-paths-along-paths' : {X : Type} {x : X} (p : x  x) (f : X  X) (q : x  f x) 
                             subst {X}  z  z  f z} p q  p ⁻¹  q  (cong f p)
transport-paths-along-paths' {X} {x} p f q = 
 (transport-paths-along-paths p  z  z) f q)  (cong  pr  pr ⁻¹  q  (cong f p)) ((cong-id-is-id p)⁻¹))

Kraus-Lemma : {X : Type}  (f : X  X)  constant f  hprop(fix f)
Kraus-Lemma {X} f g (x , p) (y , q) = 
  -- p : x ≡ f x
  -- q : y ≡ f y
  (x , p)        ≡⟨ split x y p p' r refl 
  (y , p')       ≡⟨ split y y p' q s t ⟩∎           
  (y , q) 
    where
     r : x  y
     r = x ≡⟨ p 
       f x ≡⟨ g x y 
       f y ≡⟨ q ⁻¹ ⟩∎
         y 
     p' : y  f y
     p' = subst r p
     s : y  y
     s = y   ≡⟨ p' 
         f y ≡⟨ q ⁻¹ ⟩∎
         y   
     q' : y  f y
     q' = subst {X}  y  y  f y} s p'
     t : q'  q
     t = q'                         ≡⟨ transport-paths-along-paths' s f p' 
         s ⁻¹  (p'  cong f s)     ≡⟨ cong  pr  s ⁻¹  (p'  pr)) (key-insight f g s) 
         s ⁻¹  (p'  refl)         ≡⟨ cong  pr  s ⁻¹  pr) ((refl-is-right-id p')⁻¹)  
         s ⁻¹  p'                  ≡⟨ refl  
         (p'  (q ⁻¹))⁻¹  p'       ≡⟨ cong  pr  pr  p') ((sym-trans p' (q ⁻¹))⁻¹)  
         ((q ⁻¹)⁻¹  (p' ⁻¹))  p'  ≡⟨ cong  pr  (pr  (p' ⁻¹))  p') ((sym-sym-trivial q)⁻¹) 
         (q  (p' ⁻¹))  p'         ≡⟨ trans-assoc q (p' ⁻¹) p'  
         q  ((p' ⁻¹)  p')         ≡⟨ cong  pr  q  pr) ((sym-is-inverse p')⁻¹) 
         q  refl                   ≡⟨ (refl-is-right-id q)⁻¹  ⟩∎
         q  

from-fix : {X : Type} (f : X  X)  fix f  X
from-fix f = π₀

to-fix : {X : Type} (f : X  X)  constant f  X  fix f
to-fix f g x = (f x , g x (f x))

\end{code}