{-# OPTIONS --without-K #-}
open import Level.NP
open import Type hiding ()
open import Function.NP
open import Data.Product
open import Data.Sum
import Relation.Binary.PropositionalEquality as 
open import Function.Related.TypeIsomorphisms.NP
import Function.Inverse.NP as Inv
open Inv using (_↔_; inverses; module Inverse) renaming (_$₁_ to to; _$₂_ to from)
open import Relation.Binary.NP

open import Explore.Core
open import Explore.Properties
open import Explore.Explorable
import Explore.Monad

-- NOTE: it would be nice to have another module to change the definition of an exploration
-- function by an extensionally equivalent one. Combined with this module one could both
-- pick the reduction behavior we want and save some proof effort.
module Explore.Isomorphism
  {A B : ★₀} (A↔B : A  B) where

private
  module M {} = Explore.Monad 

module _ {} (Aᵉ : Explore  A) where
  explore-iso : Explore  B
  explore-iso = M.map (to A↔B) Aᵉ

private
  Bᵉ = explore-iso

module _ { p} {Aᵉ : Explore  A} (Aⁱ : ExploreInd p Aᵉ) where
  explore-iso-ind : ExploreInd p (Bᵉ Aᵉ)
  explore-iso-ind = M.map-ind (to A↔B) Aⁱ

private
  Bⁱ = explore-iso-ind

module _ {} {Aᵉ : Explore ( ) A} ( : Lookup {} Aᵉ) where
  lookup-iso : Lookup {} (Bᵉ Aᵉ)
  lookup-iso {C} d b
    = ≡.subst C (Inverse.right-inverse-of A↔B b)
                ( d (from A↔B b))

module _ {} {Aᵉ : Explore ( ) A} (Aᶠ : Focus {} Aᵉ) where
  focus-iso : Focus {} (Bᵉ Aᵉ)
  focus-iso {C} (b , c) = Aᶠ (from A↔B b , c')
    where c' = ≡.subst C (≡.sym (Inverse.right-inverse-of A↔B b)) c

module _ ( : Sum A) where
  sum-iso : Sum B
  sum-iso f =  (f  to A↔B)

module _ (Aᵖ : Product A) where
  product-iso : Product B
  product-iso f = Aᵖ (f  to A↔B)

module _ {Aᵉ : Explore₁ A} (Aⁱ : ExploreInd₀ Aᵉ) where
  open Explorable₁₀ (Bⁱ Aⁱ) public using () renaming (reify   to reify-iso)

module _ {Aᵉ : Explore₁ A} (Aⁱ : ExploreInd₁ Aᵉ) where
  open Explorable₁₁ (Bⁱ Aⁱ) public using () renaming (unfocus to unfocus-iso)

module _ { : Sum A} (Aˢ-ok : AdequateSum ) where
  sum-iso-ok : AdequateSum (sum-iso )
  sum-iso-ok f = sym-first-iso A↔B Inv.∘ Aˢ-ok (f  to A↔B)

{- requires extensional equality
module _ {Aᵖ : Product A} (Aᵖ-ok : AdequateProduct Aᵖ) where
  product-iso-ok : AdequateProduct (product-iso Aᵖ)
  product-iso-ok f = arg-iso A↔B Inv.∘ Aᵖ-ok (f ∘ to A↔B)
-}

  {-
module _ (Aᵉ : Explore₁ A) where
  focused-iso : Focused {₀} (Bᵉ Aᵉ)
  focused-iso = inverses {!!} {!!} {!(⇒)!} {!(⇐)!}
    where ⇒ : (x : Σ _ _) → _
          ⇒ (b , c) = {!!}
          ⇐ : (x : _ ⊎ _) → _
          ⇐ (inj₁ x) = {!!}
          ⇐ (inj₂ x) = {!!}
-}