module Uniform.Constructions.Pi
  where

-- This module implements a "uniform pi" for uniform IR+(Set^op) codes.
-- As a special case, we get a code K → γ for exponentiation with
-- a set K.


open import Data.Product as P
open import Function

import Prelude
open Prelude Set  A B  B -> A)  c  id)  f g  g  f)



import Uniform.posIR
open Uniform.posIR Set  A B  B -> A)
                    c  id)  f g  g  f)

import Uniform.Shape
open Uniform.Shape Set  A B  B -> A)  c  id)  f g  g  f)


private
  C : Set1
  C = Set
  
  HomC : Set -> Set -> Set
  HomC =  A B  B -> A)


-- inversion for IR morphisms
extractι→ι : {Γ Δ : Ctxt}{e : Env Γ}{e' : Env Δ} -> 
                     {c : Env Γ -> C}{c' : Env Δ -> C} ->
                     Hom' {Γ} {Δ} e e' (ι c) (ι c') -> HomC (c e) (c' e')
extractι→ι (ι→ι g) = g

extractσ→σ :  {Γ Δ A B γ γ'}-> {e : Env Γ}{e' : Env Δ} -> 
              Hom' {Γ} {Δ} e e' (σ A γ) (σ B γ') ->
              Σ[ f  (A e -> B e')] ((x : A e) -> Hom' (e , x) (e' , f x) γ γ')
extractσ→σ (σ→σ f g) = f , g

extractδ→δ :  {Γ Δ e e' A B γ γ'} ->
              {γ→ :  {e}{f g : A e -> C} -> ((a : A e) -> HomC (f a) (g a)) ->
                  Hom' {Γ  A} {Γ  A} (e , f) (e , g) γ γ} ->
              {γ'→ :  {e f g} -> ((a : B e) -> HomC (f a) (g a)) ->
                  Hom' {Δ  B} {Δ  B} (e , f) (e , g) γ' γ'} ->
              Hom' {Γ} {Δ} e e' (δ A γ γ→) (δ B γ' γ'→) ->
              Σ[ f  (B e' -> A e) ]
                  ((h : A e -> C) -> Hom' (e , h) (e' , h  f) γ γ')
extractδ→δ (δ→δ f g) = f , g



mutual
  {-# TERMINATING #-} -- IRcMor preserves structure, but Agda can't see it;
                      -- could use sized types to fix this
  _⇒_ : {Γ : Ctxt} -> (K : Env Γ -> Set) -> IR' (Γ  K) -> IR' Γ
  K  (ι c) = ι  e  Σ[ x  (K e) ] (c (e , x))) 
  K  (σ A γ) = σ  e  (x : K e) -> A (e , x))
                  ((K  proj₁)   (IRcMor  x  let y = proj₁ (proj₁ x)
                                                     f = proj₂ (proj₁ x)
                                                     k = proj₂ x
                                                 in (y , k) , f k ) γ))
  K  (δ A γ γ→)
   = δ  e  Σ[ x  K e ] A (e , x))
       ((K  proj₁)  IRcMor  x  let y = proj₁ (proj₁ x)
                                        F = proj₂ (proj₁ x)
                                        k = proj₂ x
                                    in (y , k) , λ a  F (k , a)) γ)
        {e} {f} {g} η  ⇒-mor (K  proj₁) (K  proj₁) id _ _ (refl-shape (IRcMor _ γ))  {k}  HomcMor _ _ (γ→  a  η (k , a)))) )

  ⇒-mor : {Γ Δ : Ctxt} ->
           (K : Env Γ -> Set) ->
           (K' : Env Δ -> Set) ->
           {e : Env Γ}{e' : Env Δ} ->
           (h : K' e' -> K e) ->
           (γ : IR' (Γ  K))(γ' : IR' (Δ  K')) ->
           same-shape γ γ' ->
           ({k : K' e'} -> Hom' (e , h k) (e' , k) γ γ') ->
           Hom' e e' (K  γ) (K'  γ')
  ⇒-mor K K' h (ι c) (ι c') p f = ι→ι (P.map h  {k}  extractι→ι (f {k})))
  ⇒-mor K K' h (ι x) (σ A γ') () f 
  ⇒-mor K K' h (ι x) (δ A γ' γ→) () f
  ⇒-mor K K' h (σ A γ) (ι x) () f
  ⇒-mor K K' h (σ A γ) (σ B γ') p f = σ→σ  g k  proj₁ (extractσ→σ (f {k})) (g (h k)))  g  ⇒-mor (K  proj₁) (K'  proj₁) h (IRcMor _ γ) (IRcMor _ γ') (IRcMor-preserves-shape γ γ' p)  {k}  HomcMor _ _ (proj₂ (extractσ→σ (f {k})) (g (h k)))))
  ⇒-mor K K' h (σ A γ) (δ A₁ γ' γ→) () f
  ⇒-mor K K' h (δ A γ γ→) (ι x) () f
  ⇒-mor K K' h (δ A γ γ→) (σ A₁ γ') () f
  ⇒-mor K K' h (δ A γ γ→) (δ A₁ γ' γ→₁) p f = δ→δ (P.map h  {x}  proj₁ (extractδ→δ (f {x}))))  g  ⇒-mor (K  proj₁) (K'  proj₁) h _ _ (IRcMor-preserves-shape γ γ' p)  {k}  HomcMor _ _ (proj₂ (extractδ→δ (f {k}))  a  g ((h k) , a)))))