Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Syntax.Internal.Univ

Contents

Types
Universe kind arithmetic
- Inverting funUniv
Fibrancy
Printing

Description

Kinds of standard universes: Prop, Type, SSet.

Synopsis

data Univ
- = UProp
- | UType
- | USSet
data IsFibrant
- = IsFibrant
- | IsStrict
univUniv :: Univ -> Univ
funUniv :: Univ -> Univ -> Univ
domainUniv :: Bool -> Univ -> Univ -> Maybe Univ
codomainUniv :: Univ -> Univ -> Maybe Univ
univFibrancy :: Univ -> IsFibrant
showUniv :: Univ -> String

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 #
Bounded Univ Source #
Instance details Defined in Agda.Syntax.Internal.Univ Methods minBound :: Univ Source # maxBound :: Univ Source #
Enum Univ Source #
Instance details Defined in Agda.Syntax.Internal.Univ Methods succ :: Univ -> Univ Source # pred :: Univ -> Univ Source # toEnum :: Int -> Univ Source # fromEnum :: Univ -> Int Source # enumFrom :: Univ -> [Univ] Source # enumFromThen :: Univ -> Univ -> [Univ] Source # enumFromTo :: Univ -> Univ -> [Univ] Source # enumFromThenTo :: Univ -> Univ -> Univ -> [Univ] Source #
Generic Univ Source #
Instance details Defined in Agda.Syntax.Internal.Univ Associated Types type Rep Univ :: Type -> Type Source # Methods from :: Univ -> Rep Univ x Source # to :: Rep Univ x -> Univ Source #
Show Univ Source #
Instance details Defined in Agda.Syntax.Internal.Univ Methods showsPrec :: Int -> Univ -> ShowS Source # show :: Univ -> String Source # showList :: [Univ] -> ShowS Source #
NFData Univ Source #
Instance details Defined in Agda.Syntax.Internal.Univ Methods rnf :: Univ -> () Source #
Eq Univ Source #
Instance details Defined in Agda.Syntax.Internal.Univ Methods (==) :: Univ -> Univ -> Bool Source # (/=) :: Univ -> Univ -> Bool Source #
Ord Univ Source #
Instance details Defined in Agda.Syntax.Internal.Univ Methods compare :: Univ -> Univ -> Ordering Source # (<) :: Univ -> Univ -> Bool Source # (<=) :: Univ -> Univ -> Bool Source # (>) :: Univ -> Univ -> Bool Source # (>=) :: Univ -> Univ -> Bool Source # max :: Univ -> Univ -> Univ Source # min :: Univ -> Univ -> Univ Source #
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.4.1-7UUTMuNEKzk6ahO4JGfnDw" '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 #
Generic IsFibrant Source #
Instance details Defined in Agda.Syntax.Internal.Univ Associated Types type Rep IsFibrant :: Type -> Type Source # Methods from :: IsFibrant -> Rep IsFibrant x Source # to :: Rep IsFibrant x -> IsFibrant Source #
Show IsFibrant Source #
Instance details Defined in Agda.Syntax.Internal.Univ Methods showsPrec :: Int -> IsFibrant -> ShowS Source # show :: IsFibrant -> String Source # showList :: [IsFibrant] -> ShowS Source #
NFData IsFibrant Source #
Instance details Defined in Agda.Syntax.Internal Methods rnf :: IsFibrant -> () Source #
Eq IsFibrant Source #
Instance details Defined in Agda.Syntax.Internal.Univ Methods (==) :: IsFibrant -> IsFibrant -> Bool Source # (/=) :: IsFibrant -> IsFibrant -> Bool Source #
Ord IsFibrant Source #
Instance details Defined in Agda.Syntax.Internal.Univ Methods compare :: IsFibrant -> IsFibrant -> Ordering Source # (<) :: IsFibrant -> IsFibrant -> Bool Source # (<=) :: IsFibrant -> IsFibrant -> Bool Source # (>) :: IsFibrant -> IsFibrant -> Bool Source # (>=) :: IsFibrant -> IsFibrant -> Bool Source # max :: IsFibrant -> IsFibrant -> IsFibrant Source # min :: IsFibrant -> IsFibrant -> IsFibrant Source #
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.4.1-7UUTMuNEKzk6ahO4JGfnDw" 'False) (C1 ('MetaCons "IsFibrant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsStrict" 'PrefixI 'False) (U1 :: Type -> Type))