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)) } }) }