Documentation

Constructors

Falsity
Fields elimFalsity :: 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 -> Falsity Source

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
Fields allElim :: 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