Coinductive universes in Polarity (see: https://polarity-lang.github.io/oopsla24/)

univ.pol

-- ------------------------------- --
-- Base types                      --
-- ------------------------------- --

data Top {
    Unit,
}

data Bot { }

codata Fun(a b: Type) {
  Fun(a, b).ap(a b: Type, x: a): b,
}

codata DFun(a: Type, b: a -> Type) {
  DFun(a, b).dap(a: Type, b: a -> Type, x: a): b.ap(a, Type, x),
}

codata Pair(a b: Type) {
  Pair(a, b).fst(a b: Type): a,
  Pair(a, b).snd(a b: Type): a,
}

codata DPair(a: Type, b: a -> Type) {
  DPair(a, b).dfst(a: Type, b: a -> Type): a,
  (self: DPair(a, b)).dsnd(a: Type, b: a -> Type): b.ap(a, Type, self.dfst(a, b)),
}

data Eq(a: Type, x y: a) {
    Refl(a: Type, x: a): Eq(a, x, x),
}

data W(a: Type, b: a -> Type) {
    Sup(a: Type, b: a -> Type, x: a, f: b.ap(a, Type, x) -> W(a, b)): W(a, b),
}

-- ------------------------------- --
-- Universe of types               --
-- ------------------------------- --

-- | An open universe of types, allowing for new type formers 
-- | to be added to the theory without redefining `U`. See:
-- | https://www.cmu.edu/dietrich/philosophy/hott/slides/shulman-2022-05-12.pdf
codata U {
    -- | Decode a universe into a type
    U.el: Type,
}

codef Top': U {
    el => Top,
}

codef Bot': U {
    el => Bot,
}

codef DFun'(a: U, b: a.el -> U): U {
    el => DFun(a.el, \x. b.ap(a.el, U, x).el),
}

codef DPair'(a: U, b: a.el -> U): U {
    el => DPair(a.el, \x. b.ap(a.el, U, x).el),
}

codef Eq'(a: U, x y: a.el): U {
    el => Eq(a.el, x, y),
}

codef W'(a: U, b: a.el -> U): U {
    el => W(a.el, \x. b.ap(a.el, U, x).el),
}