Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
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 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 -> () 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 |
Instance details Defined in Agda.Syntax.Internal.Univ type Rep Univ = D1 ('MetaData "Univ" "Agda.Syntax.Internal.Univ" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 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 #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "IsFibrant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsStrict" 'PrefixI 'False) (U1 :: Type -> Type))

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 #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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.