Closed bvssvni closed 1 year ago
Currently, it is possible to prove that every function is both monic and epic, due to the axioms:
(f : a -> b) ⋀ (f . inv(f)) => id{b} (f : a -> b) ⋀ id{b} => (f . inv(f)) (f : a -> b) ⋀ (inv(f) . f) => id{a} (f : a -> b) ⋀ id{a} => (inv(f). f)
This should be changed to:
~(f . inv(f)) ⋀ (f : a -> b) ⋀ (f . inv(f)) => id{b} ~((f . inv(f))) ⋀ (f : a -> b) ⋀ id{b} => (f . inv(f)) ~(inv(f) . f) ⋀ (f : a -> b) ⋀ (inv(f) . f) => id{a} ~(inv(f). f) ⋀ (f : a -> b) ⋀ id{a} => (inv(f). f)
Here:
~(f . inv(f))
f
~(inv(f) . f)
Currently, it is possible to prove that every function is both monic and epic, due to the axioms:
This should be changed to:
Here:
~(f . inv(f))
is the same as saying thatf
is epic~(inv(f) . f)
is the same as saying thatf
is monic