Agda.Syntax.Internal.Univ

Kinds of standard universes: Prop, Type, SSet.

Types

data Univ

Flavor of standard universe (Prop < Type < SSet,).

Constructors

UProp

Fibrant universe of propositions.

UType

Fibrant universe.

USSet

Non-fibrant universe.

Instances

EmbPrj Univ

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Univ -> S Int32

icod_ :: Univ -> S Int32

value :: Int32 -> R Univ

Bounded Univ

Defined in Agda.Syntax.Internal.Univ

Methods

minBound :: Univ

maxBound :: Univ

Enum Univ

Defined in Agda.Syntax.Internal.Univ

Methods

succ :: Univ -> Univ

pred :: Univ -> Univ

toEnum :: Int -> Univ

fromEnum :: Univ -> Int

enumFrom :: Univ -> [Univ]

enumFromThen :: Univ -> Univ -> [Univ]

enumFromTo :: Univ -> Univ -> [Univ]

enumFromThenTo :: Univ -> Univ -> Univ -> [Univ]

Generic Univ

Defined in Agda.Syntax.Internal.Univ

Associated Types

type Rep Univ :: Type -> Type

Methods

from :: Univ -> Rep Univ x

to :: Rep Univ x -> Univ

Show Univ

Defined in Agda.Syntax.Internal.Univ

Methods

showsPrec :: Int -> Univ -> ShowS

show :: Univ -> String

showList :: [Univ] -> ShowS

NFData Univ

Defined in Agda.Syntax.Internal.Univ

Methods

rnf :: Univ -> ()

Eq Univ

Defined in Agda.Syntax.Internal.Univ

Methods

(==) :: Univ -> Univ -> Bool

(/=) :: Univ -> Univ -> Bool

Ord Univ

Defined in Agda.Syntax.Internal.Univ

Methods

compare :: Univ -> Univ -> Ordering

(<) :: Univ -> Univ -> Bool

(<=) :: Univ -> Univ -> Bool

(>) :: Univ -> Univ -> Bool

(>=) :: Univ -> Univ -> Bool

max :: Univ -> Univ -> Univ

min :: Univ -> Univ -> Univ

type Rep Univ

Defined in Agda.Syntax.Internal.Univ

type Rep Univ = D1 ('MetaData "Univ" "Agda.Syntax.Internal.Univ" "Agda-2.7.0-GLfwtYnpcYgL7izVkqfuSR" 'False) (C1 ('MetaCons "UProp" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "UType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "USSet" 'PrefixI 'False) (U1 :: Type -> Type)))

data IsFibrant

We have IsFibrant < IsStrict.

Constructors

IsFibrant

Fibrant universe.

IsStrict

Non-fibrant universe.

Instances

EmbPrj IsFibrant

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: IsFibrant -> S Int32

icod_ :: IsFibrant -> S Int32

value :: Int32 -> R IsFibrant

Boolean IsFibrant

Defined in Agda.Syntax.Internal.Univ

Methods

fromBool :: Bool -> IsFibrant

true :: IsFibrant

false :: IsFibrant

not :: IsFibrant -> IsFibrant

(&&) :: IsFibrant -> IsFibrant -> IsFibrant

(||) :: IsFibrant -> IsFibrant -> IsFibrant

implies :: IsFibrant -> IsFibrant -> IsFibrant

butNot :: IsFibrant -> IsFibrant -> IsFibrant

IsBool IsFibrant

Defined in Agda.Syntax.Internal.Univ

Methods

toBool :: IsFibrant -> Bool

ifThenElse :: IsFibrant -> b -> b -> b

fromBool1 :: (Bool -> Bool) -> IsFibrant -> IsFibrant

fromBool2 :: (Bool -> Bool -> Bool) -> IsFibrant -> IsFibrant -> IsFibrant

Generic IsFibrant

Defined in Agda.Syntax.Internal.Univ

Associated Types

type Rep IsFibrant :: Type -> Type

Methods

from :: IsFibrant -> Rep IsFibrant x

to :: Rep IsFibrant x -> IsFibrant

Show IsFibrant

Defined in Agda.Syntax.Internal.Univ

Methods

showsPrec :: Int -> IsFibrant -> ShowS

show :: IsFibrant -> String

showList :: [IsFibrant] -> ShowS

NFData IsFibrant

Defined in Agda.Syntax.Internal

Methods

rnf :: IsFibrant -> ()

Eq IsFibrant

Defined in Agda.Syntax.Internal.Univ

Methods

(==) :: IsFibrant -> IsFibrant -> Bool

(/=) :: IsFibrant -> IsFibrant -> Bool

Ord IsFibrant

Defined in Agda.Syntax.Internal.Univ

Methods

compare :: IsFibrant -> IsFibrant -> Ordering

(<) :: IsFibrant -> IsFibrant -> Bool

(<=) :: IsFibrant -> IsFibrant -> Bool

(>) :: IsFibrant -> IsFibrant -> Bool

(>=) :: IsFibrant -> IsFibrant -> Bool

max :: IsFibrant -> IsFibrant -> IsFibrant

min :: IsFibrant -> IsFibrant -> IsFibrant

type Rep IsFibrant

Defined in Agda.Syntax.Internal.Univ

type Rep IsFibrant = D1 ('MetaData "IsFibrant" "Agda.Syntax.Internal.Univ" "Agda-2.7.0-GLfwtYnpcYgL7izVkqfuSR" 'False) (C1 ('MetaCons "IsFibrant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsStrict" 'PrefixI 'False) (U1 :: Type -> Type))

Universe kind arithmetic

univUniv :: Univ -> Univ

The successor universe type of a universe.

funUniv :: Univ -> Univ -> Univ

Compute the universe type of a function space from the universe types of domain and codomain.

Inverting funUniv

domainUniv

Arguments

:: Bool

Have UProp?

-> Univ

Univ kind of the funSort.

-> Univ

Univ kind of the codomain.

-> Maybe Univ

Univ kind of the domain, if unique.

Conclude u1 from funUniv u1 u2 and u2.

codomainUniv

Arguments

:: Univ

Univ kind of the funSort.

-> Univ

Univ kind of the domain.

-> Maybe Univ

Univ kind of the codomain, if uniquely exists.

Conclude u2 from funUniv u1 u2 and u1.

Fibrancy

univFibrancy :: Univ -> IsFibrant

Fibrancy of standard universes.

Printing

showUniv :: Univ -> String

Hacky showing of standard universes, does not take actual names into account.