Proper handling of epic and monic functions

Closes #1734

Author: bvssvni

src/fun/comp.rs

@@ -84,6 +84,42 @@ pub fn comp_eq_right<F: Prop, G: Prop, H: Prop>(x: Eq<G, H>) -> Eq<Comp<F, G>, C
     (Rc::new(move |fg| comp_in_right_arg(fg, x.clone())),
      Rc::new(move |fh| comp_in_right_arg(fh, x2.clone())))
 }
+/// `~(f . inv(f)) ⋀ ((g . f) == (h . f)) ⋀ (f : a -> x) ⋀ (g : x -> y) ⋀ (h : x -> y)  =>  g == h`.
+pub fn epic<F: Prop, G: Prop, H: Prop, X: Prop, Y: Prop, A: Prop>(
+    qu_comp_f_inv_f: Qu<Comp<F, Inv<F>>>,
+    x: Eq<Comp<G, F>, Comp<H, F>>,
+    ty_f: Ty<F, Pow<X, A>>,
+    ty_g: Ty<G, Pow<Y, X>>,
+    ty_h: Ty<H, Pow<Y, X>>,
+) -> Eq<G, H> {
+    let x: Eq<Comp<Comp<G, F>, Inv<F>>, Comp<Comp<H, F>, Inv<F>>> = comp_eq_left(x);
+    let x: Eq<Comp<G, Comp<F, Inv<F>>>, _> = eq::in_left_arg(x, eq::symmetry(comp_assoc()));
+    let x: Eq<_, Comp<H, Comp<F, Inv<F>>>> = eq::in_right_arg(x, eq::symmetry(comp_assoc()));
+    let y: Eq<Comp<F, Inv<F>>, Id<X>> = eq_comp_right_inv_id(qu_comp_f_inv_f, ty_f);
+    let x: Eq<Comp<G, Id<X>>, _> = eq::in_left_arg(x, comp_eq_right(y.clone()));
+    let x: Eq<_, Comp<H, Id<X>>> = eq::in_right_arg(x, comp_eq_right(y));
+    let x: Eq<G, _> = eq::in_left_arg(x, comp_id_right(ty_g));
+    let x: Eq<_, H> = eq::in_right_arg(x, comp_id_right(ty_h));
+    x
+}
+/// `~(inv(f) . f) ⋀ ((f . g) == (f . h)) ⋀ (f : x -> y) ⋀ (g : a -> x) ⋀ (h : a -> x)  =>  g == h`.
+pub fn monic<F: Prop, G: Prop, H: Prop, X: Prop, Y: Prop, A: Prop>(
+    qu_comp_inv_f_f: Qu<Comp<Inv<F>, F>>,
+    x: Eq<Comp<F, G>, Comp<F, H>>,
+    ty_f: Ty<F, Pow<Y, X>>,
+    ty_g: Ty<G, Pow<X, A>>,
+    ty_h: Ty<H, Pow<X, A>>,
+) -> Eq<G, H> {
+    let x: Eq<Comp<Inv<F>, Comp<F, G>>, Comp<Inv<F>, Comp<F, H>>> = comp_eq_right(x);
+    let x: Eq<Comp<Comp<Inv<F>, F>, G>, _> = eq::in_left_arg(x, comp_assoc());
+    let x: Eq<_, Comp<Comp<Inv<F>, F>, H>> = eq::in_right_arg(x, comp_assoc());
+    let y: Eq<Comp<Inv<F>, F>, Id<X>> = eq_comp_left_inv_id(qu_comp_inv_f_f, ty_f);
+    let x: Eq<Comp<Id<X>, G>, _> = eq::in_left_arg(x, comp_eq_left(y.clone()));
+    let x: Eq<_, Comp<Id<X>, H>> = eq::in_right_arg(x, comp_eq_left(y));
+    let x: Eq<G, _> = eq::in_left_arg(x, comp_id_left(ty_g));
+    let x: Eq<_, H> = eq::in_right_arg(x, comp_id_left(ty_h));
+    x
+}
 /// `(f(a) == b) ⋀ (g(b) == c)  =>  g(f(a)) == c`.
 pub fn comp_app<F: Prop, G: Prop, A: Prop, B: Prop, C: Prop>(
     x: Eq<App<F, A>, B>,

src/fun/id.rs

@@ -46,23 +46,27 @@ pub fn id_def<A: Prop, X: Prop, N: Nat>(
 ) -> Eq<App<Id<X>, A>, A> {unimplemented!()}
 /// `inv(id{x}) == id{x}`.
 pub fn id_inv<X: Prop>() -> Eq<Inv<App<FId, X>>, App<FId, X>> {unimplemented!()}
-/// `(f : a -> b) ⋀ (f . inv(f))  =>  id{b}`.
+/// `~(f . inv(f)) ⋀ (f : a -> b) ⋀ (f . inv(f))  =>  id{b}`.
 pub fn comp_right_inv_to_id<F: Prop, A: Prop, B: Prop>(
+    _: Qu<Comp<F, Inv<F>>>,
     _: Ty<F, Pow<B, A>>,
     _: Comp<F, Inv<F>>
 ) -> App<FId, B> {unimplemented!()}
-/// `(f : a -> b) ⋀ id{b} => (f . inv(f))`.
+/// `~(f . inv(f)) ⋀ (f : a -> b) ⋀ id{b}  =>  (f . inv(f))`.
 pub fn id_to_comp_right_inv<F: Prop, A: Prop, B: Prop>(
+    _: Qu<Comp<F, Inv<F>>>,
     _: Ty<F, Pow<B, A>>,
     _: App<FId, B>
 ) -> Comp<F, Inv<F>> {unimplemented!()}
-/// `(f : a -> b) ⋀ (inv(f) . f) => id{a}`.
+/// `~(inv(f) . f) ⋀ (f : a -> b) ⋀ (inv(f) . f)  =>  id{a}`.
 pub fn comp_left_inv_to_id<F: Prop, A: Prop, B: Prop>(
+    _: Qu<Comp<Inv<F>, F>>,
     _: Ty<F, Pow<B, A>>,
     _: Comp<Inv<F>, F>
 ) -> App<FId, A> {unimplemented!()}
-/// `(f : a -> b) ⋀ id{a} => (inv(f). f)`.
+/// `~(inv(f) . f) ⋀ (f : a -> b) ⋀ id{a}  =>  (inv(f). f)`.
 pub fn id_to_comp_left_inv<F: Prop, A: Prop, B: Prop>(
+    _: Qu<Comp<Inv<F>, F>>,
     _: Ty<F, Pow<B, A>>,
     _: App<FId, A>
 ) -> Comp<Inv<F>, F> {unimplemented!()}
@@ -93,12 +97,18 @@ pub fn self_inv_to_eq_id<F: Prop, A: Prop>(
     ty_f: Ty<F, Pow<A, A>>,
     eq_f: Eq<Inv<F>, F>
 ) -> Eq<Comp<F, F>, App<FId, A>> {
+    let x = inv::self_inv_to_q(eq_f.clone());
+    let qu_f = qubit::Qubit::from_q(quality::right(x.clone()));
+    let qu_inv_f = qubit::Qubit::from_q(quality::left(x));
+    let qu_comp_f_inv_f = comp::comp_qu(qu_inv_f, qu_f);
+    let qu_comp_f_inv_f_2 = qu_comp_f_inv_f.clone();
     let ty_f_2 = ty_f.clone();
     let eq_f_2 = eq_f.clone();
     (
-        Rc::new(move |x| comp_right_inv_to_id(ty_f_2.clone(),
+        Rc::new(move |x| comp_right_inv_to_id(qu_comp_f_inv_f.clone(), ty_f_2.clone(),
             comp_in_right_arg(x, eq::symmetry(eq_f_2.clone())))),
-        Rc::new(move |x| comp_in_right_arg(id_to_comp_right_inv(ty_f.clone(), x), eq_f.clone())),
+        Rc::new(move |x| comp_in_right_arg(id_to_comp_right_inv(qu_comp_f_inv_f_2.clone(),
+            ty_f.clone(), x), eq_f.clone())),
     )
 }
 /// `inv(id{a}) ~~ id{a}`.
@@ -173,19 +183,23 @@ pub fn para_to_eq_qu<A: Prop>(para_a: Para<A>) -> Eq<Qu<A>, A> {
 pub fn pow_to_eq_qu<A: Prop, B: Prop>(x: Pow<A, B>) -> Eq<Qu<Pow<A, B>>, Pow<A, B>> {
     tauto_to_eq_qu(x.lift())
 }
-/// `(f : a -> b)  =>  (inv(f) . f) == id{a}`.
+/// `~(inv(f) . f) ⋀ (f : a -> b)  =>  (inv(f) . f) == id{a}`.
 pub fn eq_comp_left_inv_id<F: Prop, A: Prop, B: Prop>(
+    qu_comp_inv_f_f: Qu<Comp<Inv<F>, F>>,
     ty_f: Ty<F, Pow<B, A>>
 ) -> Eq<Comp<Inv<F>, F>, Id<A>> {
     let ty_f2 = ty_f.clone();
-    (Rc::new(move |x| comp_left_inv_to_id(ty_f.clone(), x)),
-     Rc::new(move |x| id_to_comp_left_inv(ty_f2.clone(), x)))
+    let qu_comp_inv_f_f_2 = qu_comp_inv_f_f.clone();
+    (Rc::new(move |x| comp_left_inv_to_id(qu_comp_inv_f_f.clone(), ty_f.clone(), x)),
+     Rc::new(move |x| id_to_comp_left_inv(qu_comp_inv_f_f_2.clone(), ty_f2.clone(), x)))
 }
-/// `(f : a -> b)  =>  (f . inv(f)) == id{b}`.
+/// `~(f . inv(f)) ⋀ (f : a -> b)  =>  (f . inv(f)) == id{b}`.
 pub fn eq_comp_right_inv_id<F: Prop, A: Prop, B: Prop>(
+    qu_comp_f_inv_f: Qu<Comp<F, Inv<F>>>,
     ty_f: Ty<F, Pow<B, A>>
 ) -> Eq<Comp<F, Inv<F>>, Id<B>> {
     let ty_f2 = ty_f.clone();
-    (Rc::new(move |x| comp_right_inv_to_id(ty_f.clone(), x)),
-     Rc::new(move |x| id_to_comp_right_inv(ty_f2.clone(), x)))
+    let qu_comp_f_inv_f_2 = qu_comp_f_inv_f.clone();
+    (Rc::new(move |x| comp_right_inv_to_id(qu_comp_f_inv_f.clone(), ty_f.clone(), x)),
+     Rc::new(move |x| id_to_comp_right_inv(qu_comp_f_inv_f_2.clone(), ty_f2.clone(), x)))
 }