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)) |