Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Internal.Univ

Description

Kinds of standard universes: Prop, Type, SSet.

Synopsis

Types

data Univ Source #

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

Constructors

UProp

Fibrant universe of propositions.

UType

Fibrant universe.

USSet

Non-fibrant universe.

Instances

Instances details
EmbPrj Univ Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Univ -> S Int32 Source #

icod_ :: Univ -> S Int32 Source #

value :: Int32 -> R Univ Source #

NFData Univ Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

Methods

rnf :: Univ -> ()

Bounded Univ Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

Methods

minBound :: Univ

maxBound :: Univ

Enum Univ Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

Associated Types

type Rep Univ 
Instance details

Defined in Agda.Syntax.Internal.Univ

type Rep Univ = D1 ('MetaData "Univ" "Agda.Syntax.Internal.Univ" "Agda-2.6.20240714-inplace" '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)))

Methods

from :: Univ -> Rep Univ x

to :: Rep Univ x -> Univ

Show Univ Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

Methods

showsPrec :: Int -> Univ -> ShowS

show :: Univ -> String

showList :: [Univ] -> ShowS

Eq Univ Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

Methods

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

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

Ord Univ Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

type Rep Univ = D1 ('MetaData "Univ" "Agda.Syntax.Internal.Univ" "Agda-2.6.20240714-inplace" '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 Source #

We have IsFibrant < IsStrict.

Constructors

IsFibrant

Fibrant universe.

IsStrict

Non-fibrant universe.

Instances

Instances details
EmbPrj IsFibrant Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: IsFibrant -> S Int32 Source #

icod_ :: IsFibrant -> S Int32 Source #

value :: Int32 -> R IsFibrant Source #

Boolean IsFibrant Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

Methods

fromBool :: Bool -> IsFibrant Source #

true :: IsFibrant Source #

false :: IsFibrant Source #

not :: IsFibrant -> IsFibrant Source #

(&&) :: IsFibrant -> IsFibrant -> IsFibrant Source #

(||) :: IsFibrant -> IsFibrant -> IsFibrant Source #

implies :: IsFibrant -> IsFibrant -> IsFibrant Source #

butNot :: IsFibrant -> IsFibrant -> IsFibrant Source #

IsBool IsFibrant Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

Methods

toBool :: IsFibrant -> Bool Source #

ifThenElse :: IsFibrant -> b -> b -> b Source #

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

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

NFData IsFibrant 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: IsFibrant -> ()

Generic IsFibrant Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

Associated Types

type Rep IsFibrant 
Instance details

Defined in Agda.Syntax.Internal.Univ

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

Methods

from :: IsFibrant -> Rep IsFibrant x

to :: Rep IsFibrant x -> IsFibrant

Show IsFibrant Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

Methods

showsPrec :: Int -> IsFibrant -> ShowS

show :: IsFibrant -> String

showList :: [IsFibrant] -> ShowS

Eq IsFibrant Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

Methods

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

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

Ord IsFibrant Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

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

Universe kind arithmetic

univUniv :: Univ -> Univ Source #

The successor universe type of a universe.

funUniv :: Univ -> Univ -> Univ Source #

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

Inverting funUniv

domainUniv Source #

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 Source #

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 Source #

Fibrancy of standard universes.

Printing

showUniv :: Univ -> String Source #

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