Agda-2.6.3.20230805: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
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

Bounded Univ Source # 
Instance details

Defined in Agda.Syntax.Internal.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 :: 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 #

NFData Univ Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

Methods

rnf :: Univ -> () #

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.3.20230805-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

Boolean IsFibrant Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

IsBool IsFibrant Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

Generic IsFibrant Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

Associated Types

type Rep IsFibrant :: Type -> Type #

Show IsFibrant Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

NFData IsFibrant Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: IsFibrant -> () #

Eq IsFibrant Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

Ord IsFibrant Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

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.3.20230805-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.