type-settheory-0.1.2: Type-level sets and functions expressed as types
Contents
Index
Search:
:***:
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
::∈:
Type.Set
:==:
Type.Set
:~>:
Type.Function
:~~>:
Type.Function
:×:
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
:∈:
Type.Set
:∩:
Type.Set
:∪:
Type.Set
:⊆:
Type.Set
:○:
Type.Function
adjustCod
Type.Function
All
1 (Type/Class)
Type.Logic
2 (Data Constructor)
Type.Logic
allElim
Type.Logic
ApplicativeType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
auto
Type.Logic
autoequality
Type.Set
autosubset
Type.Set
BiGraph
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
biGraphInjective
Type.Function
biGraphIsFun
Type.Function
biGraph_eq_HaskFun
Type.Function
BoundedType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
Cat
1 (Type/Class)
Data.Category
2 (Data Constructor)
Data.Category
cauto
Data.Category
CoKleisliType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
coKleisliType
Type.Set
complContradiction
Type.Set
Complement
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
complEmpty
Type.Set
complMaximal
Type.Set
Compo
Type.Function
compoId_Section
Type.Function
compoIsFun
Type.Function
compo_assoc
Type.Function
compo_idl
Type.Function
compo_idr
Type.Function
Const
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
constEq
Type.Function
constIsFun
Type.Function
COr
Type.Logic
DataType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
Decidable
1 (Type/Class)
Type.Logic
2 (Data Constructor)
Type.Logic
decide
Type.Logic
DependentSum
Type.Set
Diff
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
Disjoint
Type.Set
domUniq
Type.Function
dynCompare
Data.Typeable.Extras
dynEq
Data.Typeable.Extras
ecoerce
Type.Set
ecoerceFlip
Type.Set
elimComplement
Type.Set
elimCor
Type.Logic
elimDiff
Type.Set
elimEmpty
Type.Set
elimFalsity
Type.Logic
elimInter
Type.Set
elimInters
Type.Set
elimToTyCon
Type.Function
elimUnion
Type.Set
elimUnions
Type.Set
Empty
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
emptySubset
Type.Set
EnumType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
EqType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
Equaliser
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
EqualiserIncl
Type.Function
equaliserIsFun
Type.Function
equaliserSubset
Type.Function
equaliserUni
Type.Function
equal_f
Type.Function
equal_f_coerce
Type.Function
Ex
1 (Type/Class)
Type.Logic
2 (Data Constructor)
Type.Logic
ExampleSet
Type.Set.Example
ExC
1 (Type/Class)
Data.Category
2 (Data Constructor)
Data.Category
exElim
Type.Logic
ExFmap
1 (Type/Class)
Data.Category
2 (Data Constructor)
Data.Category
ExId
1 (Type/Class)
Data.Category
2 (Data Constructor)
Data.Category
ExSnd
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
extendCod
Type.Function
ExUniq
1 (Type/Class)
Type.Logic
2 (Data Constructor)
Type.Logic
ExUniq1
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
Fact
Type.Logic
Falsity
1 (Type/Class)
Type.Logic
2 (Data Constructor)
Type.Logic
FractionalType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
fromControlCategory
Data.Category
fromFunctor
Data.Category
fromTCG
Type.Function
Fst
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
fstIsFun
Type.Function
fstPrf
Type.Set
fst_tupling
Type.Function
fullImageOfInclusion
Type.Function
FunctionType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
functionType
Type.Set
FunctorType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
funEq
Type.Function
funEq'
Type.Function
getc
Data.Category
getCompare
Type.Set
getEq
Type.Set
getFmap
Type.Set
getfmap
Data.Category
getid
Data.Category
getShow
Type.Set
GFunctor
1 (Type/Class)
Data.Category
2 (Data Constructor)
Data.Category
Graph
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
graphCPS
Type.Function
graphInjective
Type.Function
graphIsFun
Type.Function
hask
Data.Category
HaskFun
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
haskFunInjective
Type.Function
haskFunIsFun
Type.Function
homIsFun
Data.Category
Id
Type.Function
idauto
Data.Category
idIsFun
Type.Function
idLemma
Type.Function
Image
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
imageCod
Type.Function
imageEmpty
Type.Function
imageGraphList
Type.Function
imageMonotonic
Type.Function
imageOfInclusion
Type.Function
imageUnion
Type.Function
image_Preimage
Type.Function
Incl
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
inclusionIsFun
Type.Function
inclusion_Injective
Type.Function
inCod
Type.Function
inDom
Type.Function
Initor
Type.Nat
initorFun
Type.Nat
InitorS
Type.Nat
InitorZ
Type.Nat
Injective
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
injective
Type.Function
injective_Inv
Type.Function
insert
Type.Set.Example
IntegralType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
Inter
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
interFst
Type.Set
interIdempotent
Type.Set
interMaximal
Type.Set
Inters
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
interSnd
Type.Set
intInExampleSet
Type.Set.Example
introToTyCon
Type.Function
Inv
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
invId
Type.Function
invInv
Type.Function
invInv0
Type.Function
IsFun
Type.Function
isFun_congruence
Type.Function
IsS
Type.Nat
IsZ
Type.Nat
kleisli
Data.Category
KleisliHom
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
kleisliHomInjective
Type.Function
kleisliHomIsFun
Type.Function
KleisliType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
kleisliType
Type.Set
lem
Type.Logic
liftCompare
Type.Set
liftEq
Type.Set
liftShowsPrec
Type.Set
lookup
Type.Set.Example
Lower
Type.Dummies
Lower1
Type.Dummies
Lower1Element
Type.Dummies
Lower2
Type.Dummies
Lower2Element
Type.Dummies
Lower3
Type.Dummies
LowerElement
Type.Dummies
lowerFun
Type.Function
makeCat
Data.Category
MonadPlusType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
MonadType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
MonoidType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
NInitial
1 (Type/Class)
Type.Nat
2 (Data Constructor)
Type.Nat
NMorphism
1 (Type/Class)
Type.Nat
2 (Data Constructor)
Type.Nat
Not
Type.Logic
NStructure
1 (Type/Class)
Type.Nat
2 (Data Constructor)
Type.Nat
NumType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
omapIsFun
Data.Category
OrdType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
PAIR
Type.Dummies
PAIR1
Type.Dummies
PAIR2
Type.Dummies
PAIR3
Type.Dummies
Powerset
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
powersetClosedDownwards
Type.Set
powersetEmpty
Type.Set
powersetInter
Type.Set
powersetMonotonic
Type.Set
powersetUnion
Type.Set
powersetWholeset
Type.Set
Preimage
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
preimage_Image
Type.Function
Prod
Type.Set
prodMonotonic
Type.Set
ProofSet
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
raiseFun
Type.Function
raiseFunCPS
Type.Function
ReadType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
rel
Type.Function
relation
Type.Function
relCPS
Type.Function
sap
Control.SMonad
sap'
Control.SMonad
sap'Default
Control.SMonad
SApplicative
Control.SMonad
sbind
Control.SMonad
sbind'
Control.SMonad
scoerce
Type.Set
Section
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
section_CompoId
Type.Function
setCodToImage
Type.Function
SetEq
Type.Set
setEqRefl
Type.Set
setEqSym
Type.Set
setEqTrans
Type.Set
sfmap
Control.SMonad
sfmap'
Control.SMonad
sfmap'Default
Control.SMonad
SFunctor
Control.SMonad
ShowType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
Singleton
Type.Set
singleton
Type.Set.Example
sjoin
Control.SMonad
sjoin'
Control.SMonad
sliftA2
Control.SMonad
sliftA2'
Control.SMonad
SMap
1 (Type/Class)
Type.Set.Example
2 (Data Constructor)
Type.Set.Example
SMonad
Control.SMonad
Snd
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
sndIsFun
Type.Function
sndPrf
Type.Set
snd_tupling
Type.Function
spure
Control.SMonad
spure'
Control.SMonad
sreturn
Control.SMonad
sreturn'
Control.SMonad
ssequence
Control.SMonad
ssequence'
Control.SMonad
stringInExampleSet
Type.Set.Example
Subset
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
subsetRefl
Type.Set
subsetTrans
Type.Set
Succ
1 (Type/Class)
Type.Nat
2 (Data Constructor)
Type.Nat
succFun
Type.Nat
Sval
Type.Function
sval
Type.Function
svalCoerce
Type.Function
svalCPS
Type.Function
svalCPS'
Type.Function
targetTuplingIsFun
Type.Function
test
Type.Set.Example
TNat
Type.Nat
Total
Type.Function
total
Type.Function
totalCPS
Type.Function
toTCG
Type.Function
ToTyCon
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
Truth
Type.Logic
TruthProof
Type.Logic
tupling_eta
Type.Function
tyconNStruct
Type.Nat
TypeableType
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
Union
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
unionIdempotent
Type.Set
unionL
Type.Set
unionMinimal
Type.Set
unionR
Type.Set
Unions
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
Univ
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
univSubset
Type.Set
V
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set
Π
1 (Type/Class)
Type.Function
2 (Data Constructor)
Type.Function
Σ
1 (Type/Class)
Type.Set
2 (Data Constructor)
Type.Set