ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Internal.Univ

Kinds of standard universes: Prop, Type, SSet.

Contents

Synopsis

Types

datadata Univ

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

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

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

datadata IsFibrant

We have IsFibrant < IsStrict.

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

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