module RollingRule where

open import Preliminaries

fix : {A : Set} (t : A → A) → Set
fix {A} t = Σ A (λ a → t a ≡ a)

module _ {A B : Set} (f : A → B) (g : B → A) where
  abstract
    rolling-rule : fix (g ∘ f) ≅ fix (f ∘ g)
    rolling-rule = inv-iso fix-gf-iso ∘ₑ fix-fg-iso where
      C : Set
      C = Σ A (λ a → Σ B (λ b → Σ (f a ≡ b) (λ _ → (g b ≡ a))))

      fix-fg-iso : fix (g ∘ f) ≅ C
      fix-fg-iso .fun a = a .fst , f (a .fst) , refl , a .snd
      fix-fg-iso .inv t .fst = t .fst
      fix-fg-iso .inv (a , _ , refl , q) .snd = q
      fix-fg-iso .inv-fun (a , p) = refl
      fix-fg-iso .fun-inv (a , (_ , (refl , q))) = refl

      fix-gf-iso : fix (f ∘ g) ≅ C
      fix-gf-iso .fun b = g (b .fst) , b .fst , b .snd , refl
      fix-gf-iso .inv t .fst = t .snd .fst
      fix-gf-iso .inv (_ , b , q , refl) .snd = q
      fix-gf-iso .inv-fun (b , p) = refl
      fix-gf-iso .fun-inv (_ , b , q , refl) = refl

    -- These two definitional equalities are used later.
    rolling-rule-fun : (x : fix (g ∘ f)) → rolling-rule .fun x .fst ≡ f (x .fst)
    rolling-rule-fun x = refl

    rolling-rule-inv-fun : (y : fix (f ∘ g)) → rolling-rule .inv y .fst ≡ g (y .fst)
    rolling-rule-inv-fun y = refl

fix-congr : {A : Set} {t s : A → A} (p : (a : A) → t a ≡ s a) →
            fix t ≅ fix s
fix-congr p = Σ-congr-snd λ a → eq-congr (p a) refl