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

```