- Sets are encoded as certain types of kind
* -> *
- A value of type
S X
is a proof that the typeX
is a member ofS
- type :∈: a set = set a
- data set1 :⊆: set2 where
- scoerce :: (set1 :⊆: set2) -> (a :∈: set1) -> a :∈: set2
- type Subset = :⊆:
- data set1 :==: set2 = SetEq (set1 :⊆: set2) (set2 :⊆: set1)
- ecoerce :: (s1 :==: s2) -> (a :∈: s1) -> a :∈: s2
- ecoerceFlip :: (s1 :==: s2) -> (a :∈: s2) -> a :∈: s1
- subsetRefl :: s :⊆: s
- subsetTrans :: (s1 :⊆: s2) -> (s2 :⊆: s3) -> s1 :⊆: s3
- setEqRefl :: s :==: s
- setEqSym :: (s1 :==: s2) -> s2 :==: s1
- setEqTrans :: (s1 :==: s2) -> (s2 :==: s3) -> s1 :==: s3
- type Singleton a = :=: a
- data s1 :∪: s2 where
- elimUnion :: (a :∈: (s1 :∪: s2)) -> Either (a :∈: s1) (a :∈: s2)
- type Union = :∪:
- unionL :: s1 :⊆: (s1 :∪: s2)
- unionR :: s2 :⊆: (s1 :∪: s2)
- unionMinimal :: (s1 :⊆: t) -> (s2 :⊆: t) -> (s1 :∪: s2) :⊆: t
- unionIdempotent :: (s :∪: s) :==: s
- data s1 :∩: s2 where
- elimInter :: (a :∈: (s1 :∩: s2)) -> (a :∈: s1, a :∈: s2)
- interFst :: (s1 :∩: s2) :⊆: s1
- interSnd :: (s1 :∩: s2) :⊆: s2
- type Inter = :∩:
- interMaximal :: (t :⊆: s1) -> (t :⊆: s2) -> t :⊆: (s1 :∩: s2)
- interIdempotent :: (s :∩: s) :==: s
- data Unions fam where
- elimUnions :: Unions fam a -> (forall s. (Lower s :∈: fam) -> (a :∈: s) -> r) -> r
- data Σ fam where
- type DependentSum = Σ
- data Inters fam where
- elimInters :: Inters fam a -> (Lower s :∈: fam) -> s a
- data Complement s where
- Complement :: Not (a :∈: s) -> Complement s a
- elimComplement :: (a :∈: Complement s) -> Not (a :∈: s)
- type Disjoint s1 s2 = (s1 :∩: s2) :⊆: Empty
- complContradiction :: Not (s a, Complement s a)
- complEmpty :: Disjoint s (Complement s)
- complMaximal :: Disjoint s t -> t :⊆: Complement s
- data Diff s t where
- elimDiff :: (a :∈: Diff s t) -> (a :∈: s, Not (a :∈: t))
- data s1 :×: s2 where
- type Prod = :×:
- fstPrf :: ((a, b) :∈: (s1 :×: s2)) -> a :∈: s1
- sndPrf :: ((a, b) :∈: (s1 :×: s2)) -> b :∈: s2
- prodMonotonic :: (s1 :⊆: t1) -> (s2 :⊆: t2) -> (s1 :×: s2) :⊆: (t1 :×: t2)
- data Empty where
- elimEmpty :: Empty a -> b
- emptySubset :: Empty :⊆: s
- data Univ where
- univSubset :: s :⊆: Univ
- data FunctionType where
- FunctionType :: FunctionType (a -> b)
- functionType :: (a -> b) :∈: FunctionType
- data KleisliType m where
- KleisliType :: KleisliType m (a -> m b)
- kleisliType :: (a -> m b) :∈: KleisliType m
- data CoKleisliType w where
- CoKleisliType :: CoKleisliType w (w a -> b)
- coKleisliType :: (w a -> b) :∈: CoKleisliType w
- data ShowType where
- getShow :: (a :∈: ShowType) -> a -> String
- data ReadType where
- data EqType where
- getEq :: (a :∈: EqType) -> a -> a -> Bool
- data OrdType where
- getCompare :: (a :∈: OrdType) -> a -> a -> Ordering
- data EnumType where
- data BoundedType where
- BoundedType :: Bounded a => BoundedType a
- data NumType where
- data IntegralType where
- IntegralType :: Integral a => IntegralType a
- data MonoidType where
- MonoidType :: Monoid a => MonoidType a
- data FractionalType where
- FractionalType :: Fractional a => FractionalType a
- data TypeableType where
- TypeableType :: Typeable a => TypeableType a
- data DataType where
- data FunctorType where
- FunctorType :: Functor a => FunctorType (Lower a)
- getFmap :: (Lower f :∈: FunctorType) -> (a -> b) -> f a -> f b
- data MonadType where
- data MonadPlusType where
- MonadPlusType :: MonadPlus a => MonadPlusType (Lower a)
- data ApplicativeType where
- ApplicativeType :: Applicative a => ApplicativeType (Lower a)
- type ::∈: a set = set (Lower a)
- data Powerset u where
- powersetWholeset :: u ::∈: Powerset u
- powersetEmpty :: Empty ::∈: Powerset u
- powersetUnion :: (s1 ::∈: Powerset u) -> (s2 ::∈: Powerset u) -> (s1 :∪: s2) ::∈: Powerset u
- powersetInter :: (s1 ::∈: Powerset u) -> (s2 ::∈: Powerset u) -> (s1 :∩: s2) ::∈: Powerset u
- powersetMonotonic :: (u1 :⊆: u2) -> (s ::∈: Powerset u1) -> s ::∈: Powerset u2
- powersetClosedDownwards :: (s1 :⊆: s2) -> (s2 ::∈: Powerset u) -> s1 ::∈: Powerset u
- autosubset :: Fact (s :⊆: t) => s :⊆: t
- autoequality :: Fact (s :==: t) => s :==: t
- data ProofSet s where
- data ExUniq1 p where
- data V s where
- liftEq :: (s :⊆: EqType) -> (s :⊆: TypeableType) -> V s -> V s -> Bool
- liftCompare :: (s :⊆: OrdType) -> (s :⊆: TypeableType) -> V s -> V s -> Ordering
- liftShowsPrec :: Typeable1 s => (s :⊆: ShowType) -> (s :⊆: TypeableType) -> Int -> V s -> ShowS
Subsets, equality
data set1 :⊆: set2 whereSource
Represents a proof that set1
is a subset of set2
Fact (Disjoint s t -> :⊆: t (Complement s)) | |
Fact (:⊆: set1 set2 -> :∈: a set1 -> :∈: a set2) | |
Fact (:⊆: s1 t -> :⊆: s2 t -> :⊆: (:∪: s1 s2) t) | |
Fact (:⊆: t s1 -> :⊆: t s2 -> :⊆: t (:∩: s1 s2)) | |
Fact (:⊆: u1 u2 -> ::∈: s (Powerset u1) -> ::∈: s (Powerset u2)) | |
Fact (:⊆: s1 s2 -> ::∈: s2 (Powerset u) -> ::∈: s1 (Powerset u)) | |
Fact (:⊆: s1 s2 -> :⊆: s2 s3 -> :⊆: s1 s3) | |
Fact (:⊆: s1 t1 -> :⊆: s2 t2 -> :⊆: (:×: s1 s2) (:×: t1 t2)) | |
(cod' ~ cod'_copy, Fact (:~>: dom cod f)) => Fact (:⊆: cod cod'_copy -> :~>: dom cod' f) | |
Fact (:⊆: dom cod -> :~>: dom cod (Incl dom cod)) | |
Fact (:∈: (Lower s) fam -> :⊆: (Inters fam) s) | |
Fact (:∈: (Lower s) fam -> :⊆: s (Unions fam)) | |
Fact (:~>: dom cod f -> :⊆: (Image f (Preimage f set)) set) | |
Fact (:~>: dom cod f -> :⊆: set dom -> :⊆: set (Preimage f (Image f set))) | |
Fact (:~>: s t f1 -> :⊆: (Equaliser f1 f2) s) | |
Fact (:~>: dom cod f -> :⊆: cod cod' -> :~>: dom cod' f) | |
Fact (:~>: dom cod f -> :~>: dom cod' f' -> :⊆: f f' -> :==: f f') | |
Fact (:~>: dom cod f -> :⊆: f (:×: dom cod)) | |
(Fact (:⊆: t s1), Fact (:⊆: t s2)) => Fact (:⊆: t (:∩: s1 s2)) | |
Fact (:⊆: s2 (:∪: s1 s2)) | |
Fact (:⊆: s1 (:∪: s1 s2)) | |
Fact (:⊆: s Univ) | |
Fact (:⊆: s s) | |
Fact (:⊆: MonadPlusType MonadType) | |
Fact (:⊆: IntegralType NumType) | |
Fact (:⊆: NumType EqType) | |
Fact (:⊆: OrdType EqType) | |
Fact (:⊆: Empty s) | |
Fact (:⊆: (:∩: s1 s2) s2) | |
Fact (:⊆: (:∩: s1 s2) s1) | |
(Fact (:⊆: s1 t), Fact (:⊆: s2 t)) => Fact (:⊆: (:∪: s1 s2) t) | |
Fact (:∈: a set) => Fact (:⊆: (Singleton a) set) | |
Fact (:⊆: ExampleSet TypeableType) | |
Fact (:⊆: ExampleSet OrdType) | |
Fact (:⊆: ExampleSet EqType) |
Extensional equality of sets
Fact (Ex dom -> :==: (Const dom x) (Const dom' x') -> :=: x x') | |
Fact (:==: s1 s2 -> :==: s2 s3 -> :==: s1 s3) | |
Fact (:==: s1 s2 -> :==: s2 s1) | |
Fact (:==: s1 s2 -> :∈: a s2 -> :∈: a s1) | |
Fact (:==: s1 s2 -> :∈: a s1 -> :∈: a s2) | |
Fact (:~>: dom (:×: cod1 cod2) f -> :==: (:***: (:○: (Fst cod1 cod2) f) (:○: (Snd cod1 cod2) f)) f) | |
Fact (:~>: dom cod1 f1 -> :~>: dom cod2 f2 -> :==: (:○: (Snd cod1 cod2) (:***: f1 f2)) f2) | |
Fact (:~>: dom cod1 f1 -> :~>: dom cod2 f2 -> :==: (:○: (Fst cod1 cod2) (:***: f1 f2)) f1) | |
Fact (:~>: s2 cod g -> :~>: s21 s2 f -> :~>: dom s21 f1 -> :==: (:○: (:○: g f) f1) (:○: g (:○: f f1))) | |
Fact (:~>: total base bun -> :~>: base total f -> :==: (:○: bun f) (Id base) -> Section bun f) | |
Fact (:~>: total base bun -> :~>: base total f -> Section bun f -> :==: (:○: bun f) (Id base)) | |
Fact (:~>: d c f -> :==: (:○: f (Id d)) f) | |
Fact (:~>: d c f -> :==: (:○: (Id c) f) f) | |
Fact (:~>: dom cod f -> :==: (Image f (:∪: s1 s2)) (:∪: (Image f s1) (Image f s2))) | |
Fact (:~>: dom cod f -> :~>: dom2 cod f -> :==: dom dom2) | |
Fact (:~>: d c f' -> :==: f f' -> :∈: (x, y) f -> :∈: (x, y') f' -> :=: y y') | |
Fact (:~>: s0 s g -> :~>: s t f1 -> :==: (:○: f1 g) (:○: f2 g) -> :~>: s0 (Equaliser f1 f2) g) | |
Fact (:~>: dom cod f -> :~>: dom cod' f' -> :⊆: f f' -> :==: f f') | |
Fact (:==: s s) | |
Fact (:==: (Inv (Id dom)) (Id dom)) |
ecoerceFlip :: (s1 :==: s2) -> (a :∈: s2) -> a :∈: s1Source
Coercion using a set equality (flipped)
subsetRefl :: s :⊆: sSource
subsetTrans :: (s1 :⊆: s2) -> (s2 :⊆: s3) -> s1 :⊆: s3Source
setEqTrans :: (s1 :==: s2) -> (s2 :==: s3) -> s1 :==: s3Source
Union, intersection, difference
Binary union
unionIdempotent :: (s :∪: s) :==: sSource
Binary intersection
interIdempotent :: (s :∩: s) :==: sSource
Union of a family
type DependentSum = ΣSource
Intersection of a family
elimInters :: Inters fam a -> (Lower s :∈: fam) -> s aSource
data Complement s whereSource
Complement
Complement :: Not (a :∈: s) -> Complement s a |
Fact (Not (s a, Complement s a)) | |
Fact (Disjoint s t -> :⊆: t (Complement s)) | |
Fact (Disjoint s (Complement s)) |
elimComplement :: (a :∈: Complement s) -> Not (a :∈: s)Source
complContradiction :: Not (s a, Complement s a)Source
complEmpty :: Disjoint s (Complement s)Source
complMaximal :: Disjoint s t -> t :⊆: Complement sSource
Products
Binary products
Fact (:⊆: s1 t1 -> :⊆: s2 t2 -> :⊆: (:×: s1 s2) (:×: t1 t2)) | |
Fact (:∈: (a, b) (:×: s1 s2) -> :∈: b s2) | |
Fact (:∈: (a, b) (:×: s1 s2) -> :∈: a s1) | |
Fact (:~>: dom (:×: cod1 cod2) f -> :==: (:***: (:○: (Fst cod1 cod2) f) (:○: (Snd cod1 cod2) f)) f) | |
Fact (:~>: dom cod f -> :∈: pair f -> :∈: pair (:×: dom cod)) | |
Fact (:~>: dom cod f -> :⊆: f (:×: dom cod)) | |
Fact (:~>: dom cod1 f1 -> :~>: dom cod2 f2 -> :~>: dom (:×: cod1 cod2) (:***: f1 f2)) | |
(Fact (:~>: dom cod1 f1), Fact (:~>: dom cod2 f2)) => Fact (:~>: dom (:×: cod1 cod2) (:***: f1 f2)) | |
Fact (:~>: (:×: s1 s2) s2 (Snd s1 s2)) | |
Fact (:~>: (:×: s1 s2) s1 (Fst s1 s2)) | |
Fact (:~>: (:×: Univ Univ) (KleisliType m) (KleisliHom m)) | |
Fact (:~>: (:×: Univ Univ) FunctionType HaskFun) | |
Fact (:~>: (:×: Univ Univ) Univ (BiGraph f)) |
prodMonotonic :: (s1 :⊆: t1) -> (s2 :⊆: t2) -> (s1 :×: s2) :⊆: (t1 :×: t2)Source
Product is monotonic wrt. subset inclusion
Particular sets
Empty set (barring cheating with undefined
)
emptySubset :: Empty :⊆: sSource
Set of all types of kind *
univSubset :: s :⊆: UnivSource
data FunctionType whereSource
FunctionType :: FunctionType (a -> b) |
Fact (:∈: (a -> b) FunctionType) | |
Fact (:~>: (:×: Univ Univ) FunctionType HaskFun) |
functionType :: (a -> b) :∈: FunctionTypeSource
data KleisliType m whereSource
KleisliType :: KleisliType m (a -> m b) |
Fact (:∈: (a -> m b) (KleisliType m)) | |
Fact (:~>: (:×: Univ Univ) (KleisliType m) (KleisliHom m)) |
kleisliType :: (a -> m b) :∈: KleisliType mSource
data CoKleisliType w whereSource
CoKleisliType :: CoKleisliType w (w a -> b) |
Fact (:∈: (w a -> b) (CoKleisliType w)) |
coKleisliType :: (w a -> b) :∈: CoKleisliType wSource
Sets from common typeclasses
getCompare :: (a :∈: OrdType) -> a -> a -> OrderingSource
data BoundedType whereSource
BoundedType :: Bounded a => BoundedType a |
Bounded a => Fact (:∈: a BoundedType) |
data IntegralType whereSource
IntegralType :: Integral a => IntegralType a |
Fact (:⊆: IntegralType NumType) | |
Integral a => Fact (:∈: a IntegralType) |
data MonoidType whereSource
MonoidType :: Monoid a => MonoidType a |
Monoid a => Fact (:∈: a MonoidType) |
data FractionalType whereSource
FractionalType :: Fractional a => FractionalType a |
Fractional a => Fact (:∈: a FractionalType) |
data TypeableType whereSource
TypeableType :: Typeable a => TypeableType a |
Fact (:⊆: ExampleSet TypeableType) | |
Typeable a => Fact (:∈: a TypeableType) |
Kind (* -> *)
data FunctorType whereSource
FunctorType :: Functor a => FunctorType (Lower a) |
Functor a => Fact (:∈: (Lower a) FunctorType) |
getFmap :: (Lower f :∈: FunctorType) -> (a -> b) -> f a -> f bSource
data MonadPlusType whereSource
MonadPlusType :: MonadPlus a => MonadPlusType (Lower a) |
Fact (:⊆: MonadPlusType MonadType) | |
MonadPlus a => Fact (:∈: (Lower a) MonadPlusType) |
data ApplicativeType whereSource
ApplicativeType :: Applicative a => ApplicativeType (Lower a) |
Applicative a => Fact (:∈: (Lower a) ApplicativeType) |
Powerset
Powerset
powersetWholeset :: u ::∈: Powerset uSource
Misc
autosubset :: Fact (s :⊆: t) => s :⊆: tSource
autoequality :: Fact (s :==: t) => s :==: tSource
Unique existence of sets
Unique existence, unlowered
From sets to the value level
V s
is the sum of all types x
such that s x
is provable.
liftCompare :: (s :⊆: OrdType) -> (s :⊆: TypeableType) -> V s -> V s -> OrderingSource
liftShowsPrec :: Typeable1 s => (s :⊆: ShowType) -> (s :⊆: TypeableType) -> Int -> V s -> ShowSSource