type-settheory-0.1.3.1: Sets and functions-as-relations in the type system

Type.Logic

Description

Propositions as types (of kind `*`), proofs as values

Synopsis

# Documentation

newtype Falsity Source

Constructors

 Falsity FieldselimFalsity :: forall a. a

Instances

 Typeable Falsity Decidable Falsity Typeable a => Show (a -> Falsity) Fact (Falsity -> a)

data Truth Source

Constructors

 TruthProof

Instances

 Show Truth Typeable Truth Decidable Truth Fact Truth

type Not a = a -> FalsitySource

class Fact a whereSource

This class collects lemmas. It plays no foundational role.

Methods

auto :: aSource

Instances

 Fact Truth Fact (p a) => Fact (Ex p) 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 (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))

class Decidable a whereSource

Methods

decide :: Either (Not a) aSource

Instances

 Decidable Truth Decidable Falsity Finite s => Decidable (Ex s) Decidable a => Decidable (Not a) (Decidable a, Decidable b) => Decidable (a -> b) (Decidable a, Decidable b) => Decidable (Either a b) (Decidable a, Decidable b) => Decidable (a, b)

data Ex p whereSource

Existential quantification

Constructors

 Ex :: p b -> Ex p

Instances

 Finite s => Decidable (Ex s) Fact (p a) => Fact (Ex p) Fact (ExUniq p -> Ex p) Fact (Ex dom -> :==: (Const dom x) (Const dom' x') -> :=: x x')

exElim :: forall p r. (forall b. p b -> r) -> Ex p -> rSource

newtype All p Source

Universal quantification

Constructors

 All FieldsallElim :: forall b. p b

Instances

 Fact (All p -> p b)

data ExUniq p whereSource

Unique existence

Constructors

 ExUniq :: p b -> (forall b'. p b' -> b :=: b') -> ExUniq p

Instances

 Fact (ExUniq p -> p b -> p b' -> :=: b b') Fact (ExUniq p -> Ex 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

class Decidable1 s whereSource

Methods

decide1 :: Either (Not (s a)) (s a)Source

class Finite s whereSource

Methods

enum :: [Ex s]Source