module 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

-- Constructions on codes; for now only a non-dependent δ code.
-- More constructions can be found in Constructions.Product and
-- Constructions.Coproduct.

open import Data.Unit

import posIR
open posIR C HomC idC _∘C_


--------------------------
δ₁ : (F : C -> IR+)(F→ : ∀ {f g} -> (HomC f g) ->  Hom (F f) (F g)) -> IR+
δ₁ F F→ = δ ⊤ (λ f → F (f _)) (λ η → F→ (η _))
--------------------------