```module posIR
(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.Empty
open import Data.Unit
open import Data.Product
open import Function

import Prelude
open Prelude C HomC idC _∘C_

-- IR+ codes and IR+ morphisms -----------------------------------

mutual
data IR+ : Set1 where
ι : C -> IR+
σ : (A : Set) -> (f : A -> IR+) -> IR+
δ : (A : Set) -> (F : (A -> C) -> IR+) ->
(F→ : ∀ {f g} -> ((a : A) -> HomC (f a) (g a)) -> Hom (F f) (F g))
-> IR+

data Hom : IR+ → IR+ → Set1 where
ι→ι : {c c' : _} → HomC c c' → Hom (ι c) (ι c')
σ→σ : {A : _}{f : _}{B : _}{g : _} ->
(h : A -> B) ->
((a : A) → Hom (f a) ((g ∘ h) a)) → Hom (σ A f) (σ B g)
δ→δ : {A : Set}{F : _}
{F→ : ∀ {f g} -> ((a : A) -> HomC (f a) (g a)) -> Hom (F f) (F g)}
{B : Set}{G : _}
{G→ : ∀ {f g} -> ((a : B) -> HomC (f a) (g a)) -> Hom (G f) (G g)} ->
(g : B -> A) ->
((h : A -> C) -> Hom (F h) (G (h ∘ g)))
-> Hom (δ A F F→) (δ B G G→)

------------------------------------------------------------------

-- Identity ------------------------------------------------------

idIR+ : {γ : IR+} -> Hom γ γ
idIR+ {ι c} = ι→ι (idC c)
idIR+ {σ A f} = σ→σ id (λ a → idIR+ {f a})
idIR+ {δ A F F→} = δ→δ id (λ h → idIR+ {F h})

-- Composition ---------------------------------------------------

_∘IR+_ : {a b c : IR+} -> Hom b c -> Hom a b -> Hom a c
ι→ι f ∘IR+ ι→ι g = ι→ι (f ∘C g)
σ→σ h γ ∘IR+ σ→σ g φ = σ→σ (h ∘ g) (λ a → γ (g a) ∘IR+ φ a)
δ→δ h γ ∘IR+ δ→δ g φ = δ→δ (g ∘ h) (λ k → γ (k ∘ g) ∘IR+ φ k)

------------------------------------------------------------------

-- Decoding ------------------------------------------------------

-- Object part

⟦_⟧IR+ : IR+ -> FamC -> FamC
⟦ ι c ⟧IR+  UT = ⊤ , (λ _ → c)
⟦ σ A f ⟧IR+  UT = ΣFamC A (λ a → ⟦ f a ⟧IR+ UT)
⟦ δ A F _ ⟧IR+ (U , T) = ΣFamC (A -> U) (λ g → ⟦ F (T ∘ g) ⟧IR+ (U , T))

-- Morphism part

mutual
-- not really mutual, ⟦_⟧Hom does not depend on ⟦_⟧→ ...
-- However, if one considers ⟦_⟧IR+ and ⟦_⟧→ to be defined together
-- (object and morphism part of the same functor), then there really
-- is a mutual dependency.

⟦_⟧→ : (γ : IR+) -> {A B : FamC} ->
HomFamC A B -> HomFamC (⟦ γ ⟧IR+ A) (⟦ γ ⟧IR+ B)
⟦ ι c ⟧→ hk = idFamC
⟦ σ A f ⟧→ hk = [ inA a ∘FamC (⟦ f a ⟧→ hk) ][ a ∈ A ]
⟦ δ A F F→ ⟧→ {X , P} {Y , Q} (h , k)
= [ inA {B = λ g → ⟦ F (Q ∘ g) ⟧IR+ (Y , Q)} (h ∘ g)
∘FamC (⟦ F→ (k ∘ g) ⟧Hom (Y , Q)
∘FamC ⟦ F (P ∘ g) ⟧→ (h , k)) ][ g ∈ _ ]

⟦_⟧Hom : {γ γ' : IR+} -> Hom γ γ' -> (X : FamC) ->
HomFamC (⟦ γ ⟧IR+ X) (⟦ γ' ⟧IR+ X)
⟦ ι→ι f ⟧Hom UT = id , (λ _ → f)
⟦ σ→σ h γ ⟧Hom UT = ΣFamCmor h (λ a → ⟦ γ a ⟧Hom UT )
⟦ δ→δ g γ ⟧Hom (U , T) = ΣFamCmor (λ z → z ∘ g)
(λ k → ⟦ γ (T ∘ k) ⟧Hom (U , T))
```