```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 2 _×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)

```