use crate::*;
use path_semantics::{POrdProof, Ty};
use quality::Q;
use qubit::Qu;
use hooo::{Pow, Tauto};
use hooo::pow::PowExt;
use nat::{Nat, S, Z};
pub mod bool_alg;
pub mod hott;
pub mod real;
pub mod eqx;
pub fn and_is_const<A: Prop, B: Prop>(_a: IsConst<A>, _b: IsConst<B>) -> IsConst<And<A, B>> {
unimplemented!()
}
pub fn or_is_const<A: Prop, B: Prop>(_a: IsConst<A>, _b: IsConst<B>) -> IsConst<Or<A, B>> {
unimplemented!()
}
pub fn imply_is_const<A: Prop, B: Prop>(_a: IsConst<A>, _b: IsConst<B>) -> IsConst<Imply<A, B>> {
unimplemented!()
}
pub fn pord_is_const<A: Prop, B: Prop>(
_a: IsConst<A>,
_b: IsConst<B>
) -> IsConst<POrdProof<A, B>> {
unimplemented!()
}
pub fn ty_is_const<A: Prop, B: Prop>(a: IsConst<A>, b: IsConst<B>) -> IsConst<Ty<A, B>> {
and_is_const(imply_is_const(a.clone(), b.clone()), pord_is_const(a, b))
}
pub fn qu_tauto_eq_to_q<F: Prop, G: Prop>(x: Qu<F>, tauto_eq: Tauto<Eq<F, G>>) -> Q<F, G> {
(tauto_eq(True), (x.clone(), hooo::qu_in_arg(x, tauto_eq)))
}
pub fn qu_double<F: Prop>(x: Qu<F>) -> Qu<Inv<Inv<F>>> {
qu_tauto_eq_to_q(x, hooo::pow_eq_to_tauto_eq((involve_inv, inv_involve))).1.1
}
pub fn qu_rev_double<F: Prop>(x: Qu<Inv<Inv<F>>>) -> Qu<F> {
qu_tauto_eq_to_q(x, hooo::pow_eq_to_tauto_eq((inv_involve, involve_inv))).1.1
}
pub fn qu_inv_tauto_eq_to_qu_inv<F: Prop, G: Prop>(
x: Qu<Inv<F>>,
tauto_eq: Tauto<Eq<F, G>>
) -> Qu<Inv<G>> {qu_tauto_eq_to_q(x, hooo::pow_transitivity(tauto_eq, inv_eq)).1.1}
pub fn inv_double_val<F: Prop, X: Prop>() -> Eq<App<Inv<Inv<F>>, X>, App<F, X>> {
app_map_eq(involve_eq())
}
pub fn q_inv<F: Prop, G: Prop>((eq_fg, (qu_f, qu_g)): Q<F, G>) -> Q<Inv<F>, Inv<G>> {
(inv_eq(eq_fg), (inv_qu(qu_f), inv_qu(qu_g)))
}
pub fn q_adjoint_left<F: Prop, G: Prop>(x: Q<Inv<F>, G>) -> Q<F, Inv<G>> {
hooo::q_in_left_arg(q_inv(x), hooo::pow_eq_to_tauto_eq((inv_involve, involve_inv)))
}
pub fn q_adjoint_right<F: Prop, G: Prop>(x: Q<F, Inv<G>>) -> Q<Inv<F>, G> {
quality::symmetry(q_adjoint_left(quality::symmetry(x)))
}
pub fn q_adjoint<F: Prop, G: Prop>() -> Eq<Q<Inv<F>, G>, Q<F, Inv<G>>> {
hooo::pow_eq_to_tauto_eq((q_adjoint_left, q_adjoint_right))(True)
}
pub fn qu_to_app_eq<A: Prop, B: Prop, F: Prop>(
x: Qu<Inv<F>>
) -> Eq<Eq<App<F, A>, B>, Eq<App<Inv<F>, B>, A>> {
let qu_inv_inv_f: Qu<Inv<Inv<F>>> = inv_qu(x.clone());
(Rc::new(move |y| inv_val_qu(x.clone(), y)),
Rc::new(move |y|
eq::in_left_arg(inv_val_qu(qu_inv_inv_f.clone(), y), app_map_eq(involve_eq()))))
}
pub type App2<F, X, Y> = App<App<F, X>, Y>;
#[derive(Copy, Clone)]
pub struct App<F, X>(F, X);
pub fn app_is_const<F: Prop, X: Prop>(_f: IsConst<F>, _x: IsConst<X>) -> IsConst<App<F, X>> {
unimplemented!()
}
pub fn app_eq<F: Prop, X: Prop, Y: Prop>(
_eq_xy: Eq<X, Y>
) -> Eq<App<F, X>, App<F, Y>> {unimplemented!()}
pub fn app_map_eq<F: Prop, G: Prop, X: Prop>(
_eq_fg: Eq<F, G>
) -> Eq<App<F, X>, App<G, X>> {unimplemented!()}
pub fn app_rev_fun_ty<F: Prop, X: Prop, Y: Prop, A: Prop>(
_: Pow<Ty<App<F, A>, Y>, Ty<A, X>>
) -> Ty<F, Pow<Y, X>> {unimplemented!()}
pub fn app_lam_ty<F: Prop, X: Prop, Y: Prop, A: Prop>(
_ty_f: Ty<F, Imply<X, Y>>,
_ty_a: Ty<A, X>,
) -> Ty<App<F, A>, Y> {unimplemented!()}
pub fn app_rev_lam_ty<F: Prop, X: Prop, Y: Prop, A: Prop>(
_ty_a: Ty<A, X>,
_ty_fa: Imply<Ty<A, X>, Ty<App<F, A>, Y>>
) -> Ty<F, Imply<Y, X>> {unimplemented!()}
pub fn app_fun_ty<F: Prop, X: Prop, Y: Prop, A: Prop>(
ty_f: Ty<F, Pow<Y, X>>,
ty_a: Ty<A, X>,
) -> Ty<App<F, A>, Y> {app_lam_ty(fun_to_lam_ty(ty_f), ty_a)}
pub fn app2_fun_ty<F: Prop, X: Prop, Y: Prop, Z: Prop, A: Prop, B: Prop>(
ty_f: Ty<F, Pow<Pow<Z, Y>, X>>,
ty_a: Ty<A, X>,
ty_b: Ty<B, Y>,
) -> Ty<App2<F, A, B>, Z> {
app_fun_ty(app_fun_ty(ty_f, ty_a), ty_b)
}
pub fn app2_lam_ty<F: Prop, X: Prop, Y: Prop, Z: Prop, A: Prop, B: Prop>(
ty_f: Ty<F, Imply<X, Imply<Y, Z>>>,
ty_a: Ty<A, X>,
ty_b: Ty<B, Y>,
) -> Ty<App2<F, A, B>, Z> {
app_lam_ty(app_lam_ty(ty_f, ty_a), ty_b)
}
pub fn app_lift_ty_lam<F: Prop, A: Prop, B: Prop, X: Prop, Y: Prop>(
x: Eq<App<F, A>, B>,
ty_a: Ty<A, X>,
ty_b: Ty<B, Y>,
) -> Ty<Lam<Ty<A, X>, App<F, A>>, Imply<X, Y>> {
lam_ty(ty_a, path_semantics::ty_in_left_arg(ty_b, eq::symmetry(x)))
}
pub fn fun_to_lam_ty<F: Prop, X: Prop, Y: Prop>(ty_f: Ty<F, Pow<Y, X>>) -> Ty<F, Imply<X, Y>> {
let x = hooo::pow_to_imply(hooo::pow_to_imply);
(imply::transitivity(ty_f.0, x.clone()), ty_f.1.by_imply_right(x))
}
pub fn app_fun_unfold<F: Prop, A: Prop, X: Prop, Y: Prop>(
ty_f: Tauto<Ty<Pow<App<F, A>, A>, Pow<Y, X>>>,
) -> Ty<F, Pow<Y, X>> {app_rev_fun_ty(hooo::tauto_hooo_rev_ty(ty_f))}
pub fn tauto_lam_to_tauto_fun_ty<F: Prop, X: Prop, Y: Prop>(
ty_f: Tauto<Ty<F, Imply<X, Y>>>
) -> Ty<Tauto<F>, Pow<Y, X>> {
use hooo::{tauto_imply_to_imply_tauto_pow, tauto_imply_to_pow, hooo_pord, pow_to_imply};
(tauto_imply_to_imply_tauto_pow(ty_f.trans(and::fst)),
hooo_pord(ty_f.trans(and::snd)).by_imply_right(pow_to_imply(tauto_imply_to_pow)))
}
pub fn app_tauto_lam_to_tauto_fun_ty<F: Prop, X: Prop, Y: Prop, A: Prop>(
ty_f: Tauto<Ty<Pow<App<F, A>, A>, Imply<X, Y>>>
) -> Ty<F, Pow<Y, X>> {
use hooo::pow_lift;
let x = hooo::pow_tauto_to_pow_tauto_tauto(tauto_lam_to_tauto_fun_ty)(ty_f);
let y = tauto!(path_semantics::ty_eq_left((Rc::new(|x: Tauto<_>| x(True)), Rc::new(pow_lift))));
let x = hooo::tauto_in_arg(x, y);
app_fun_unfold(x)
}
pub fn app_fun_swap_ty<F: Prop, X: Prop, Y: Prop, A: Prop, B: Prop>(
x: Pow<Ty<App<F, A>, Y>, Ty<A, X>>
) -> Pow<Ty<App<F, B>, Y>, Ty<B, X>> {
fn f<F: Prop, X: Prop, Y: Prop, A: Prop, B: Prop>(ty_b: Ty<B, X>) ->
Imply<Pow<Ty<App<F, A>, Y>, Ty<A, X>>, Ty<App<F, B>, Y>>
{Rc::new(move |x| app_fun_ty(app_rev_fun_ty(x), ty_b.clone()))}
hooo::hooo_imply(f)(hooo::pow_lift(x))
}
pub fn app_fun_swap_tauto_ty<F: Prop, Y: Prop, A: Prop, B: Prop>() ->
Eq<Tauto<Ty<App<F, A>, Y>>, Tauto<Ty<App<F, B>, Y>>>
{
use hooo::tr;
use path_semantics::{ty_rev_true, ty_inhabit};
let x: Tauto<True> = hooo::pow_refl;
let ty_a = x.trans(ty_rev_true).trans(ty_inhabit);
let ty_b = x.trans(ty_rev_true).trans(ty_inhabit);
let (y1, y2) = (Rc::new(app_fun_swap_ty), Rc::new(app_fun_swap_ty));
(Rc::new(move |x| ty_b.trans(y1(tr().trans(x)))),
Rc::new(move |x| ty_a.trans(y2(tr().trans(x)))))
}
#[derive(Copy, Clone)]
pub struct Inv<F>(F);
pub fn inv_ty<F: Prop, X: Prop, Y: Prop>(
_ty_f: Ty<F, Pow<Y, X>>
) -> Ty<Inv<F>, Pow<X, Y>> {unimplemented!()}
pub fn inv_is_const<F: Prop>(_a: IsConst<F>) -> IsConst<Inv<F>> {unimplemented!()}
pub fn inv_val_qu<F: Prop, A: Prop, B: Prop>(
_: Qu<Inv<F>>,
_: Eq<App<F, A>, B>
) -> Eq<App<Inv<F>, B>, A> {unimplemented!()}
pub fn inv_involve<F: Prop>(_: Inv<Inv<F>>) -> F {unimplemented!()}
pub fn involve_inv<F: Prop>(_: F) -> Inv<Inv<F>> {unimplemented!()}
pub fn inv_eq<F: Prop, G: Prop>(_: Eq<F, G>) -> Eq<Inv<F>, Inv<G>> {unimplemented!()}
pub fn inv_qu<F: Prop>(_: Qu<F>) -> Qu<Inv<F>> {unimplemented!()}
pub fn path<F: Prop, X: Prop, Y: Prop>(
_: Qu<Inv<F>>,
_: Ty<F, Pow<Y, X>>,
_: Pow<Y, X>
) -> And<F, Inv<F>> {unimplemented!()}
pub fn inv_val<F: Prop, G: Prop, A: Prop, B: Prop>(
x: Q<Inv<F>, G>,
y: Eq<App<F, A>, B>
) -> Eq<App<Inv<F>, B>, A> {inv_val_qu(Qu::<Inv<F>>::from_q(quality::left(x)), y)}
pub fn inv_val_other<F: Prop, G: Prop, A: Prop, B: Prop>(
x: Q<Inv<F>, G>,
y: Eq<App<F, A>, B>
) -> Eq<App<G, B>, A> {
eq::in_left_arg(inv_val(x.clone(), y), app_map_eq(quality::to_eq(x)))
}
pub fn involve_eq<F: Prop>() -> Eq<Inv<Inv<F>>, F> {
hooo::pow_eq_to_tauto_eq((inv_involve, involve_inv))(True)
}
pub fn path_inv<F: Prop, X: Prop, Y: Prop>(
qu_inv_f: Qu<Inv<F>>,
ty_f: Ty<F, Pow<Y, X>>,
x: Pow<Y, X>
) -> Pow<X, Y> {
use path_semantics::{ty_triv, ty_true};
ty_true(ty_triv(inv_ty(ty_f.clone()), path(qu_inv_f, ty_f, x).1))
}
#[derive(Copy, Clone)]
pub struct Comp<F, G>(F, G);
pub fn comp_ty<F: Prop, G: Prop, X: Prop, Y: Prop, Z: Prop>(
_ty_f: Ty<F, Pow<Y, X>>,
_ty_g: Ty<G, Pow<Z, Y>>
) -> Ty<Comp<G, F>, Pow<Z, X>> {unimplemented!()}
pub fn comp_is_const<F: Prop, G: Prop>(_a: IsConst<F>, _b: IsConst<G>) -> IsConst<Comp<G, F>> {
unimplemented!()
}
pub fn inv_comp_to_comp_inv<F: Prop, G: Prop>(_: Inv<Comp<G, F>>) -> Comp<Inv<F>, Inv<G>> {
unimplemented!()
}
pub fn comp_inv_to_inv_comp<F: Prop, G: Prop>(_: Comp<Inv<F>, Inv<G>>) -> Inv<Comp<G, F>> {
unimplemented!()
}
pub fn app_to_comp<F: Prop, G: Prop, X: Prop>(_: App<G, App<F, X>>) -> App<Comp<G, F>, X> {
unimplemented!()
}
pub fn comp_to_app<F: Prop, G: Prop, X: Prop>(_: App<Comp<G, F>, X>) -> App<G, App<F, X>> {
unimplemented!()
}
pub fn comp_assoc<F: Prop, G: Prop, H: Prop>() -> Eq<Comp<H, Comp<G, F>>, Comp<Comp<H, G>, F>> {
unimplemented!()
}
pub fn comp_id_left<F: Prop>() -> Eq<Comp<FId, F>, F> {unimplemented!()}
pub fn comp_id_right<F: Prop>() -> Eq<Comp<F, FId>, F> {unimplemented!()}
pub fn comp_inv<F: Prop, G: Prop>() -> Eq<Comp<Inv<F>, Inv<G>>, Inv<Comp<G, F>>> {
(hooo::pow_to_imply(comp_inv_to_inv_comp), hooo::pow_to_imply(inv_comp_to_comp_inv))
}
pub fn eq_app_comp<F: Prop, G: Prop, X: Prop>() -> Eq<App<G, App<F, X>>, App<Comp<G, F>, X>> {
(Rc::new(move |x| app_to_comp(x)), Rc::new(move |x| comp_to_app(x)))
}
pub fn comp_in_left_arg<F: Prop, G: Prop, H: Prop>(x: Comp<G, F>, y: Eq<G, H>) -> Comp<H, F> {
Comp(y.0(x.0), x.1)
}
pub fn comp_in_right_arg<F: Prop, G: Prop, H: Prop>(x: Comp<G, F>, y: Eq<F, H>) -> Comp<G, H> {
Comp(x.0, y.0(x.1))
}
pub fn comp_eq_left<F: Prop, G: Prop, H: Prop>(x: Eq<F, H>) -> Eq<Comp<F, G>, Comp<H, G>> {
let x2 = eq::symmetry(x.clone());
(Rc::new(move |fg| comp_in_left_arg(fg, x.clone())),
Rc::new(move |hg| comp_in_left_arg(hg, x2.clone())))
}
pub fn comp_eq_right<F: Prop, G: Prop, H: Prop>(x: Eq<G, H>) -> Eq<Comp<F, G>, Comp<F, H>> {
let x2 = eq::symmetry(x.clone());
(Rc::new(move |fg| comp_in_right_arg(fg, x.clone())),
Rc::new(move |fh| comp_in_right_arg(fh, x2.clone())))
}
#[derive(Clone, Copy)]
pub struct Dup(());
pub fn dup_ty<A: Prop>() -> Ty<Dup, Pow<Tup<A, A>, A>> {unimplemented!()}
pub fn dup_is_const() -> IsConst<Dup> {unimplemented!()}
pub fn dup_def<A: Prop>() -> Eq<App<Dup, A>, Tup<A, A>> {unimplemented!()}
#[derive(Clone, Copy)]
pub struct FId(());
pub fn id_ty<A: Prop>() -> Ty<FId, Pow<A, A>> {unimplemented!()}
pub fn id_is_const() -> IsConst<FId> {unimplemented!()}
pub fn id_def<A: Prop>() -> Eq<App<FId, A>, A> {unimplemented!()}
pub fn id_q() -> Q<Inv<FId>, FId> {unimplemented!()}
pub fn comp_right_inv_to_id<F: Prop>(_: Comp<F, Inv<F>>) -> FId {unimplemented!()}
pub fn id_to_comp_right_inv<F: Prop>(_: FId) -> Comp<F, Inv<F>> {unimplemented!()}
pub fn comp_left_inv_to_id<F: Prop>(_: Comp<Inv<F>, F>) -> FId {unimplemented!()}
pub fn id_to_comp_left_inv<F: Prop>(_: FId) -> Comp<Inv<F>, F> {unimplemented!()}
pub fn self_inv_ty<F: Prop, A: Prop, B: Prop>(
ty_f: Ty<F, Pow<B, A>>
) -> Ty<Q<F, Inv<F>>, Q<Pow<B, A>, Pow<A, B>>> {
path_semantics::ty_q_formation(ty_f.clone(), inv_ty(ty_f))
}
pub fn self_inv_to_eq_id<F: Prop>(eq_f: Eq<Inv<F>, F>) -> Eq<Comp<F, F>, FId> {
let eq_f_2 = eq_f.clone();
(
Rc::new(move |x| comp_right_inv_to_id(
comp_in_right_arg(x, eq::symmetry(eq_f_2.clone())))),
Rc::new(move |x| comp_in_right_arg(id_to_comp_right_inv(x), eq_f.clone())),
)
}
#[derive(Copy, Clone)]
pub struct Type<N>(N);
impl<N: 'static + Clone> path_semantics::LProp for Type<N> {
type N = N;
type SetLevel<T: 'static + Clone> = Type<T>;
}
pub fn type_imply<N: Nat>(Type(n): Type<N>) -> Type<S<N>> {Type(S(n))}
pub fn type_is_const<N: Nat>() -> IsConst<Type<N>> {unimplemented!()}
pub fn fun_ty<A: Prop, B: Prop, X: Prop, Y: Prop>(
_: Ty<A, X>,
_: Ty<B, Y>
) -> Ty<Pow<B, A>, Pow<Y, X>> {unimplemented!()}
pub fn fun_type_ty<N: Nat, M: Nat>() -> Ty<Pow<Type<M>, Type<N>>, Type<Z>> {unimplemented!()}
pub fn judgement_ty<A: Prop, B: Prop, N: Nat>(_ty_b: Ty<B, Type<N>>) -> Ty<Ty<A, B>, Type<N>> {
unimplemented!()
}
pub fn type_ty<N: Nat>() -> Ty<Type<N>, Type<S<N>>> {
(hooo::pow_to_imply(type_imply), POrdProof::new())
}
pub fn fun_type0<A: Prop, B: Prop, N: Nat, M: Nat>(
ty_a: Ty<A, Type<N>>,
ty_b: Ty<B, Type<M>>
) -> Ty<Pow<B, A>, Type<Z>> {path_semantics::ty_transitivity(fun_ty(ty_a, ty_b), fun_type_ty())}
pub fn q_inv_ty<F: Prop, G: Prop, A: Prop, B: Prop>(
ty_f: Ty<F, Pow<B, A>>,
q: Q<Inv<F>, G>,
) -> Ty<Q<F, G>, Q<Pow<B, A>, Pow<A, B>>> {
use quality::transitivity as trans;
let y = self_inv_ty(ty_f);
let q2 = q.clone();
let x: Eq<Q<F, Inv<F>>, Q<F, G>> = (
Rc::new(move |x| trans(x, q2.clone())),
Rc::new(move |x| trans(x, quality::symmetry(q.clone())))
);
path_semantics::ty_in_left_arg(y, x)
}
#[derive(Copy, Clone)]
pub struct Tup<A, B>(A, B);
pub fn tup_type_ty<N: Nat, M: Nat>() -> Ty<Tup<Type<N>, Type<M>>, Type<Z>> {
unimplemented!()
}
pub fn tup_ty<A: Prop, B: Prop, X: Prop, Y: Prop>(
_ty_a: Ty<A, X>,
_ty_b: Ty<B, Y>
) -> Ty<Tup<A, B>, Tup<X, Y>> {unimplemented!()}
pub fn tup_is_const<A: Prop, B: Prop>(_a: IsConst<A>, _b: IsConst<B>) -> IsConst<Tup<A, B>> {
unimplemented!()
}
pub fn tup_fst_const<A: Prop, B: Prop>(_: IsConst<Tup<A, B>>) -> IsConst<A> {unimplemented!()}
pub fn tup_snd_const<A: Prop, B: Prop>(_: IsConst<Tup<A, B>>) -> IsConst<B> {unimplemented!()}
pub fn tup_eq_fst<A: Prop, B: Prop, C: Prop>((ab, ba): Eq<A, B>) -> Eq<Tup<A, C>, Tup<B, C>> {
(Rc::new(move |y| Tup(ab(y.0), y.1)), Rc::new(move |y| Tup(ba(y.0), y.1)))
}
pub fn tup_eq_snd<A: Prop, B: Prop, C: Prop>((ab, ba): Eq<A, B>) -> Eq<Tup<C, A>, Tup<C, B>> {
(Rc::new(move |y| Tup(y.0, ab(y.1))), Rc::new(move |y| Tup(y.0, ba(y.1))))
}
pub fn tup_rev_eq_fst<A: Prop, B: Prop, C: Prop, D: Prop>(
_: Ty<C, D>,
_: Eq<Tup<A, C>, Tup<B, C>>
) -> Eq<A, B> {unimplemented!()}
pub fn tup_rev_eq_snd<A: Prop, B: Prop, C: Prop, D: Prop>(
_: Ty<C, D>,
_: Eq<Tup<C, A>, Tup<C, B>>
) -> Eq<A, B> {unimplemented!()}
pub fn tup_fst<A: Prop, B: Prop, X: Prop, Y: Prop>(
ty_tup_ab: Ty<Tup<A, B>, Tup<X, Y>>
) -> Ty<A, X> {path_semantics::ty_in_left_arg(app_fun_ty(fst_ty(), ty_tup_ab), fst_def())}
pub fn tup_snd<A: Prop, B: Prop, X: Prop, Y: Prop>(
ty_tup_ab: Ty<Tup<A, B>, Tup<X, Y>>
) -> Ty<B, Y> {path_semantics::ty_in_left_arg(app_fun_ty(snd_ty(), ty_tup_ab), snd_def())}
pub fn tup_in_left_arg<A: Prop, B: Prop, C: Prop>(x: Tup<A, B>, y: Eq<A, C>) -> Tup<C, B> {
tup_eq_fst(y).0(x)
}
pub fn tup_in_right_arg<A: Prop, B: Prop, C: Prop>(x: Tup<A, B>, y: Eq<B, C>) -> Tup<A, C> {
tup_eq_snd(y).0(x)
}
pub fn tup_eq_fst_snd<A: Prop, B: Prop>() ->
Eq<Tup<A, B>, Tup<App<Fst, Tup<A, B>>, App<Snd, Tup<A, B>>>>
{eq::transitivity(eq::symmetry(tup_eq_fst(fst_def())), tup_eq_snd(eq::symmetry(snd_def())))}
pub type Tup3<A, B, C> = Tup<A, Tup<B, C>>;
pub fn tup3_fst<A: Prop, B: Prop, C: Prop, X: Prop, Y: Prop, Z: Prop>(
x: Ty<Tup3<A, B, C>, Tup3<X, Y, Z>>
) -> Ty<A, X> {tup_fst(x)}
pub fn tup3_snd<A: Prop, B: Prop, C: Prop, X: Prop, Y: Prop, Z: Prop>(
x: Ty<Tup3<A, B, C>, Tup3<X, Y, Z>>
) -> Ty<B, Y> {tup_fst(tup_snd(x))}
pub fn tup3_trd<A: Prop, B: Prop, C: Prop, X: Prop, Y: Prop, Z: Prop>(
x: Ty<Tup3<A, B, C>, Tup3<X, Y, Z>>
) -> Ty<C, Z> {tup_snd(tup_snd(x))}
pub fn tup3_eq_fst<A: Prop, B: Prop, C: Prop, D: Prop>(
x: Eq<A, B>
) -> Eq<Tup3<A, C, D>, Tup3<B, C, D>> {tup_eq_fst(x)}
pub fn tup3_eq_snd<A: Prop, B: Prop, C: Prop, D: Prop>(
x: Eq<A, B>
) -> Eq<Tup3<C, A, D>, Tup3<C, B, D>> {tup_eq_snd(tup_eq_fst(x))}
pub fn tup3_eq_trd<A: Prop, B: Prop, C: Prop, D: Prop>(
x: Eq<A, B>
) -> Eq<Tup3<C, D, A>, Tup3<C, D, B>> {tup_eq_snd(tup_eq_snd(x))}
pub fn tup3_rev_eq_fst<A: Prop, B: Prop, C: Prop, D: Prop, X: Prop, Y: Prop>(
ty_c: Ty<C, X>,
ty_d: Ty<D, Y>,
x: Eq<Tup3<A, C, D>, Tup3<B, C, D>>
) -> Eq<A, B> {tup_rev_eq_fst(tup_ty(ty_c, ty_d), x)}
pub fn tup3_rev_eq_snd<A: Prop, B: Prop, C: Prop, D: Prop, X: Prop, Y: Prop>(
ty_c: Ty<C, X>,
ty_d: Ty<D, Y>,
x: Eq<Tup3<C, A, D>, Tup3<C, B, D>>
) -> Eq<A, B> {tup_rev_eq_fst(ty_d, tup_rev_eq_snd(ty_c, x))}
pub fn tup3_rev_eq_trd<A: Prop, B: Prop, C: Prop, D: Prop, X: Prop, Y: Prop>(
ty_c: Ty<C, X>,
ty_d: Ty<D, Y>,
x: Eq<Tup3<C, D, A>, Tup3<C, D, B>>
) -> Eq<A, B> {tup_rev_eq_snd(ty_d, tup_rev_eq_snd(ty_c, x))}
#[derive(Copy, Clone)]
pub struct Fst(());
pub fn fst_ty<A: Prop, B: Prop>() -> Ty<Fst, Pow<A, Tup<A, B>>> {unimplemented!()}
pub fn fst_is_const() -> IsConst<Fst> {unimplemented!()}
pub fn fst_def<A: Prop, B: Prop>() -> Eq<App<Fst, Tup<A, B>>, A> {unimplemented!()}
pub fn fst_lower<T: Prop, X: Prop, A: Prop, B: Prop>(
_: Ty<T, Tup<Ty<X, A>, B>>
) -> Eq<App<Fst, T>, X> {unimplemented!()}
pub fn fst<T: Prop, A: Prop, B: Prop>(x: Ty<T, Tup<A, B>>) -> Ty<App<Fst, T>, A> {
app_fun_ty(fst_ty(), x)
}
#[derive(Copy, Clone)]
pub struct Snd(());
pub fn snd_ty<A: Prop, B: Prop>() -> Ty<Snd, Pow<B, Tup<A, B>>> {unimplemented!()}
pub fn snd_is_const() -> IsConst<Snd> {unimplemented!()}
pub fn snd_def<A: Prop, B: Prop>() -> Eq<App<Snd, Tup<A, B>>, B> {unimplemented!()}
pub fn snd_lower<T: Prop, X: Prop, A: Prop, B: Prop>(
_: Ty<T, Tup<A, Ty<X, B>>>
) -> Eq<App<Snd, T>, X> {unimplemented!()}
pub fn snd<T: Prop, A: Prop, B: Prop>(x: Ty<T, Tup<A, B>>) -> Ty<App<Snd, T>, B> {
app_fun_ty(snd_ty(), x)
}
#[derive(Clone, Copy)]
pub struct Subst<E, A, B>(E, A, B);
pub fn subst_trivial<A: Prop, B: Prop>() -> Eq<Subst<A, A, B>, B> {unimplemented!()}
pub fn subst_id<A: Prop, B: Prop>() -> Eq<Subst<A, B, A>, A> {unimplemented!()}
pub fn subst_nop<A: Prop, B: Prop>() -> Eq<Subst<A, B, B>, A> {unimplemented!()}
pub fn subst_ty<A: Prop, B: Prop, C: Prop>(_ty_a: Ty<A, B>) -> Eq<Subst<B, C, A>, B> {
unimplemented!()
}
pub fn subst_const<A: Prop, B: Prop, C: Prop>(_a_is_const: IsConst<A>) -> Eq<Subst<A, B, C>, A> {
unimplemented!()
}
pub fn subst_tup<A: Prop, B: Prop, C: Prop, D: Prop>() ->
Eq<Subst<Tup<A, B>, C, D>, Tup<Subst<A, C, D>, Subst<B, C, D>>> {unimplemented!()}
pub fn subst_lam<A: Prop, B: Prop, C: Prop, D: Prop, X: Prop>() ->
Eq<Subst<Lam<Ty<A, X>, B>, C, D>, Lam<Ty<A, Subst<X, C, D>>, Subst<Subst<B, C, D>, A, C>>>
{unimplemented!()}
pub fn subst_lam_const<A: Prop, B: Prop, C: Prop, D: Prop, X: Prop>(
_x: Eq<Subst<Lam<Ty<A, X>, B>, C, D>, Lam<Ty<A, Subst<X, C, D>>, Subst<Subst<B, C, D>, A, C>>>
) -> IsConst<A> {unimplemented!()}
pub fn subst_eq<A: Prop, B: Prop, C: Prop, D: Prop, E: Prop, F: Prop>(_x: Eq<Subst<A, C, D>, B>) ->
Eq<Subst<Subst<A, C, D>, E, F>, Subst<B, C, D>> {unimplemented!()}
pub fn subst_eq_lam_body<A: Prop, B: Prop, C: Prop, D: Prop, E: Prop>(
_x: Eq<Subst<A, C, D>, B>
) -> Eq<Lam<E, Subst<A, C, D>>, Lam<E, B>> {unimplemented!()}
#[derive(Copy, Clone)]
pub struct IsConst<A>(A);
pub fn const_tup<A: Prop, B: Prop>(a: IsConst<A>, b: IsConst<B>) -> IsConst<Tup<A, B>> {
tup_is_const(a, b)
}
pub fn tup_const<A: Prop, B: Prop>(_x: IsConst<Tup<A, B>>) -> And<IsConst<A>, IsConst<B>> {
unimplemented!()
}
pub fn const_eq<A: Prop, B: Prop>((ab, ba): Eq<A, B>) -> Eq<IsConst<A>, IsConst<B>> {
(Rc::new(move |a| IsConst(ab(a.0))), Rc::new(move |b| IsConst(ba(b.0))))
}
pub fn const_in_arg<A: Prop, B: Prop>(a: IsConst<A>, x: Eq<A, B>) -> IsConst<B> {
const_eq(x).0(a)
}
#[derive(Copy, Clone)]
pub struct Lam<X, Y>(X, Y);
pub fn lam_ty<A: Prop, B: Prop, X: Prop, Y: Prop>(
_ty_a: Ty<A, X>,
_ty_b: Ty<B, Y>,
) -> Ty<Lam<Ty<A, X>, B>, Imply<X, Y>> {unimplemented!()}
pub fn lam_lift<A: Prop, B: Prop, X: Prop>(ty_a: Ty<A, X>, b: B) -> Lam<Ty<A, X>, B> {Lam(ty_a, b)}
pub fn lam_eq_lift<A: Prop, X: Prop, B: Prop, C: Prop>(
_ty_a: Ty<A, X>,
_eq: Eq<B, C>
) -> Eq<Lam<Ty<A, X>, B>, Lam<Ty<A, X>, C>> {unimplemented!()}
pub fn lam<A: Prop, B: Prop, X: Prop, C: Prop>(
_ty_c: Ty<C, X>
) -> Eq<App<Lam<Ty<A, X>, B>, C>, Subst<B, A, C>> {unimplemented!()}
pub fn lam_app_ty<A: Prop, B: Prop, X: Prop, Y: Prop, C: Prop>(
ty_a: Ty<A, X>,
ty_b: Ty<B, Y>,
ty_c: Ty<C, X>,
) -> Ty<App<Lam<Ty<A, X>, B>, C>, Y> {
let ty_lam: Ty<Lam<Ty<A, X>, B>, Imply<X, Y>> = lam_ty(ty_a, ty_b);
let app_lam_ty: Ty<App<_, _>, Y> = app_lam_ty(ty_lam, ty_c);
app_lam_ty
}
pub fn lam_app_ty_trivial<A: Prop, B: Prop, X: Prop>(
ty_b: Ty<B, X>
) -> Ty<App<Lam<Ty<A, X>, B>, B>, X> {
path_semantics::ty_eq_left(lam_app_trivial(ty_b.clone())).1(ty_b)
}
pub fn lam_app_trivial<A: Prop, B: Prop, X: Prop>(
ty_b: Ty<B, X>
) -> Eq<App<Lam<Ty<A, X>, B>, B>, B> {
eq::transitivity(lam(ty_b), subst_id())
}
pub type LamId<A, X> = Lam<Ty<A, X>, A>;
pub fn lam_id_eq<A: Prop, X: Prop>() -> Eq<LamId<A, X>, FId> {unimplemented!()}
pub fn lam_id_q<A: Prop, X: Prop>() -> Q<LamId<A, X>, FId> {
hooo::q_in_left_arg(quality::right(id_q()), hooo::tauto_eq_symmetry(tauto!(lam_id_eq())))
}
pub fn lam_id_ty<A: Prop, X: Prop>(ty_a: Ty<A, X>) -> Ty<LamId<A, X>, Imply<X, X>> {
lam_ty(ty_a.clone(), ty_a)
}
pub fn lam_id_app_ty<A: Prop, B: Prop, X: Prop>(
ty_a: Ty<A, X>,
ty_b: Ty<B, X>,
) -> Ty<App<LamId<A, X>, B>, X> {
app_lam_ty(lam_id_ty(ty_a), ty_b)
}
pub fn lam_id<A: Prop, B: Prop, X: Prop>() -> Eq<App<LamId<A, X>, B>, B> {
eq::transitivity(app_map_eq(quality::to_eq(lam_id_q())), id_def())
}
pub type LamFst<A, X, B, Y> = Lam<Ty<A, X>, Lam<Ty<B, Y>, A>>;
pub fn lam_fst_ty<A: Prop, X: Prop, B: Prop, Y: Prop>(
ty_a: Ty<A, X>,
ty_b: Ty<B, Y>,
) -> Ty<LamFst<A, X, B, Y>, Imply<X, Imply<Y, X>>> {
lam_ty(ty_a.clone(), lam_ty(ty_b, ty_a))
}
pub fn lam_fst<A: Prop, X: Prop, B: Prop, Y: Prop, C: Prop>(
ty_c: Ty<C, X>
) -> Eq<App<LamFst<A, X, B, Y>, C>, Lam<Ty<B, Subst<Y, A, C>>, C>> {
eq::transitivity(eq::transitivity(lam(ty_c), subst_lam()),
subst_eq_lam_body(eq::transitivity(subst_eq(subst_trivial()), subst_id())))
}
pub type LamSnd<A, X, B, Y> = Lam<Ty<A, X>, LamId<B, Y>>;
pub fn lam_snd_ty<A: Prop, X: Prop, B: Prop, Y: Prop>(
ty_a: Ty<A, X>,
ty_b: Ty<B, Y>
) -> Ty<LamSnd<A, X, B, Y>, Imply<X, Imply<Y, Y>>> {
lam_ty(ty_a, lam_ty(ty_b.clone(), ty_b))
}
pub fn lam_snd<A: Prop, B: Prop, C: Prop, X: Prop, Y: Prop>(
ty_c: Ty<C, X>
) -> Eq<App<LamSnd<A, X, B, Y>, C>, Lam<Ty<B, Subst<Y, A, C>>, B>> {
let x2 = subst_lam();
let b_is_const = subst_lam_const(x2.clone());
eq::transitivity(lam(ty_c), eq::transitivity(x2,
subst_eq_lam_body(eq::transitivity(subst_eq(subst_const(b_is_const.clone())),
subst_const(b_is_const)))))
}
pub type DepFunTy<A, X, PredP> = Pow<App<PredP, A>, Ty<A, X>>;
pub type DepFun<F, A, X, PredP> = Ty<F, DepFunTy<A, X, PredP>>;
pub type DepLamTy<A, X, PredP> = Imply<Ty<A, X>, App<PredP, X>>;
pub type DepLam<F, A, X, PredP> = Ty<F, DepLamTy<A, X, PredP>>;
pub type DepTupTy<A, X, PredP> = Tup<Ty<A, X>, App<PredP, A>>;
pub type DepTup<A, X, B, PredP> = Ty<Tup<A, B>, DepTupTy<A, X, PredP>>;
pub fn dep_fun_pord<A: Prop, B: Prop, X: Prop, Y: Prop>(
_: POrdProof<A, X>,
_: Pow<POrdProof<B, Y>, A>
) -> POrdProof<Pow<B, A>, Pow<Y, X>> {unimplemented!()}
pub fn dep_fun_ty<A: Prop, B: Prop, X: Prop, Y: Prop>(
_ty_a: Ty<A, X>,
_ty_b: Pow<Ty<B, Y>, A>
) -> Ty<Pow<B, A>, Pow<Y, X>> {unimplemented!()}
pub fn dep_tup_pord<A: Prop, B: Prop, X: Prop, Y: Prop>(
_: POrdProof<A, X>,
_: Pow<POrdProof<B, Y>, A>
) -> POrdProof<Tup<A, B>, Tup<X, Y>> {unimplemented!()}
pub fn dep_tup_ty<A: Prop, B: Prop, X: Prop, Y: Prop>(
ty_a: Ty<A, X>,
ty_b: Pow<Ty<B, Y>, A>
) -> Ty<Tup<A, B>, Tup<X, Y>> {
let ty_a2 = ty_a.clone();
let x: Imply<Tup<A, B>, Tup<X, Y>> = Rc::new(move |tup_ab| {
let x: Ty<B, Y> = ty_b(tup_ab.0.clone());
tup_ty(ty_a2.clone(), x).0(tup_ab)
});
let y: POrdProof<Tup<A, B>, Tup<X, Y>> = dep_tup_pord(ty_a.1, ty_b.trans(and::snd));
(x, y)
}
pub fn dep_app<F: Prop, X: Prop, A: Prop, B: Prop>(
_: Pow<App<F, A>, Ty<A, X>>
) -> Pow<App<F, B>, Ty<B, X>> {unimplemented!()}
pub fn dep_fun_app<F: Prop, A: Prop, B: Prop>(_: App<Pow<App<F, A>, A>, B>) -> App<F, B> {
unimplemented!()
}
fn dep_fun_swap_app_ty<F: Prop, A: Prop, B: Prop, X: Prop, Y: Prop>(
x: Ty<F, Pow<App<Y, A>, Ty<A, X>>>
) -> Ty<F, Pow<App<Y, B>, Ty<B, X>>> {
path_semantics::ty_in_right_arg(x, (Rc::new(dep_app), Rc::new(dep_app)))
}
pub fn dep_fun_ty_formation<A: Prop, X: Prop, P: Prop>(
ty_x: Tauto<Ty<X, Type<Z>>>,
pow_ty_pa_ty_a: Pow<Ty<App<P, A>, Type<Z>>, Ty<A, X>>
) -> Tauto<Ty<DepFunTy<A, X, P>, Type<Z>>> {
use hooo::{pow_lift, hooo_rev_and};
fn f<A: Prop, B: Prop, X: Prop, Y: Prop>((x, y): And<Ty<A, X>, Pow<Ty<B, Y>, A>>) ->
Ty<Pow<B, A>, Pow<Y, X>> {dep_fun_ty(x, y)}
fn g<A: Prop, B: Prop>(x: Ty<Pow<B, A>, Pow<Type<Z>, Type<Z>>>) -> Ty<Pow<B, A>, Type<Z>> {
path_semantics::ty_transitivity(x, fun_type_ty())
}
hooo_rev_and((ty_x.trans(judgement_ty), pow_lift(pow_ty_pa_ty_a))).trans(f).trans(g)
}
pub fn dep_fun_intro<A: Prop, B: Prop, X: Prop, Y: Prop, P: Prop>(
x: Pow<Ty<App<P, A>, App<Y, A>>, Ty<A, X>>
) -> Tauto<Ty<Pow<App<P, A>, A>, Pow<App<Y, B>, Ty<B, X>>>> {
use hooo::{pow_transitivity, tauto_hooo_ty};
tauto_hooo_ty(pow_transitivity(path_semantics::ty_lower, x.clone())).trans(dep_fun_swap_app_ty)
}
pub fn dep_fun_elim<F: Prop, X: Prop, P: Prop, A: Prop, B: Prop>(
ty_f: Tauto<Ty<F, Pow<App<P, A>, Ty<A, X>>>>,
ty_b: Tauto<Ty<B, X>>
) -> Tauto<Ty<App<F, B>, App<P, B>>> {
use hooo::hooo_rev_and;
fn g<F: Prop, A: Prop, X: Prop, Y: Prop>(
(f, x): And<Ty<F, Pow<Y, Ty<A, X>>>, Ty<A, X>>
) -> Ty<App<F, A>, Y> {app_fun_ty(f, path_semantics::ty_lift(x))}
let x: Tauto<Ty<F, Pow<App<P, B>, Ty<B, X>>>> = ty_f.trans(dep_fun_swap_app_ty);
hooo_rev_and((x, ty_b)).trans(g::<F, B, X, App<P, B>>)
}
pub fn dep_tup_ty_formation<A: Prop, X: Prop, P: Prop>(
ty_x: Tauto<Ty<X, Type<Z>>>,
pow_ty_pa_ty_a: Pow<Ty<App<P, A>, Type<Z>>, Ty<A, X>>
) -> Tauto<Ty<DepTupTy<A, X, P>, Type<Z>>> {
use hooo::{pow_lift, hooo_rev_and};
fn f<A: Prop, B: Prop, X: Prop, Y: Prop>((x, y): And<Ty<A, X>, Pow<Ty<B, Y>, A>>) ->
Ty<Tup<A, B>, Tup<X, Y>> {dep_tup_ty(x, y)}
fn g<A: Prop, B: Prop>(x: Ty<Tup<A, B>, Tup<Type<Z>, Type<Z>>>) -> Ty<Tup<A, B>, Type<Z>> {
path_semantics::ty_transitivity(x, tup_type_ty())
}
hooo_rev_and((ty_x.trans(judgement_ty), pow_lift(pow_ty_pa_ty_a))).trans(f).trans(g)
}
pub fn dep_tup_intro<A: Prop, X: Prop, B: Prop, P: Prop>(
ty_a: Tauto<Ty<A, X>>,
ty_b: Tauto<Ty<B, App<P, A>>>,
) -> Tauto<DepTup<A, X, B, P>> {
let f = hooo::hooo_imply(tauto!(Rc::new(move |(ty_a, ty_b)| tup_ty(ty_a, ty_b))));
let x = hooo::hooo_rev_and((ty_a.trans(path_semantics::ty_lift), ty_b));
f(x)
}
pub fn dep_tup_elim<T: Prop, X: Prop, A: Prop, B: Prop>(
ty_t: Tauto<Ty<T, Tup<Ty<X, A>, App<B, X>>>>
) -> And<Tauto<Ty<App<Fst, T>, A>>, Tauto<Ty<App<Snd, T>, App<B, App<Fst, T>>>>> {
use hooo::{tauto_eq_symmetry, tauto_in_arg};
use path_semantics::{ty_eq_left, ty_eq_right, ty_lower};
let x = ty_t.trans(fst_lower);
(tauto_in_arg(ty_t.trans(fst), tauto_eq_symmetry(x.trans(ty_eq_left)
.trans(ty_eq_right))).trans(ty_lower),
tauto_in_arg(ty_t.trans(snd), tauto_eq_symmetry(x.trans(app_eq).trans(ty_eq_right))))
}
#[derive(Copy, Clone)]
pub struct ParTup(());
pub type Par<F, G> = App<ParTup, Tup<F, G>>;
pub type ParInv<F, G> = Par<Inv<F>, Inv<G>>;
pub fn par_tup_fun_ty<F: Prop, G: Prop, X1: Prop, X2: Prop, Y1: Prop, Y2: Prop>(
_ty_f: Ty<F, Pow<Y1, X1>>,
_ty_g: Ty<G, Pow<Y2, X2>>,
) -> Ty<Par<F, G>, Pow<Tup<Y1, Y2>, Tup<X1, X2>>> {
unimplemented!()
}
pub fn par_tup_lam_ty<F: Prop, G: Prop, X1: Prop, X2: Prop, Y1: Prop, Y2: Prop>(
_ty_f: Ty<F, Imply<X1, Y1>>,
_ty_g: Ty<G, Imply<X2, Y2>>,
) -> Ty<Par<F, G>, Imply<Tup<X1, X2>, Tup<Y1, Y2>>> {
unimplemented!()
}
pub fn par_tup_is_const() -> IsConst<ParTup> {unimplemented!()}
pub fn par_tup_id() -> Eq<Par<FId, FId>, FId> {unimplemented!()}
pub fn par_tup_app_is_const<F: Prop, G: Prop>(
f: IsConst<F>,
g: IsConst<G>
) -> IsConst<Par<F, G>> {
app_is_const(par_tup_is_const(), tup_is_const(f, g))
}
pub fn par_tup_comp<F1: Prop, F2: Prop, G1: Prop, G2: Prop>() ->
Eq<Comp<Par<G1, G2>, Par<F1, F2>>, Par<Comp<G1, F1>, Comp<G2, F2>>>
{unimplemented!()}
pub fn par_tup_inv<F: Prop, G: Prop>() -> Eq<Inv<Par<F, G>>, ParInv<F, G>>
{unimplemented!()}
pub fn par_tup_def<F: Prop, G: Prop, I0: Prop, I1: Prop, O0: Prop, O1: Prop>(
_eq0: Eq<App<F, I0>, O0>,
_eq1: Eq<App<G, I1>, O1>,
) -> Eq<App<Par<F, G>, Tup<I0, I1>>, Tup<O0, O1>> {unimplemented!()}
#[derive(Copy, Clone)]
pub struct Norm1<F, G1, G2>(pub Comp<Comp<G2, F>, Inv<G1>>);
pub type SymNorm1<F, G> = Norm1<F, G, G>;
#[derive(Copy, Clone)]
pub struct Norm2<F, G1, G2, G3>(pub Comp<Comp<G3, F>, ParInv<G1, G2>>);
pub type SymNorm2<F, G> = Norm2<F, G, G, G>;
pub fn norm1_def<F: Prop, G1: Prop, G2: Prop>() ->
Eq<Norm1<F, G1, G2>, Comp<Comp<G2, F>, Inv<G1>>> {eqx!(def Norm1)}
pub fn norm2_def<F: Prop, G1: Prop, G2: Prop, G3: Prop>() ->
Eq<Norm2<F, G1, G2, G3>, Comp<Comp<G3, F>, ParInv<G1, G2>>> {eqx!(def Norm2)}
pub fn norm1_comp<F: Prop, G1: Prop, G2: Prop, G3: Prop, G4: Prop>() ->
Eq<Norm1<Norm1<F, G1, G2>, G3, G4>, Norm1<F, Comp<G3, G1>, Comp<G4, G2>>>
{
let y = eq::transitivity(comp_eq_left(comp_assoc()), eq::symmetry(comp_assoc()));
let y = eq::transitivity(eq::transitivity(y, comp_eq_right(comp_inv())), comp_eq_left(comp_assoc()));
eqx!(eqx!(y, norm1_def, cr, cl, l), norm1_def, l, r)
}
pub fn sym_norm1_comp<F: Prop, G1: Prop, G2: Prop>() ->
Eq<SymNorm1<SymNorm1<F, G1>, G2>, SymNorm1<F, Comp<G2, G1>>>
{norm1_comp()}
pub fn norm1_eq<F: Prop, G1: Prop, G2: Prop, H: Prop>(x: Eq<F, H>) ->
Eq<Norm1<F, G1, G2>, Norm1<H, G1, G2>> {eqx!(comp_eq_left(comp_eq_right(x)), norm1_def, eq)}
pub fn norm1_eq_in<F: Prop, G1: Prop, G2: Prop, H: Prop>(x: Eq<G1, H>) ->
Eq<Norm1<F, G1, G2>, Norm1<F, H, G2>> {eqx!(comp_eq_right(inv_eq(x)), norm1_def, eq)}
pub fn norm1_eq_out<F: Prop, G1: Prop, G2: Prop, H: Prop>(x: Eq<G2, H>) ->
Eq<Norm1<F, G1, G2>, Norm1<F, G1, H>>
{eqx!(eqx!(comp_eq_left(comp_eq_left(x)), norm1_def, l), norm1_def, r)}
pub fn norm2_eq<F: Prop, G1: Prop, G2: Prop, G3: Prop, H: Prop>(x: Eq<F, H>) ->
Eq<Norm2<F, G1, G2, G3>, Norm2<H, G1, G2, G3>>
{eqx!(comp_eq_left(comp_eq_right(x)), norm2_def, eq)}
pub fn eq_norm2_norm1<F: Prop, G1: Prop, G2: Prop, G3: Prop>() ->
Eq<Norm2<F, G1, G2, G3>, Norm1<F, Par<G1, G2>, G3>>
{eqx!(eqx!(comp_eq_right(eq::symmetry(par_tup_inv())), norm1_def, r), norm2_def, l)}
pub fn eq_norm2_norm1_comp<F: Prop, G1: Prop, G2: Prop, G3: Prop, G4: Prop, G5: Prop, G6: Prop>()
-> Eq<Norm2<Norm2<F, G1, G2, G3>, G4, G5, G6>,
Norm1<Norm1<F, Par<G1, G2>, G3>, Par<G4, G5>, G6>>
{eq::transitivity(norm2_eq(eq_norm2_norm1()), eq_norm2_norm1())}
pub fn norm2_comp<F: Prop, G1: Prop, G2: Prop, G3: Prop, G4: Prop, G5: Prop, G6: Prop>() ->
Eq<Norm2<Norm2<F, G1, G2, G3>, G4, G5, G6>, Norm2<F, Comp<G4, G1>, Comp<G5, G2>, Comp<G6, G3>>>
{
let (y0, y1) = eq_norm2_norm1_comp();
let (y2, y3) = norm1_comp();
let (y4, y5) = eq_norm2_norm1();
let (x0, x1) = norm1_eq_in(par_tup_comp());
(imply::transitivity(imply::transitivity(imply::transitivity(y0, y2), x0), y5),
imply::transitivity(imply::transitivity(imply::transitivity(y4, x1), y3), y1))
}
pub fn sym_norm2_comp<F: Prop, G1: Prop, G2: Prop>() ->
Eq<SymNorm2<SymNorm2<F, G1>, G2>, SymNorm2<F, Comp<G2, G1>>>
{norm2_comp()}
pub fn sym_norm1_id<F: Prop>() -> Eq<SymNorm1<F, FId>, F> {
let x = quality::to_eq(id_q());
let x = eq::transitivity(eq::transitivity(comp_eq_right(x), comp_id_right()), comp_id_left());
eqx!(x, norm1_def, l)
}
pub fn sym_norm2_id<F: Prop>() -> Eq<SymNorm2<F, FId>, F> {
let x = eqx!(comp_eq_right(inv_eq(par_tup_id())), norm1_def, eq);
eq::transitivity(eq::transitivity(eq_norm2_norm1(), x), sym_norm1_id())
}
pub fn norm1_inv<F: Prop>() -> Eq<Norm1<FId, F, FId>, Inv<F>> {
eqx!(eq::transitivity(comp_eq_left(comp_id_left()), comp_id_left()), norm1_def, l)
}
pub type FunExtAppEq<F, G, A, X> = Comp<Lam<Ty<A, X>, Eq<App<F, A>, App<G, A>>>, Comp<Snd, Snd>>;
pub type FunExtTy<F, G, X, Y, A> = DepFunTy<
Tup3<F, G, A>, Tup3<Pow<Y, X>, Pow<Y, X>, X>,
FunExtAppEq<F, G, A, X>,
>;
#[derive(Copy, Clone)]
pub struct FunExt(());
pub fn fun_ext_ty<F: Prop, G: Prop, X: Prop, Y: Prop, A: Prop>() ->
Ty<App<FunExt, Tup<F, G>>, Pow<FunExtTy<F, G, X, Y, A>, Tauto<Eq<F, G>>>>
{unimplemented!()}
pub fn qu_inv_fun_ext<F: Prop, G: Prop>() -> Qu<Inv<App<FunExt, Tup<F, G>>>> {unimplemented!()}
pub fn fun_ext_app_eq_from_eq<F: Prop, G: Prop, A: Prop, X: Prop>(
ty_a: Ty<A, X>,
eq: Eq<F, G>
) -> App<FunExtAppEq<F, G, A, X>, Tup3<F, G, A>> {
let x = app_map_eq(comp_eq_left(lam_eq_lift(ty_a.clone(),
(True.map_any(), app_map_eq(eq).map_any()))));
let x = eq::transitivity(x, eq::symmetry(eq_app_comp()));
let x = eq::transitivity(x, app_eq(eq::symmetry(eq_app_comp())));
let x = eq::transitivity(eq::transitivity(x, app_eq(app_eq(snd_def()))), app_eq(snd_def()));
eq::transitivity(x, eq::transitivity(lam(ty_a), subst_nop())).1(True)
}
pub fn fun_ext<F: Prop, G: Prop, X: Prop, Y: Prop, A: Prop>(
tauto_eq_fg: Tauto<Eq<F, G>>
) -> FunExtTy<F, G, X, Y, A> {
use path_semantics::ty_eq_left;
use hooo::{hooo_eq, hooo_imply, pow_eq_right, pow_transitivity, tauto_eq_symmetry, tr};
fn g<F: Prop, G: Prop>(x: Eq<F, G>) -> Eq<Eq<F, F>, Eq<F, G>> {
(x.map_any(), eq::refl().map_any())
}
fn h<A: Prop, B: Prop, C: Prop, X: Prop>(ty_a: Ty<A, X>) ->
Imply<Eq<B, C>, Eq<Lam<Ty<A, X>, B>, Lam<Ty<A, X>, C>>>
{Rc::new(move |x| lam_eq_lift(ty_a.clone(), x))}
let x = hooo_imply(h)(hooo::tr().trans(tauto_eq_fg.trans(app_map_eq).trans(g)))
.trans(comp_eq_left).trans(app_map_eq);
let y = {
let x = tauto_eq_symmetry(tauto_eq_fg).trans(tup3_eq_snd);
eq::transitivity(hooo_eq(tr().trans(x.trans(app_eq))), pow_eq_right(x.trans(ty_eq_left)))
};
eq::in_left_arg(hooo_eq(pow_transitivity(tup3_trd, x)), y).0(fun_ext_refl())
}
pub fn fun_rev_ext<F: Prop, G: Prop, X: Prop, Y: Prop, A: Prop>(
x: FunExtTy<F, G, X, Y, A>
) -> Tauto<Eq<F, G>> {path_inv(qu_inv_fun_ext(), fun_ext_ty(), fun_ext)(x)}
pub fn fun_ext_app_eq_refl<F: Prop, A: Prop, X: Prop>(
ty_a: Ty<A, X>
) -> App<FunExtAppEq<F, F, A, X>, Tup3<F, F, A>> {fun_ext_app_eq_from_eq(ty_a, eq::refl())}
pub fn fun_ext_refl<F: Prop, X: Prop, Y: Prop, A: Prop>() -> FunExtTy<F, F, X, Y, A> {
hooo::pow_transitivity(tup3_trd, fun_ext_app_eq_refl)
}
pub fn fun_ext_symmetry<F: Prop, G: Prop, X: Prop, Y: Prop, A: Prop>(
x: FunExtTy<F, G, X, Y, A>
) -> FunExtTy<G, F, X, Y, A> {fun_ext(hooo::tauto_eq_symmetry(fun_rev_ext(x)))}
pub fn fun_ext_transitivity<F: Prop, G: Prop, H: Prop, X: Prop, Y: Prop, A: Prop>(
fun_ext_fg: FunExtTy<F, G, X, Y, A>,
fun_ext_gh: FunExtTy<G, H, X, Y, A>,
) -> FunExtTy<F, H, X, Y, A> {
let fg = fun_rev_ext(fun_ext_fg);
let gh = fun_rev_ext(fun_ext_gh);
fun_ext(hooo::tauto_eq_transitivity(fg, gh))
}