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

icod_ :: Univ -> S Word32 Source #

value :: Word32 -> 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.7.20250510-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.7.20250510-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 Word32 Source #

icod_ :: IsFibrant -> S Word32 Source #

value :: Word32 -> 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 Source # 
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.7.20250510-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.7.20250510-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.