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.3-Ljl5wY0h7qEDjMk20qhhzf" '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 Source #
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.3-Ljl5wY0h7qEDjMk20qhhzf" 'False) (C1 ('MetaCons "IsFibrant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsStrict" 'PrefixI 'False) (U1 :: Type -> Type))