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