module Uniform.Intro
  (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

import Prelude
open Prelude C HomC idC _∘C_

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

mutual

  {-# NO_POSITIVITY_CHECK #-}
  data U (c : UIR+) : Set where
    intro : index (⟦ c ⟧UIR+ (U c , T)) -> U c

  {-# TERMINATING #-}
  T : {c : UIR+} -> U c -> C
  T {c} (intro x) = fam (⟦ c ⟧UIR+ (U c , T)) x

introMorphism : {c : UIR+} -> HomFamC (⟦ c ⟧UIR+ (U c , T)) (U c , T)
introMorphism = intro , (λ x → idC _)