module Refinement where

open import Prelude

open import Function using (id)
open import Data.Product using (Σ; _,_) renaming (map to _**_)
open import Relation.Binary.PropositionalEquality using (_≡_; cong)


record Refinement {I J : Set} (X : I → Set) (Y : J → Set) : Set₁ where
  field
    e : J → I
    P : ∀ {i} (j : e ⁻¹ i) → X i → Set
    ℜ : ∀ {i} (j : e ⁻¹ i) → Iso (Y (und j)) (Σ (X i) (P j))

record Swap {I J : Set} {X : I → Set} {Y : J → Set} (r : Refinement X Y) : Set₁ where
  field
    Q : ∀ {i} (j : Refinement.e r ⁻¹ i) (x : X i) → Set
    s : ∀ {i} (j : Refinement.e r ⁻¹ i) (x : X i) → Iso (Refinement.P r j x) (Q j x)

idSwap : ∀ {I J} {X : I → Set} {Y : J → Set} {r : Refinement X Y} → Swap r
idSwap {r = r} = record { Q = Refinement.P r
                        ; s = λ _ _ → idIso }

toRefinement : ∀ {I J} {X : I → Set} {Y : J → Set} {r : Refinement X Y} → Swap r → Refinement X Y
toRefinement {r = r} s =
  record { e = Refinement.e r
         ; P = Swap.Q s
         ; ℜ = λ j → transIso (Refinement.ℜ r j)
                              (record { to   = id ** (λ {x} → Iso.to (Swap.s s j x))
                                      ; from = id ** (λ {x} → Iso.from (Swap.s s j x))
                                      ; to-from-inverse = λ { {x , q} → cong (_,_ x) (Iso.to-from-inverse (Swap.s s j x)) }
                                      ; from-to-inverse = λ { {x , p} → cong (_,_ x) (Iso.from-to-inverse (Swap.s s j x)) } }) }