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