type-settheory-0.1.2: Type-level sets and functions expressed as typesSource codeContentsIndex
Type.Logic
Description
Propositions as types (of kind *), proofs as values
Synopsis
newtype Falsity = Falsity {
elimFalsity :: forall a. a
}
data Truth = TruthProof
type Not a = a -> Falsity
class Fact a where
auto :: a
data Decidable a = Decidable {
decide :: Either (Not a) a
}
data Ex p where
Ex :: p b -> Ex p
exElim :: forall p r. (forall b. p b -> r) -> Ex p -> r
newtype All p = All {
allElim :: forall b. p b
}
data ExUniq p where
ExUniq :: p b -> (forall b'. p b' -> b :=: b') -> ExUniq p
type COr r a b = Cont r (Either a b)
lem :: COr r (a -> r) a
elimCor :: COr r a b -> (a -> r) -> (b -> r) -> r
Documentation
newtype Falsity Source
Constructors
Falsity
elimFalsity :: forall a. a
show/hide Instances
data Truth Source
Constructors
TruthProof
show/hide Instances
type Not a = a -> FalsitySource
class Fact a whereSource
This class collects lemmas. It plays no foundational role.
Methods
auto :: aSource
show/hide Instances
Fact Truth
Fact (p a) => Fact (Ex p)
Fact (Decidable Truth)
Fact (Decidable Falsity)
Fact (Not ((,) (s a) (Complement s a)))
Fact (Injective (BiGraph f))
Fact (Injective (Graph f))
Fact (Injective (KleisliHom m))
Fact (Injective HaskFun)
Fact (Injective (Incl dom cod))
(Fact (a -> c), Fact (b -> c)) => Fact (Either a b -> c)
Fact ((,) a b -> b)
Fact ((,) a b -> a)
Fact (a -> Not (Not a))
Fact (b -> Either a b)
Fact (a -> Either a b)
Fact (ExUniq p -> p b -> p b' -> b :=: b')
Fact (ExUniq p -> Ex p)
Fact (All p -> p b)
Fact (Ex dom -> (Const dom x :==: Const dom' x') -> x :=: x')
Fact (Decidable a -> Decidable (Not a))
Fact (Decidable a -> Decidable b -> Decidable (a -> b))
Fact (Decidable a -> Decidable b -> Decidable (Either a b))
Fact (Decidable a -> Decidable b -> Decidable ((,) a b))
Fact (Falsity -> a)
Fact (Empty a -> b)
Fact (Disjoint s t -> t :⊆: Complement s)
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 ((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 (((,) a b :∈: (s1 :×: s2)) -> b :∈: s2)
Fact (((,) a b :∈: (s1 :×: s2)) -> a :∈: s1)
Fact ((x :∈: cod) -> (dom :~>: cod) (Const dom x))
Fact ((Lower s :∈: fam) -> Inters fam :⊆: s)
Fact ((Lower s :∈: fam) -> s :⊆: Unions fam)
Fact ((dom :~~>: cod) (Lower f) -> (dom :~>: cod) f)
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 ((dom :~>: cod) f -> Image f (Preimage f set) :⊆: set)
Fact ((dom :~>: cod) f -> (set :⊆: dom) -> set :⊆: Preimage f (Image f set))
Fact ((dom :~>: cod) f -> Injective f -> (Image f dom :~>: dom) (Inv f))
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 ((dom :~>: cod) f -> (dom :~~>: cod) (Lower f))
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 ((dom :~>: cod) f -> ((,) a b :∈: f) -> b :∈: cod)
Fact ((dom :~>: cod) f -> ((,) a b :∈: f) -> a :∈: dom)
Fact ((d :~>: c) f' -> (f :==: f') -> ((,) x y :∈: f) -> ((,) x y' :∈: f') -> y :=: y')
Fact ((s :~>: t) f1 -> (Equaliser f1 f2 :~>: s) (EqualiserIncl s f1 f2))
Fact ((s0 :~>: s) g -> (s :~>: t) f1 -> ((f1 :○: g) :==: (f2 :○: g)) -> (s0 :~>: Equaliser f1 f2) g)
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 -> (a :∈: dom) -> ExSnd f a)
Fact ((dom :~>: cod) f -> (pair :∈: f) -> pair :∈: (dom :×: cod))
Fact ((dom :~>: cod) f -> f :⊆: (dom :×: cod))
Fact ((dom :~>: cod) f -> ((,) a b1 :∈: f) -> ((,) a b2 :∈: f) -> b1 :=: b2)
Fact ((s2 :~>: s3) g -> (s1 :~>: s2) f -> (s1 :~>: s3) (g :○: f))
Fact ((dom :~>: cod1) f1 -> (dom :~>: cod2) f2 -> (dom :~>: (cod1 :×: cod2)) (f1 :***: f2))
(Fact a, Fact b) => Fact ((,) a b)
Fact (Disjoint s (Complement s))
Fact (Singleton a a)
Fact (s :==: s)
Fact (Inv (Id dom) :==: Id dom)
(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)
Fact ((w a -> b) :∈: CoKleisliType w)
Fact ((a -> m b) :∈: KleisliType m)
Fact ((a -> b) :∈: FunctionType)
(a ~ a_copy, b ~ b_copy) => Fact ((,) ((,) a_copy b_copy) (f a b) :∈: BiGraph f)
(a1 ~ a, b1 ~ b, m1 ~ m) => Fact ((,) ((,) a1 b1) (a -> m1 b) :∈: KleisliHom m)
(a_copy ~ a, b_copy ~ b) => Fact ((,) ((,) a_copy b_copy) (a -> b) :∈: HaskFun)
a ~ a_copy => Fact ((,) a_copy (f a) :∈: Graph f)
Data a => Fact (a :∈: DataType)
Typeable a => Fact (a :∈: TypeableType)
Fractional a => Fact (a :∈: FractionalType)
Monoid a => Fact (a :∈: MonoidType)
Integral a => Fact (a :∈: IntegralType)
Num a => Fact (a :∈: NumType)
Bounded a => Fact (a :∈: BoundedType)
Enum a => Fact (a :∈: EnumType)
Ord a => Fact (a :∈: OrdType)
Eq a => Fact (a :∈: EqType)
Read a => Fact (a :∈: ReadType)
Show a => Fact (a :∈: ShowType)
Applicative a => Fact (Lower a :∈: ApplicativeType)
MonadPlus a => Fact (Lower a :∈: MonadPlusType)
Monad a => Fact (Lower a :∈: MonadType)
Functor a => Fact (Lower a :∈: FunctorType)
(Lower f ~ lf, Fact ((dom :~>: cod) f)) => Fact ((dom :~~>: cod) lf)
(Fact ((dom :~>: cod1) f1), Fact ((dom :~>: cod2) f2)) => Fact ((dom :~>: (cod1 :×: cod2)) (f1 :***: f2))
(Fact ((s2 :~>: s3) g), Fact ((s1 :~>: s2) f)) => Fact ((s1 :~>: s3) (g :○: f))
Fact (dom :⊆: cod) => Fact ((dom :~>: cod) (Incl dom cod))
Fact ((dom :~>: dom) (Id dom))
Fact ((Univ :~>: Univ) (Graph f))
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))
data Decidable a Source
Constructors
Decidable
decide :: Either (Not a) a
show/hide Instances
data Ex p whereSource
Existential quantification
Constructors
Ex :: p b -> Ex p
show/hide Instances
Fact (p a) => Fact (Ex p)
exElim :: forall p r. (forall b. p b -> r) -> Ex p -> rSource
newtype All p Source
Universal quantification
Constructors
All
allElim :: forall b. p b
data ExUniq p whereSource
Unique existence
Constructors
ExUniq :: p b -> (forall b'. p b' -> b :=: b') -> ExUniq p
type COr r a b = Cont r (Either a b)Source
lem :: COr r (a -> r) aSource
elimCor :: COr r a b -> (a -> r) -> (b -> r) -> rSource
Produced by Haddock version 2.4.2