module Uniform.Constructions.Product
  (C : Set1)(HomC : C -> C -> Set)
  (idC : (c : C) -> HomC c c)
  (_∘C_ : {a b c : C} -> HomC b c -> HomC a b -> HomC a c)
  where

open import Data.Product as P
open import Function

import Uniform.posIR
open Uniform.posIR C HomC idC _∘C_

infixl  _×IR[_,_]_

mutual
  replace-ι : {Γ : Ctxt} ->
              (G : C -> C -> C)
              (Gmor : ∀ {a b a' b'} -> (f : HomC a b)(g : HomC a' b')
                                         -> HomC (G a a') (G b b')) ->
              IR' Γ -> (Env Γ -> C) -> IR' Γ
  replace-ι G Gmor (ι c') c = ι (λ e → G (c' e) (c e))
  replace-ι G Gmor (σ A γ) c = σ A (replace-ι G Gmor γ (c ∘ proj₁))
  replace-ι G Gmor (δ A γ γ→) c
    = δ A (replace-ι G Gmor γ (λ { (x , g) → c x }))
          (replace-ι-mor (idC _) ∘ γ→)

  replace-ι-mor : {Γ Δ : Ctxt} ->
                  {G : C -> C -> C}
                  {Gmor : ∀{a b a' b'} -> (f : HomC a b)(g : HomC a' b')
                                                   -> HomC (G a a') (G b b')} ->
              {e : Env Γ}{e' : Env Δ}{γ : IR' Γ}{ψ : IR' Δ} ->
              {c : Env Γ -> C}{c' : Env Δ -> C} ->
              HomC (c e) (c' e') -> Hom' e e' γ ψ ->  
              Hom' e e' (replace-ι G Gmor γ c) (replace-ι G Gmor ψ c')
  replace-ι-mor {Gmor = Gmor} h (ι→ι f) = ι→ι (Gmor f h)
  replace-ι-mor h (σ→σ f g) = σ→σ f (replace-ι-mor h ∘ g)
  replace-ι-mor h (δ→δ f g) = δ→δ f (replace-ι-mor h ∘ g)

syntax replace-ι G Gmor γ c = γ [ιx↦ι[ G , Gmor ][ c ,x]]

mutual
  _×IR[_,_]_ : {Γ : Ctxt} ->
               IR' Γ -> 
               (G : C -> C -> C) ->
               (Gmor : ∀{a b a' b'} -> (f : HomC a b)(g : HomC a' b')
                                              -> HomC (G a a') (G b b')) ->
               IR' Γ -> IR' Γ
  (ι c) ×IR[ G , Gmor ] ψ = ψ [ιx↦ι[ G , Gmor ][ c ,x]]
  (σ A γ) ×IR[ G , Gmor ] ψ = σ A (γ ×IR[ G , Gmor ] (IRwkσ ψ))
  _×IR[_,_]_ {Γ} (δ A γ γ→) G Gmor ψ
    = δ A (γ ×IR[ G , Gmor ] (IRwkδ ψ))
          (λ {e} {f} {g} η → _×IR[_,_]-mor_ {Γ' = Γ ,δ A} {Γ'' = Γ ,δ A}
                                            {e'' = e , g} {γ' = γ}
                                            (γ→ η) G Gmor
                                            (HomcMor _ _ (idIR' ψ)))

  _×IR[_,_]-mor_ : {Γ Γ' Γ'' : Ctxt} ->
                  {e e' : Env Γ}{e'' : Env Γ'}
                  {γ : IR' Γ}{γ' : IR' Γ}{ψ ψ' : IR' Γ} ->
                  Hom' e e' γ γ -> 
                  (G : C -> C -> C) ->
                  (Gmor : ∀{a b a' b'} -> (f : HomC a b)(g : HomC a' b')
                                                  -> HomC (G a a') (G b b')) ->
                  Hom' e e' ψ ψ' -> 
                  Hom' e e' (γ ×IR[ G , Gmor ] ψ) (γ ×IR[ G , Gmor ] ψ')
  (ι→ι f) ×IR[ G , Gmor ]-mor h = replace-ι-mor f h
  _×IR[_,_]-mor_ {Γ' = Γ'} {Γ''} {e'' = e''} {σ A γ} (σ→σ f g) G Gmor h
    = σ→σ f (λ x → _×IR[_,_]-mor_ {Γ' = Γ'} {Γ''} {e'' = e''} {γ' = γ} (g x) G Gmor (HomcMor _ _ h))
  _×IR[_,_]-mor_ {Γ' = Γ'} {Γ''} {e'' = e''} {δ A γ γ→} (δ→δ f g) G Gmor h
    = δ→δ f (λ k → _×IR[_,_]-mor_ {Γ' = Γ'} {Γ''} {e'' = e''} {γ' = γ} (g k) G Gmor (HomcMor _ _ h))