ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Internal.Univ

Kinds of standard universes: Prop, Type, SSet.

Types

2 declarations

datadata Univ

Flavor of standard universe (Prop < Type < SSet,).

Instances9Bounded, Enum, Eq, Ord, Show, Generic, …

Bounded UnivDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Univ
Enum UnivDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Univ
Eq UnivDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Univ
Ord UnivDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Univ
Show UnivDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Univ
Generic UnivDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Univ
NFData UnivDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Univ
EmbPrj UnivDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Internal · orphan
type Rep Univ = D1 ('MetaData "Univ" "Agda.Syntax.Internal.Univ" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) (C1 ('MetaCons "UProp" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "UType" 'PrefixI 'False) U1 :+: C1 ('MetaCons "USSet" 'PrefixI 'False) U1))Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Univ

datadata IsFibrant

We have IsFibrant < IsStrict.

Instances9Eq, Ord, Show, Generic, NFData, Boolean, …

Eq IsFibrantDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Univ
Ord IsFibrantDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Univ
Show IsFibrantDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Univ
Generic IsFibrantDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Univ
NFData IsFibrantDefined in Agda-2.7.0.1 · Agda.Syntax.Internal · orphan
Boolean IsFibrantDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Univ
IsBool IsFibrantDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Univ
EmbPrj IsFibrantDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Internal · orphan
type Rep IsFibrant = D1 ('MetaData "IsFibrant" "Agda.Syntax.Internal.Univ" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) (C1 ('MetaCons "IsFibrant" 'PrefixI 'False) U1 :+: C1 ('MetaCons "IsStrict" 'PrefixI 'False) U1)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Univ

2 declarations

valueunivUniv :: Univ -> Univ

The successor universe type of a universe.

valuefunUniv :: Univ -> Univ -> Univ

Compute the universe type of a function space from the universe types of domain and codomain.

valuedomainUniv

Conclude u1 from funUniv u1 u2 and u2.

valuecodomainUniv

Conclude u2 from funUniv u1 u2 and u1.

1 declaration

valueunivFibrancy :: Univ -> IsFibrant

Fibrancy of standard universes.

1 declaration

valueshowUniv :: Univ -> String

Hacky showing of standard universes, does not take actual names into account.