module Uniform.Constructions
  (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.Unit
open import Data.Product

import Prelude
open Prelude C HomC idC _∘C_

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

--------------------------------------
δ₁ : {Γ : Ctxt} ->
     (γ : IR' (Γ ,δ λ _ → ⊤)) ->
     (γ→ : ∀ {e f g} -> HomC f g -> Hom' (e , λ _ → f) (e , λ _ → g) γ γ)
       -> IR' Γ
δ₁ γ γ→ = δ (λ _ → ⊤) γ (λ η → γ→ (η _))
--------------------------------------

-- Splitting up the interpretation in index part and family part

⟦_⟧₀IR' : {Γ : Ctxt} -> IR' Γ -> Env Γ -> FamC -> Set
⟦ γ ⟧₀IR' e UT = index (⟦ γ ⟧IR' e UT)

⟦_⟧₁IR' : {Γ : Ctxt} -> (γ : IR' Γ) -> (e : Env Γ) -> (UT : FamC) ->
          ⟦ γ ⟧₀IR' e UT -> C
⟦ γ ⟧₁IR' e UT = fam (⟦ γ ⟧IR' e UT)