// Interval arithmetic
prim I
prim intervalInv (i : I) : I
prim intervalMin (i j : I) : I
prim intervalMax (i j : I) : I

// String and operations
prim String: Type
prim strcat (str1 str2: String) : String

// Coercion rules
prim coe (r s : I) (A : I → Type) : A r → A s

// Partial and subtypes
prim Partial (φ : I) (A : Type) : Set
prim Sub (A : Type) (φ : I) (Partial φ A) : Set
prim inS {A : Type} {φ : I} (x : A) : Sub A φ ⦃ φ := x ⦄
prim outS {A : Type} {φ : I} {p : Partial φ A} (x : Sub A φ p) : A