open import Relation.Binary.PropositionalEquality as PE

module Examples.NestedTypes where

postulate ext : ∀ {ℓ} → Extensionality ℓ ℓ

open import Data.Product as P
open import Data.Sum as S
open import Function
open import Function.Equality hiding (id; _∘_)
open import Function.Related.TypeIsomorphisms
open import Function.Inverse as FI renaming (id to ↔refl; _∘_ to ↔trans; sym to ↔sym)

open import Relation.Binary.Sum
open import Relation.Binary.Product.Pointwise
open import Relation.Binary.Sigma.Pointwise as SR hiding (refl; ↔)


import Prelude
open Prelude Set (λ A B → B -> A) (λ c → id) (λ f g → g ∘ f)

import Prelude.Isos
open Prelude.Isos Set (λ A B → B -> A) (λ c → id) (λ f g → g ∘ f)
                      (λ f → refl)
                      (λ f → refl)
                      (λ f g h → refl)

import Uniform.posIR
open Uniform.posIR Set (λ A B → B -> A)
                   (λ c → id) (λ f g → g ∘ f)

import Uniform.Constructions
open Uniform.Constructions Set (λ A B → B -> A) (λ c → id) (λ f g → g ∘ f)

import Uniform.Constructions.Product
open Uniform.Constructions.Product Set (λ A B → B -> A)
                                   (λ c → id) (λ f g → g ∘ f)

import Uniform.Constructions.Coproduct
open Uniform.Constructions.Coproduct Set (λ A B → B -> A)
                                     (λ c → id) (λ f g → g ∘ f)

open import Uniform.Constructions.Pi

import Uniform.Shape
open Uniform.Shape Set (λ A B → B -> A) (λ c → id) (λ f g → g ∘ f)


open import Data.Container as Cont hiding (⟪_⟫; _⇒_)
open import Data.Container.Combinator as C hiding (id; _∘_; _⊎_; _×_)

Cont : Set1
Cont = Container _

-- Containers are functors, so they preserve ↔
-- This is easier to prove than the general case, since
-- containers satisfy the functor laws definitionally
⟦_⟧-preserves-↔ : (C : Cont) -> {X Y : Set} -> X ↔ Y ->
                    Cont.⟦ C ⟧ X ↔ Cont.⟦ C ⟧ Y
⟦ (S ▷ P) ⟧-preserves-↔  q
  = record { to = record { _⟨$⟩_ = Cont.map (_⟨$⟩_ (Inverse.to q))
                         ; cong = PE.cong (Cont.map (_⟨$⟩_ (Inverse.to q)))
                         }
           ; from = record { _⟨$⟩_ = Cont.map (_⟨$⟩_ (Inverse.from q))
                           ; cong = PE.cong (Cont.map (_⟨$⟩_ (Inverse.from q)))
                           }
           ; inverse-of
               = record {
                   left-inverse-of
                     = λ x → Eq⇒≡ (refl , (λ p → Inverse.left-inverse-of q _))
                 ; right-inverse-of
                     = λ x → Eq⇒≡ (refl , (λ p → Inverse.right-inverse-of q _))
                 }
           }
      where open Inverse
            open Function.Equality.Π
            Eq⇒≡ : ∀ {c} {C : Container c} {X : Set c} {xs ys : ⟦ C ⟧ X} →
                    Eq _≡_ xs ys → xs ≡ ys
            Eq⇒≡ {xs = s , f} {ys = .s , f′} (refl , f≈f′) =
              PE.cong (_,_ s) (ext f≈f′)

data Nest : Set1 where
  Id : Nest
  K : Cont -> Nest
  _⊞_ _⊠_ _⊛_ : Nest -> Nest -> Nest

infixl  _⊞_
infixl  _⊠_
infixr  _⊛_

⟪_⟫ : Nest -> (Set -> Set) -> (Set -> Set)
⟪   Id  ⟫ H   = H
⟪  K C  ⟫ H   = Cont.⟦ C ⟧
⟪ F ⊞ G ⟫ H X = ⟪ F ⟫ H X ⊎ ⟪ G ⟫ H X
⟪ F ⊠ G ⟫ H X = ⟪ F ⟫ H X × ⟪ G ⟫ H X
⟪ F ⊛ G ⟫ H   = ⟪ F ⟫ H ∘ ⟪ G ⟫ H


⟪_⟫-mor : (N : Nest) ->
              {F G : Set -> Set} ->
              (Gmor : {X Y : Set} -> (f : X -> Y) -> G X -> G Y) ->
              (η : (X : Set) -> F X -> G X) ->
              (X Y : Set) -> (h : X -> Y) -> ⟪ N ⟫ F X -> ⟪ N ⟫ G Y
⟪ Id ⟫-mor Gmor η X Y h = Gmor h ∘ η X
⟪ K C ⟫-mor Gmor η X Y h (s , f) = s , h ∘ f
⟪ N ⊞ N' ⟫-mor Gmor η X Y h
 = S.map (⟪ N ⟫-mor Gmor η X Y h) (⟪ N' ⟫-mor Gmor η X Y h)
⟪ N ⊠ N' ⟫-mor Gmor η X Y h
 = P.map (⟪ N ⟫-mor Gmor η X Y h) (⟪ N' ⟫-mor Gmor η X Y h)
⟪ N ⊛ N' ⟫-mor Gmor η X Y z
 = ⟪ N ⟫-mor Gmor η (⟪ N' ⟫ _ X) (⟪ N' ⟫ _ Y)
                                    (⟪ N' ⟫-mor Gmor η X Y z)


⟪_⟫Cont : Nest -> Cont -> Cont
⟪   Id  ⟫Cont H = H
⟪  K C  ⟫Cont H = C
⟪ F ⊞ G ⟫Cont H = ⟪ F ⟫Cont H C.⊎ ⟪ G ⟫Cont H
⟪ F ⊠ G ⟫Cont H = ⟪ F ⟫Cont H C.× ⟪ G ⟫Cont H
⟪ F ⊛ G ⟫Cont H = ⟪ F ⟫Cont H C.∘ ⟪ G ⟫Cont H

⟪_⟫-restricts-to-Cont : (N : Nest) -> (C : Cont) ->
                        ⟪ N ⟫ (Cont.⟦ C ⟧) ↔̇ Cont.⟦ ⟪ N ⟫Cont C ⟧
⟪ Id ⟫-restricts-to-Cont C = ↔refl
⟪ K D ⟫-restricts-to-Cont C = ↔refl
⟪ F ⊞ G ⟫-restricts-to-Cont C
   = ↔trans (FI.sym (C.Sum.correct (⟪ F ⟫Cont C) (⟪ G ⟫Cont C)))
             (⟪ F ⟫-restricts-to-Cont C ⊎-↔ ⟪ G ⟫-restricts-to-Cont C)
⟪ F ⊠ G ⟫-restricts-to-Cont C
   = ↔trans (FI.sym (C.Product.correct ext (⟪ F ⟫Cont C) (⟪ G ⟫Cont C)))
             (⟪ F ⟫-restricts-to-Cont C ×-↔ ⟪ G ⟫-restricts-to-Cont C)
⟪ F ⊛ G ⟫-restricts-to-Cont C {X}
   = ↔trans (FI.sym (C.Composition.correct (⟪ F ⟫Cont C) (⟪ G ⟫Cont C)))
       (↔trans (⟦ (⟪ F ⟫Cont C) ⟧-preserves-↔ (⟪ G ⟫-restricts-to-Cont C))
                (⟪ F ⟫-restricts-to-Cont C))


-- ⟦ N • γ ⟧UIR C ↔FamC (⟪ N ⟫Cont C) C.∘ (⟦ γ ⟧UIR C)
_•_ :  Nest -> UIR+ -> UIR+
Id • γ = δ₁ ((λ X → proj₂ X _) ⇒ IRwkσ (IRwkδ γ))
               (λ f → ⇒-mor _ _ f _ _ (refl-shape (IRwkσ (IRwkδ γ)))
                              (HomcMor _ _ (HomcMor _ _ (idIR' γ))))
(K (S ▷ P)) • γ = σ (λ _ → S) ((λ X → P (proj₂ X)) ⇒ IRwkσ (IRwkσ γ))
(N ⊞ N') • γ = (N • γ) +UIR (N' • γ)
(N ⊠ N') • γ =  (N • γ) ×IR[ (λ Ps P's' → Ps ⊎ P's') , S.map ] (N' • γ)
(N ⊛ N') • γ = N • (N' • γ)



⟪_⟫IR : Nest -> UIR+
⟪ Id ⟫IR = δ₁ (ι (λ { (_ , X) → X _})) (λ f → ι→ι f)
⟪ K (S ▷ P) ⟫IR = σ (λ _ → S) (ι (λ { (_ , s) → P s })) 
⟪ F ⊞ G ⟫IR = ⟪ F ⟫IR +UIR ⟪ G ⟫IR
⟪ F ⊠ G ⟫IR = ⟪ F ⟫IR ×IR[(λ Ps P's' → Ps ⊎ P's') , S.map ] ⟪ G ⟫IR
⟪ F ⊛ G ⟫IR = F • ⟪ G ⟫IR