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 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 :: 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.4-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 #
Generic IsFibrant Source #
Instance details 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 Source #
Instance details Defined in Agda.Syntax.Internal.Univ Methods showsPrec :: Int -> IsFibrant -> ShowS show :: IsFibrant -> String showList :: [IsFibrant] -> ShowS
NFData IsFibrant
Instance details Defined in Agda.Syntax.Internal Methods rnf :: IsFibrant -> ()
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.4-inplace" 'False) (C1 ('MetaCons "IsFibrant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsStrict" 'PrefixI 'False) (U1 :: Type -> Type))