module 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 posIR
open posIR C HomC idC _∘C_

infixl  _×IR[_,_]_

mutual
  replace-ι : (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+ -> C -> IR+
  replace-ι G Gmor (ι c') c = ι (G c c')
  replace-ι G Gmor (σ A f) c = σ A (λ a → replace-ι G Gmor (f a) c)
  replace-ι G Gmor (δ A F F→) c = δ A (λ k → replace-ι G Gmor (F k) c)
                                      (λ {f} {g} η → replace-ι-mor G Gmor (F f) (F g) c (F→ η))

  replace-ι-mor : (G : C -> C -> C)
                  (Gmor : ∀{a b a' b'} -> (f : HomC a b)(g : HomC a' b')
                                                   -> HomC (G a a') (G b b')) ->
              (x y : IR+) -> (c : C) ->
              Hom x y -> 
              Hom (replace-ι G Gmor x c) (replace-ι G Gmor y c)
  replace-ι-mor G Gmor (ι c) (ι c') d (ι→ι f) = ι→ι (Gmor (idC d) f)
  replace-ι-mor G Gmor (ι x) (σ A f) d ()
  replace-ι-mor G Gmor (ι x) (δ A F F→) d ()
  replace-ι-mor G Gmor (σ A f) (ι x) d ()
  replace-ι-mor G Gmor (σ A f) (σ B g) d (σ→σ h γ)
    = σ→σ h (λ a → replace-ι-mor G Gmor (f a) (g (h a)) d (γ a))
  replace-ι-mor G Gmor (σ A f) (δ A₁ F F→) d ()
  replace-ι-mor G Gmor (δ A F F→) (ι x) d ()
  replace-ι-mor G Gmor (δ A F F→) (σ A₁ f) d ()
  replace-ι-mor G Gmor (δ A F F→) (δ B H H→) d (δ→δ g γ)
    = δ→δ g (λ k → replace-ι-mor G Gmor (F k) (H (k ∘ g)) d (γ k))

replace-ι-morC : (G : C -> C -> C)
                 (Gmor : ∀{a b a' b'} -> (f : HomC a b)(g : HomC a' b')
                                            -> HomC (G a a') (G b b')) ->
                 (x : IR+) -> (c c' : C) -> HomC c c' -> 
                 Hom (replace-ι G Gmor x c) (replace-ι G Gmor x c')
replace-ι-morC G Gmor (ι d) c c' g = ι→ι (Gmor g (idC d))
replace-ι-morC G Gmor (σ A f) c c' g
  = σ→σ id (λ a → replace-ι-morC G Gmor (f a) c c' g)
replace-ι-morC G Gmor (δ A F F→) c c' g
  = δ→δ id (λ k → replace-ι-morC G Gmor (F k) c c' g)

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

mutual
  _×IR[_,_]_  : 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 ] γ = replace-ι G Gmor γ c
  (σ A f) ×IR[ G , Gmor ] γ = σ A (λ a → (f a) ×IR[ G , Gmor ] γ)
  (δ A F F→) ×IR[ G , Gmor ] γ = δ A (λ a → (F a) ×IR[ G , Gmor ] γ)
                                 (λ η → (F→ η) ×IR[ G , Gmor ]-mor)

  _×IR[_,_]-mor : {x y : IR+} ->
                  Hom x y -> 
                  (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+} ->
                  Hom (x ×IR[ G , Gmor ] γ) (y ×IR[ G , Gmor ] γ)
  (ι→ι f)   ×IR[ G , Gmor ]-mor = replace-ι-morC G Gmor _ _ _ f
  (σ→σ f g) ×IR[ G , Gmor ]-mor = σ→σ f (λ a → (g a) ×IR[ G , Gmor ]-mor)
  (δ→δ f g) ×IR[ G , Gmor ]-mor = δ→δ f (λ h → (g h) ×IR[ G , Gmor ]-mor)