List of all items
Structs
- True
- ava_modal::Pos
- con_qubit::ConQubit
- fun::App
- fun::Dup
- fun::FComp
- fun::Fst
- fun::IsConst
- fun::Lam
- fun::Norm1
- fun::Norm2
- fun::ParTup
- fun::Snd
- fun::Subst
- fun::Tup
- fun::Type
- fun::bool_alg::AndNotEq
- fun::bool_alg::Bool
- fun::bool_alg::FAnd
- fun::bool_alg::FFalse1
- fun::bool_alg::FImply
- fun::bool_alg::FNand
- fun::bool_alg::FNot
- fun::bool_alg::FOr
- fun::bool_alg::FTrue1
- fun::bool_alg::FXor
- fun::bool_alg::Fa
- fun::bool_alg::Tr
- fun::feq::FEq
- fun::fin::Empty
- fun::fin::Fin
- fun::fin::FinSucc
- fun::fun_ext::FFunExt
- fun::id::FId
- fun::inv::FInv
- fun::list::FConcat
- fun::list::FCons
- fun::list::FLen
- fun::list::FList
- fun::list::FNil
- fun::list::Head
- fun::list::Tail
- fun::natc::FAddc
- fun::natc::FMulc
- fun::natc::FSc
- fun::natc::Natc
- fun::natc::Zc
- fun::natp::FAdd
- fun::natp::FEven
- fun::natp::FMul
- fun::natp::FOdd
- fun::natp::FSucc
- fun::natp::Nat
- fun::natp::Prev
- fun::natp::Zero
- fun::real::Add
- fun::real::Aleph
- fun::real::Ge
- fun::real::Gt
- fun::real::Le
- fun::real::Lt
- fun::real::Neg
- fun::real::Real
- fun::real::Sub
- fun::real::Zero
- hott::Id
- hott::IsHType
- hott::Refl
- nat::S
- nat::Z
- path_semantics::LTrue
- path_semantics::POrdProof
- qubit::Qubit
- queenity::Sq
Enums
Traits
- DProp
- Decidable
- Prop
- con_qubit::ConQubitParadox
- existence::Catuskoti
- existence::EProp
- existence::Existential
- fun::VProp
- fun::phott::QuHLev
- fun_traits::RawIdDef
- halt::Halt
- hooo::pow::PowExt
- hooo_traits::ConstructiveHoooRevNot
- hooo_traits::ConstructivePowNot
- hooo_traits::GlobalTautoHoooRevImply
- hooo_traits::HoooDualEq
- hooo_traits::HoooDualImply
- hooo_traits::HoooNRImply
- hooo_traits::HoooNeq
- hooo_traits::HoooNot
- hooo_traits::HoooRevImply
- hooo_traits::Lob
- hooo_traits::TautoHoooDualImply
- hooo_traits::TautoHoooNRImply
- hooo_traits::TautoHoooNeq
- hooo_traits::TautoHoooNot
- hooo_traits::TautoHoooRevImply
- nat::Add
- nat::Dec
- nat::EqNat
- nat::Lt
- nat::Nat
- path_semantics::DLProp
- path_semantics::ELProp
- path_semantics::LProp
- path_semantics::Lookup
- path_semantics::POrd
- path_semantics::SortMax
- path_semantics::SortMin
- quality_traits::IdQ
- quality_traits::NoOtherQ
- quality_traits::PurePlatonism
- quality_traits::QId
- quality_traits::SeshNeq
- quality_traits::UniqQ
- queenity::NoOtherSq
- queenity::UniqSq
- univalence::HLev
- univalence::HomotopyEquality
- univalence::HomotopyEquivalence
- univalence::HomotopyLevel0
Macros
Functions
- and::assoc
- and::distrib
- and::eq_left
- and::eq_left_false
- and::eq_right
- and::eq_right_false
- and::exc_both
- and::exc_left
- and::exc_right
- and::false_arg
- and::from_de_morgan
- and::from_imply
- and::fst
- and::in_left
- and::in_left_arg
- and::in_right
- and::in_right_arg
- and::paradox
- and::paradox_e
- and::rev_assoc
- and::rev_distrib
- and::rev_eq_left_true
- and::rev_eq_right_true
- and::snd
- and::symmetry
- and::to_de_morgan
- and::to_eq_neg
- and::to_eq_pos
- and::to_imply
- and::to_or
- and::true_arg
- ava_modal::eq_nnec_posn
- ava_modal::eq_nnecn_pos
- ava_modal::eq_nposn_nec
- ava_modal::eq_posn_nnec
- ava_modal::nec_to_tauto
- ava_modal::nnpara_para_to_nnpos
- ava_modal::nnpos_to_nnpara_para
- ava_modal::not_not_to_pos
- ava_modal::npos_to_para
- ava_modal::para_to_npos
- ava_modal::pos_not
- ava_modal::pos_to_not_not
- ava_modal::pos_to_para_para
- ava_modal::tauto_to_nec
- ava_modal::to_pos_tauto_eq
- con_qubit::and_neg_to_caq
- con_qubit::and_pos_to_cq
- con_qubit::caq_left
- con_qubit::caq_right
- con_qubit::caq_symmetry
- con_qubit::caq_to_cqun
- con_qubit::caq_to_eq
- con_qubit::caq_transitivity
- con_qubit::cq_left
- con_qubit::cq_right
- con_qubit::cq_symmetry
- con_qubit::cq_to_cqu
- con_qubit::cq_to_eq
- con_qubit::cq_transitivity
- con_qubit::cqu_to_cq
- con_qubit::cqu_unwrap_to_nn
- con_qubit::cqun_to_caq
- con_qubit::excm_to_nncqu
- con_qubit::excmcqu_to_cqu
- con_qubit::ncaq_symmetry
- con_qubit::ncq_symmetry
- con_qubit::ncqu_absurd
- con_qubit::nn_cqunn_to_ncqun_absurd
- con_qubit::nnccq_to_cq
- eq::absurd
- eq::anti
- eq::assoc
- eq::assoc_eq
- eq::assoc_left
- eq::assoc_right
- eq::contra
- eq::contra_excm
- eq::double_neg
- eq::eq_left
- eq::eq_not_to_neq
- eq::eq_right
- eq::eq_to_eq_excm
- eq::imply_to_or_da
- eq::imply_to_or_db
- eq::in_left
- eq::in_left_arg
- eq::in_right
- eq::in_right_arg
- eq::inv_triangle
- eq::is_false
- eq::is_true
- eq::modus_tollens
- eq::neq_left
- eq::neq_right
- eq::neq_symmetry
- eq::neq_to_eq_not
- eq::neq_to_nand
- eq::refl
- eq::rev_modus_tollens
- eq::rev_modus_tollens_eq_excm
- eq::rev_modus_tollens_excm
- eq::rev_modus_tollens_imply_excm
- eq::swap_left
- eq::swap_right
- eq::symmetry
- eq::symmetry_eq
- eq::to_eq_false
- eq::trans3
- eq::trans4
- eq::trans5
- eq::transitivity
- eq::transpose
- eq::triangle
- eq::true_eq
- existence::and
- existence::and_ea_eb_to_excm_crosseq
- existence::and_ea_eb_to_or_crosseq
- existence::catuskoti_e_absurd
- existence::catuskoti_excm_absurd
- existence::crosseq_adj_to_eqe
- existence::crosseq_adj_to_ncrosseq
- existence::crosseq_adjoint
- existence::crosseq_refl
- existence::crosseq_symmetry
- existence::crosseq_to_eqe
- existence::crosseq_to_eqn
- existence::crosseq_to_eqnn
- existence::crosseq_transitivity
- existence::double_neg_e
- existence::en
- existence::eq_to_crosseq
- existence::eqn_to_crosseq
- existence::eqnn_to_crosseq
- existence::excm_to_e
- existence::imply
- existence::imply_e
- existence::or
- existence::or_e
- existence::or_from_de_morgan
- existence::rev_crosseq_adjoint
- existence::rev_en
- fun::and_is_const
- fun::app2_fun_ty
- fun::app2_lam_ty
- fun::app_eq
- fun::app_fun_ext
- fun::app_fun_swap_ty
- fun::app_fun_ty
- fun::app_fun_unfold
- fun::app_is_const
- fun::app_lam_ty
- fun::app_lift_ty_lam
- fun::app_map_eq
- fun::app_rev_fun_ty
- fun::app_rev_lam_ty
- fun::app_tauto_lam_to_tauto_fun_ty
- fun::app_theory
- fun::app_to_comp
- fun::bool_alg::and_fa
- fun::bool_alg::and_is_const
- fun::bool_alg::and_tr
- fun::bool_alg::and_ty
- fun::bool_alg::bool1_cover
- fun::bool_alg::bool1_exists
- fun::bool_alg::bool1_fun_ext
- fun::bool_alg::bool2_exists
- fun::bool_alg::bool2_fun_ext
- fun::bool_alg::bool_excm_eq_fa
- fun::bool_alg::bool_excm_eq_tr
- fun::bool_alg::bool_exists_to_pow_eq_fa
- fun::bool_alg::bool_exists_to_pow_eq_tr
- fun::bool_alg::bool_is_const
- fun::bool_alg::bool_ty
- fun::bool_alg::bool_values
- fun::bool_alg::eq_norm1_by_false1
- fun::bool_alg::eq_norm1_by_true1
- fun::bool_alg::eq_norm1_not_not
- fun::bool_alg::eq_norm2_and_not_or
- fun::bool_alg::eq_norm2_or_not_and
- fun::bool_alg::eq_not_not
- fun::bool_alg::eq_not_not_idb
- fun::bool_alg::eqb_fa
- fun::bool_alg::eqb_fa_fa
- fun::bool_alg::eqb_fa_tr
- fun::bool_alg::eqb_tr
- fun::bool_alg::eqb_tr_fa
- fun::bool_alg::eqb_tr_tr
- fun::bool_alg::eqb_ty
- fun::bool_alg::fa_is_const
- fun::bool_alg::fa_ty
- fun::bool_alg::false1_def
- fun::bool_alg::false1_is_const
- fun::bool_alg::false1_ty
- fun::bool_alg::idb_def
- fun::bool_alg::idb_is_const
- fun::bool_alg::idb_ty
- fun::bool_alg::imply_def
- fun::bool_alg::imply_fa
- fun::bool_alg::imply_is_const
- fun::bool_alg::imply_tr
- fun::bool_alg::imply_ty
- fun::bool_alg::nand_def
- fun::bool_alg::nand_fa
- fun::bool_alg::nand_is_const
- fun::bool_alg::nand_tr
- fun::bool_alg::nand_ty
- fun::bool_alg::not_fa
- fun::bool_alg::not_is_const
- fun::bool_alg::not_q
- fun::bool_alg::not_tr
- fun::bool_alg::not_ty
- fun::bool_alg::or_fa
- fun::bool_alg::or_is_const
- fun::bool_alg::or_tr
- fun::bool_alg::or_ty
- fun::bool_alg::para_eq_tr_fa
- fun::bool_alg::para_inv_and
- fun::bool_alg::para_inv_false1
- fun::bool_alg::para_inv_or
- fun::bool_alg::para_inv_true1
- fun::bool_alg::tr_is_const
- fun::bool_alg::tr_ty
- fun::bool_alg::true1_def
- fun::bool_alg::true1_is_const
- fun::bool_alg::true1_ty
- fun::bool_alg::xor_def
- fun::bool_alg::xor_fa
- fun::bool_alg::xor_tr
- fun::bool_alg::xor_ty
- fun::comp_app
- fun::comp_app_def
- fun::comp_assoc
- fun::comp_eq_left
- fun::comp_eq_right
- fun::comp_id_left
- fun::comp_id_right
- fun::comp_in_left_arg
- fun::comp_in_right_arg
- fun::comp_is_const
- fun::comp_qu
- fun::comp_to_app
- fun::comp_ty
- fun::const_eq
- fun::const_in_arg
- fun::const_tup
- fun::cover
- fun::dep::dep_app
- fun::dep::dep_fun_app
- fun::dep::dep_fun_elim
- fun::dep::dep_fun_intro
- fun::dep::dep_fun_pord
- fun::dep::dep_fun_ty
- fun::dep::dep_fun_ty_formation
- fun::dep::dep_tup_elim
- fun::dep::dep_tup_intro
- fun::dep::dep_tup_pord
- fun::dep::dep_tup_ty
- fun::dep::dep_tup_ty_formation
- fun::dup_def
- fun::dup_is_const
- fun::dup_ty
- fun::eq_app_comp
- fun::eq_app_norm1
- fun::eq_app_norm2
- fun::eq_norm2_norm1
- fun::eq_norm2_norm1_comp
- fun::fcomp_is_const
- fun::feq::equal_fa_lower
- fun::feq::equal_from_para_eq
- fun::feq::equal_is_const
- fun::feq::equal_lift
- fun::feq::equal_refl
- fun::feq::equal_symmetry
- fun::feq::equal_transitivity
- fun::feq::equal_ty
- fun::feq::implicit_equal_is_const
- fun::feq::tauto_eq_to_tauto_equal
- fun::fin::empty_ty
- fun::fin::fin_succ_ty
- fun::fin::fin_ty
- fun::fst
- fun::fst_def
- fun::fst_is_const
- fun::fst_lower
- fun::fst_ty
- fun::fun_ext::fun_ext
- fun::fun_ext::fun_ext_app_eq_from_eq
- fun::fun_ext::fun_ext_app_eq_refl
- fun::fun_ext::fun_ext_refl
- fun::fun_ext::fun_ext_symmetry
- fun::fun_ext::fun_ext_transitivity
- fun::fun_ext::fun_ext_ty
- fun::fun_ext::fun_rev_ext
- fun::fun_ext::qu_inv_fun_ext
- fun::fun_to_lam_ty
- fun::fun_ty
- fun::fun_type0
- fun::fun_type_ty
- fun::id::eq_qu_false_false
- fun::id::eq_qu_true_true
- fun::id::id_def
- fun::id::id_def_type
- fun::id::id_is_const
- fun::id::id_qu
- fun::id::id_qu_ty
- fun::id::id_ty
- fun::id::implicit_id_is_const
- fun::id::not_qu_false
- fun::id::para_to_eq_qu
- fun::id::para_to_not_qu
- fun::id::pow_qu
- fun::id::pow_to_eq_qu
- fun::id::tauto_to_eq_qu
- fun::id::tauto_to_qu
- fun::id::theory
- fun::id::to_qu
- fun::id::true_qu
- fun::id::type_eq_to_q
- fun::imply_is_const
- fun::inv::comp_inv
- fun::inv::comp_inv_qu
- fun::inv::comp_left_inv_to_id
- fun::inv::comp_rev_inv
- fun::inv::comp_right_inv_to_id
- fun::inv::eq_comp_inv
- fun::inv::eq_comp_left_inv_id
- fun::inv::eq_comp_right_inv_id
- fun::inv::eq_qu_double
- fun::inv::finv_is_const
- fun::inv::id_inv
- fun::inv::id_q
- fun::inv::id_to_comp_left_inv
- fun::inv::id_to_comp_right_inv
- fun::inv::inv_double_val
- fun::inv::inv_eq
- fun::inv::inv_involve
- fun::inv::inv_is_const
- fun::inv::inv_rev_eq
- fun::inv::inv_rev_val_qu
- fun::inv::inv_swap_eq
- fun::inv::inv_ty
- fun::inv::inv_val
- fun::inv::inv_val_other
- fun::inv::inv_val_qu
- fun::inv::involve_eq
- fun::inv::involve_inv
- fun::inv::path
- fun::inv::path_inv
- fun::inv::qu_double
- fun::inv::qu_inv_tauto_eq_to_qu_inv
- fun::inv::qu_rev_double
- fun::inv::qu_tauto_eq_to_q
- fun::inv::qu_to_app_eq
- fun::inv::self_inv_to_eq_id
- fun::inv::self_inv_to_q
- fun::inv::self_inv_ty
- fun::inv::split_epic
- fun::inv::split_monic
- fun::judgement_ty
- fun::lam
- fun::lam_app_nop
- fun::lam_app_trivial
- fun::lam_app_ty
- fun::lam_app_ty_trivial
- fun::lam_eq_lift
- fun::lam_fst
- fun::lam_fst_ty
- fun::lam_id
- fun::lam_id_app_ty
- fun::lam_id_eq
- fun::lam_id_q
- fun::lam_id_ty
- fun::lam_lift
- fun::lam_snd
- fun::lam_snd_ty
- fun::lam_ty
- fun::list::concat_cons
- fun::list::concat_nil
- fun::list::concat_ty
- fun::list::cons_ty
- fun::list::head_ty
- fun::list::len_cons
- fun::list::len_nil
- fun::list::len_ty
- fun::list::list_def
- fun::list::list_exists
- fun::list::list_ty
- fun::list::nil_ty
- fun::list::norm1_concat_len
- fun::list::tail_ty
- fun::natc::addc_closed
- fun::natc::addc_sc
- fun::natc::addc_ty
- fun::natc::addc_zeroc
- fun::natc::eq_last_zeroc
- fun::natc::mulc_sc
- fun::natc::mulc_ty
- fun::natc::mulc_zc
- fun::natc::natc_def
- fun::natc::natc_ty
- fun::natc::sc_def
- fun::natc::sc_eq_rev
- fun::natc::sc_ty
- fun::natc::zeroc_ty
- fun::natp::add_assoc
- fun::natp::add_eq_left
- fun::natp::add_eq_right
- fun::natp::add_eq_zero_to_add_zero_right
- fun::natp::add_is_const
- fun::natp::add_rev_eq_left
- fun::natp::add_rev_eq_right
- fun::natp::add_subst_const_right
- fun::natp::add_succ
- fun::natp::add_succ_plus_one
- fun::natp::add_symmetry
- fun::natp::add_ty
- fun::natp::add_zero
- fun::natp::add_zero_right
- fun::natp::eq_comp_even_succ_succ
- fun::natp::eq_comp_even_succ_succ_proof
- fun::natp::eq_even_succ_succ
- fun::natp::eq_plus_one_one_two
- fun::natp::even_succ
- fun::natp::even_ty
- fun::natp::even_zero
- fun::natp::induction
- fun::natp::induction_ty
- fun::natp::mul_assoc
- fun::natp::mul_distr
- fun::natp::mul_eq_left
- fun::natp::mul_eq_right
- fun::natp::mul_is_const
- fun::natp::mul_one
- fun::natp::mul_rev_eq_left
- fun::natp::mul_rev_eq_right
- fun::natp::mul_succ
- fun::natp::mul_symmetry
- fun::natp::mul_ty
- fun::natp::mul_zero
- fun::natp::nat1_fun_ext
- fun::natp::nat_cover
- fun::natp::nat_def
- fun::natp::nat_exists
- fun::natp::nat_is_const
- fun::natp::nat_ty
- fun::natp::norm2_add_even
- fun::natp::odd_def
- fun::natp::odd_succ
- fun::natp::odd_ty
- fun::natp::odd_zero
- fun::natp::one_ty
- fun::natp::para_eq_even_odd
- fun::natp::para_eq_succ
- fun::natp::para_eq_zero_one
- fun::natp::para_pre_zero
- fun::natp::previous
- fun::natp::previous_symmetry
- fun::natp::subst_induction
- fun::natp::subst_succ
- fun::natp::succ_app_is_const
- fun::natp::succ_app_ty
- fun::natp::succ_eq
- fun::natp::succ_eq_rev
- fun::natp::succ_is_const
- fun::natp::succ_rev_app_ty
- fun::natp::succ_ty
- fun::natp::two_ty
- fun::natp::zero_is_const
- fun::natp::zero_ty
- fun::norm1_comp
- fun::norm1_def
- fun::norm1_eq
- fun::norm1_eq_in
- fun::norm1_eq_out
- fun::norm1_id
- fun::norm1_inv
- fun::norm1_ty
- fun::norm2_app
- fun::norm2_comp
- fun::norm2_def
- fun::norm2_eq
- fun::norm2_ty
- fun::or_is_const
- fun::par_tup_app_is_const
- fun::par_tup_comp
- fun::par_tup_def
- fun::par_tup_fun_ty
- fun::par_tup_id
- fun::par_tup_inv
- fun::par_tup_is_const
- fun::par_tup_lam_ty
- fun::phott::collapse_to_eq_qu_2
- fun::phott::collapse_to_hom_eq_3
- fun::phott::collapse_to_set_left
- fun::phott::collapse_to_set_right
- fun::phott::eq_tauto_is_contr
- fun::phott::is_contr_to_is_prop
- fun::phott::is_contr_to_tauto
- fun::phott::is_contr_to_tauto_eq_true
- fun::phott::is_contr_true
- fun::phott::is_prop_false
- fun::phott::is_prop_to_is_groupoid
- fun::phott::is_prop_to_is_set
- fun::phott::is_prop_true
- fun::phott::is_set_id
- fun::phott::is_set_not
- fun::phott::is_set_to_is_groupoid
- fun::phott::para_to_is_prop
- fun::phott::pow_to_is_prop
- fun::phott::tauto_eq_true_to_is_contr
- fun::phott::tauto_to_is_contr
- fun::phott::tauto_to_is_prop
- fun::pord_is_const
- fun::q_inv_ty
- fun::real::real_def
- fun::real::real_is_const
- fun::real::real_ty
- fun::real::zero_is_const
- fun::real::zero_ty
- fun::snd
- fun::snd_def
- fun::snd_is_const
- fun::snd_lower
- fun::snd_ty
- fun::subst_app
- fun::subst_const
- fun::subst_eq
- fun::subst_eq_lam_body
- fun::subst_lam
- fun::subst_lam_const
- fun::subst_nop
- fun::subst_trivial
- fun::subst_tup
- fun::subst_ty
- fun::sym_norm1_comp
- fun::sym_norm1_id
- fun::sym_norm1_ty
- fun::sym_norm2_app
- fun::sym_norm2_comp
- fun::sym_norm2_id
- fun::sym_norm2_ty
- fun::tauto_lam_to_tauto_fun_ty
- fun::tup3_eq_fst
- fun::tup3_eq_snd
- fun::tup3_eq_trd
- fun::tup3_fst
- fun::tup3_rev_eq_fst
- fun::tup3_rev_eq_snd
- fun::tup3_rev_eq_trd
- fun::tup3_snd
- fun::tup3_trd
- fun::tup_const
- fun::tup_eq
- fun::tup_eq_fst
- fun::tup_eq_fst_snd
- fun::tup_eq_snd
- fun::tup_fst
- fun::tup_fst_const
- fun::tup_in_left_arg
- fun::tup_in_right_arg
- fun::tup_is_const
- fun::tup_rev_eq_fst
- fun::tup_rev_eq_snd
- fun::tup_snd
- fun::tup_snd_const
- fun::tup_ty
- fun::tup_type_ty
- fun::ty_is_const
- fun::type_imply
- fun::type_is_const
- fun::type_ty
- halt::neg_to_para
- hooo::consistency
- hooo::cut
- hooo::cut_elim
- hooo::decide
- hooo::eq_not_para_to_eq_para
- hooo::eq_refl
- hooo::eq_tauto_para_to_para_uniform
- hooo::eq_tauto_to_eq_para
- hooo::eq_tauto_to_eq_para_excm
- hooo::exists_construct
- hooo::exists_excm_to_pow
- hooo::exists_fst
- hooo::exists_join
- hooo::exists_left
- hooo::exists_left_refl
- hooo::exists_not_to_not_pow
- hooo::exists_not_to_not_tauto_right
- hooo::exists_pow
- hooo::exists_rev_true
- hooo::exists_right
- hooo::exists_snd
- hooo::exists_tauto
- hooo::exists_to_exists_true
- hooo::exists_to_not_para
- hooo::exists_true
- hooo::exists_true_true
- hooo::fa
- hooo::hooo_and
- hooo::hooo_dual_and
- hooo::hooo_dual_neq
- hooo::hooo_dual_nrimply
- hooo::hooo_dual_or
- hooo::hooo_dual_rev_and
- hooo::hooo_dual_rev_eq
- hooo::hooo_dual_rev_imply
- hooo::hooo_dual_rev_neq
- hooo::hooo_dual_rev_nrimply
- hooo::hooo_dual_rev_or
- hooo::hooo_e_rev_not
- hooo::hooo_eq
- hooo::hooo_imply
- hooo::hooo_or
- hooo::hooo_pord
- hooo::hooo_rev_and
- hooo::hooo_rev_eq
- hooo::hooo_rev_neq
- hooo::hooo_rev_not
- hooo::hooo_rev_not_excm
- hooo::hooo_rev_nrimply
- hooo::hooo_rev_or
- hooo::hooo_rev_ty
- hooo::hooo_ty
- hooo::imply_tauto_to_imply_para
- hooo::imply_tauto_to_imply_para_excm
- hooo::lift_q
- hooo::modus_ponens_to_exists
- hooo::not_not_both_to_exists
- hooo::not_not_para_rev_double
- hooo::not_not_to_exists
- hooo::not_not_to_exists_true
- hooo::not_not_to_not_para
- hooo::not_not_to_para_para
- hooo::not_not_to_para_para_e
- hooo::not_not_to_para_para_with_tauto_excm
- hooo::not_para_to_exists
- hooo::not_para_to_not_not
- hooo::not_para_to_not_not_e
- hooo::not_para_to_para_para
- hooo::not_para_to_para_para_e
- hooo::not_para_to_para_para_with_tauto_excm
- hooo::not_tauto_not_para_to_theory
- hooo::not_theory
- hooo::para_and_to_or
- hooo::para_and_to_or_excm
- hooo::para_decide
- hooo::para_decide_e
- hooo::para_eq_symmetry
- hooo::para_eq_transitivity_left
- hooo::para_eq_transitivity_right
- hooo::para_exists_false
- hooo::para_exists_false_false
- hooo::para_from_or
- hooo::para_in_arg
- hooo::para_left_and
- hooo::para_liar
- hooo::para_not
- hooo::para_not_and_to_or_e
- hooo::para_not_and_to_or_tauto_e
- hooo::para_not_double
- hooo::para_not_rev_double
- hooo::para_not_rev_triple
- hooo::para_not_to_not_not_tauto
- hooo::para_not_to_para_para
- hooo::para_not_triple
- hooo::para_or_e
- hooo::para_para
- hooo::para_para_to_not_not
- hooo::para_para_to_not_para
- hooo::para_pow_contra
- hooo::para_pow_contra_nn
- hooo::para_rev_not
- hooo::para_right_and
- hooo::para_to_eq_false
- hooo::para_to_not
- hooo::para_to_or
- hooo::para_to_tauto_excm
- hooo::para_to_tauto_excm_transitivity
- hooo::para_to_tauto_not
- hooo::para_uniform_and
- hooo::para_uniform_to_eq_tauto_para
- hooo::pow_contra_to_pow_contra_nn
- hooo::pow_dual_rev_or_lift
- hooo::pow_eq_left
- hooo::pow_eq_refl
- hooo::pow_eq_right
- hooo::pow_eq_symmetry
- hooo::pow_eq_to_tauto_eq
- hooo::pow_eq_transitivity
- hooo::pow_excm_nn_to_rev_double
- hooo::pow_imply_to_imply_tauto_pow
- hooo::pow_in_left_arg
- hooo::pow_in_right_arg
- hooo::pow_lift
- hooo::pow_lower
- hooo::pow_modus_tollens
- hooo::pow_not
- hooo::pow_not_double_down
- hooo::pow_not_e
- hooo::pow_not_tauto_e
- hooo::pow_not_tauto_excm
- hooo::pow_refl
- hooo::pow_rev_lift_refl
- hooo::pow_right_and_symmetry
- hooo::pow_tauto_to_imply_tauto
- hooo::pow_tauto_to_pow_tauto_tauto
- hooo::pow_to_imply
- hooo::pow_to_imply_lift
- hooo::pow_to_pow_exists
- hooo::pow_to_pow_tauto
- hooo::pow_to_pow_tauto_tauto
- hooo::pow_to_tauto_imply
- hooo::pow_transitivity
- hooo::pow_ty
- hooo::pow_unfold_fa
- hooo::q_in_left_arg
- hooo::q_in_right_arg
- hooo::qu_in_arg
- hooo::tauto_and
- hooo::tauto_and_to_eq_pos
- hooo::tauto_decide
- hooo::tauto_e_to_or
- hooo::tauto_e_to_or_pow
- hooo::tauto_eq_excm_to_tauto_excm_eq
- hooo::tauto_eq_in_left_arg
- hooo::tauto_eq_symmetry
- hooo::tauto_eq_to_pow_eq
- hooo::tauto_eq_transitivity
- hooo::tauto_excm_to_not_theory
- hooo::tauto_excm_to_or
- hooo::tauto_excm_to_or_pow
- hooo::tauto_excm_to_tauto_excm_not
- hooo::tauto_excm_to_uniform
- hooo::tauto_from_eq_true
- hooo::tauto_from_para_transitivity
- hooo::tauto_hooo_and
- hooo::tauto_hooo_dual_and
- hooo::tauto_hooo_dual_neq
- hooo::tauto_hooo_dual_nrimply
- hooo::tauto_hooo_dual_or
- hooo::tauto_hooo_dual_rev_and
- hooo::tauto_hooo_dual_rev_eq
- hooo::tauto_hooo_dual_rev_imply
- hooo::tauto_hooo_dual_rev_neq
- hooo::tauto_hooo_dual_rev_nrimply
- hooo::tauto_hooo_dual_rev_or
- hooo::tauto_hooo_eq
- hooo::tauto_hooo_imply
- hooo::tauto_hooo_or
- hooo::tauto_hooo_pord
- hooo::tauto_hooo_rev_and
- hooo::tauto_hooo_rev_eq
- hooo::tauto_hooo_rev_neq
- hooo::tauto_hooo_rev_not
- hooo::tauto_hooo_rev_nrimply
- hooo::tauto_hooo_rev_or
- hooo::tauto_hooo_rev_ty
- hooo::tauto_hooo_ty
- hooo::tauto_imply_in_left_arg
- hooo::tauto_imply_in_right_arg
- hooo::tauto_imply_pow
- hooo::tauto_imply_to_imply_tauto_pow
- hooo::tauto_imply_to_pow
- hooo::tauto_imply_to_pow_tauto
- hooo::tauto_imply_transitivity
- hooo::tauto_in_arg
- hooo::tauto_modus_ponens
- hooo::tauto_not
- hooo::tauto_not_double
- hooo::tauto_not_excm
- hooo::tauto_not_to_para
- hooo::tauto_or
- hooo::tauto_or_left
- hooo::tauto_or_right
- hooo::tauto_para_rev_not
- hooo::tauto_pow_eq_left
- hooo::tauto_pow_eq_right
- hooo::tauto_pow_imply
- hooo::tauto_qu_eq
- hooo::tauto_rev_and
- hooo::tauto_rev_not
- hooo::tauto_rev_or
- hooo::tauto_to_eq_true
- hooo::tauto_to_or
- hooo::tauto_to_or_e
- hooo::tauto_to_or_pow
- hooo::tauto_to_or_pow_e
- hooo::tauto_to_para_not
- hooo::tauto_to_tauto_excm
- hooo::theory_in_arg
- hooo::theory_not_to_theory
- hooo::theory_to_not_para
- hooo::theory_to_not_tauto
- hooo::to_not_pow
- hooo::tr
- hooo::uniform
- hooo::uniform_and
- hooo::uniform_dual_and
- hooo::uniform_dual_rev_or
- hooo::uniform_in_arg
- hooo::uniform_refl
- hooo::uniform_symmetry
- hooo::uniform_to_tauto_excm
- hooo::uniform_transitivity
- hott::ap_fun
- hott::ap_lam
- hott::from_is_contr
- hott::id_in_left_arg
- hott::id_in_right_arg
- hott::id_to_eq
- hott::id_ty
- hott::is_groupoid_to_id
- hott::is_groupoid_to_is_set
- hott::is_htype_to_id
- hott::is_prop_to_id
- hott::is_set_to_id
- hott::is_set_to_is_prop
- hott::refl
- hott::to_is_contr
- hott::true_is_contr
- imply::absurd
- imply::and_map
- imply::chain
- imply::double_neg
- imply::eq_left
- imply::eq_right
- imply::flip_neg_left
- imply::flip_neg_left_excm
- imply::flip_neg_right
- imply::from_or
- imply::id
- imply::in_left
- imply::in_left_arg
- imply::in_right
- imply::in_right_arg
- imply::join
- imply::modus_ponens
- imply::modus_tollens
- imply::or_split_da
- imply::or_split_db
- imply::or_split_dc
- imply::or_split_excm_a
- imply::reduce
- imply::reorder_args
- imply::rev_chain
- imply::rev_double_neg
- imply::rev_double_neg_eq_excm
- imply::rev_double_neg_excm
- imply::rev_double_neg_imply_excm
- imply::rev_modus_ponens
- imply::rev_modus_tollens
- imply::rev_modus_tollens_eq_excm
- imply::rev_modus_tollens_excm
- imply::rev_modus_tollens_imply_excm
- imply::to_or_da
- imply::to_or_db
- imply::to_or_excm_a
- imply::to_or_excm_b
- imply::total
- imply::total_excm
- imply::transitivity
- mid::absurd_down
- mid::absurd_down_with_tauto_e
- mid::absurd_theory
- mid::absurd_theory_tauto_excm
- mid::and_e_theory_to_mid
- mid::down
- mid::down_to_e
- mid::down_to_excm
- mid::down_to_not_up
- mid::down_to_theory
- mid::down_to_up
- mid::down_to_up_with_tauto_e
- mid::down_to_virtual_not
- mid::mica_to_e
- mid::mid_to_and_e_theory
- mid::mid_to_e
- mid::mid_to_theory
- mid::paradox
- mid::subordinate
- mid::theory_to_mid
- mid::theory_to_up
- mid::theory_to_up_with_tauto_e
- mid::up
- mid::up_excm
- mid::up_to_e
- mid::up_to_not_down
- mid::up_to_theory
- mid::up_to_virtual
- mid::up_to_virtual_excm
- mid::virtual_to_theory
- modal::b
- modal::eq_nec_pos_strong_pos
- modal::eq_nnpos_nnecn
- modal::five
- modal::four
- modal::k
- modal::lob_triv
- modal::n
- modal::nec_consistency
- modal::nec_not_godel
- modal::nec_not_lob
- modal::nec_pos_to_strong_pos
- modal::nec_to_nposn
- modal::nec_to_pos
- modal::nnecn_to_nnpos
- modal::nnecn_to_pos
- modal::nnpos_to_nnecn
- modal::npara_to_pos
- modal::npos_to_para
- modal::npos_to_posn
- modal::nposn_to_nec
- modal::para_godel
- modal::para_lob
- modal::para_para_to_pos
- modal::para_to_npos
- modal::pos_to_nnecn
- modal::pos_to_npara
- modal::pos_to_para_para
- modal::posn_to_npos
- modal::strong_pos_to_nec_pos
- modal::t
- modal::to_nnpos
- nat::eq
- nat::lt
- nat::lt_neq
- not::absurd
- not::double
- not::eq
- not::rev_double
- not::rev_double_excm
- not::rev_triple
- or::assoc
- or::both
- or::bound_neg
- or::bound_pos
- or::distrib
- or::eq_nn
- or::from_de_morgan
- or::in_left_arg
- or::in_right_arg
- or::symmetry
- or::to_de_morgan
- path_semantics::assume
- path_semantics::assume_inc_path_level
- path_semantics::assume_naive
- path_semantics::assume_norm_path_level
- path_semantics::assume_refl
- path_semantics::check_q
- path_semantics::comp
- path_semantics::creation
- path_semantics::creation_hom
- path_semantics::eq_lev
- path_semantics::lt_lev
- path_semantics::naive_comp
- path_semantics::naive_red_false
- path_semantics::pand_both_eq
- path_semantics::to_naive
- path_semantics::to_pand_fst
- path_semantics::to_pand_snd
- path_semantics::to_por_fst
- path_semantics::to_por_snd
- path_semantics::ty::and
- path_semantics::ty::eq_left
- path_semantics::ty::eq_right
- path_semantics::ty::eq_true_ltrue
- path_semantics::ty::eqq_imply
- path_semantics::ty::hom_imply
- path_semantics::ty::imply_right
- path_semantics::ty::in_left_arg
- path_semantics::ty::in_right_arg
- path_semantics::ty::lift
- path_semantics::ty::lower
- path_semantics::ty::ltrue
- path_semantics::ty::neq_to_not_qu
- path_semantics::ty::neq_to_sesh
- path_semantics::ty::non_triv
- path_semantics::ty::or
- path_semantics::ty::or_split
- path_semantics::ty::or_split_da
- path_semantics::ty::or_split_db
- path_semantics::ty::or_split_dc
- path_semantics::ty::q_formation
- path_semantics::ty::qu_formation
- path_semantics::ty::transitivity
- path_semantics::ty::triv
- path_semantics::ty::true_ltrue
- path_semantics::ty::true_true
- path_semantics::ty::ty_false
- path_semantics::ty::ty_rev_true
- path_semantics::ty::ty_true
- path_semantics::ty_core
- path_semantics::ty_core_to_naive
- path_semantics::uniq_ty
- path_semantics::use_pand_both
- path_semantics::xy_norm
- quality::aq_hom_in_left_arg
- quality::aq_hom_in_right_arg
- quality::aq_inv_to_sesh
- quality::aq_left
- quality::aq_right
- quality::aq_sesh_eq_neq
- quality::aq_sesh_hom_in_left_arg
- quality::aq_sesh_hom_in_right_arg
- quality::aq_sesh_left
- quality::aq_sesh_right
- quality::aq_sesh_to_neq
- quality::aq_sesh_to_q_inv
- quality::aq_symmetry
- quality::aq_to_eq
- quality::aq_transitivity
- quality::eq_maybe_lift
- quality::eq_q_symmetry
- quality::eqq_to_excm_q
- quality::eqq_to_excm_q_with_excm_eq
- quality::hom_in_left_arg
- quality::hom_in_right_arg
- quality::left
- quality::naq_left
- quality::naq_right
- quality::naq_symmetry
- quality::neq_to_aq_sesh
- quality::neq_to_sesh
- quality::nq_left
- quality::nq_right
- quality::nq_symmetry
- quality::q_inv_to_sesh
- quality::right
- quality::sesh_eq_neq
- quality::sesh_hom_in_left_arg
- quality::sesh_hom_in_right_arg
- quality::sesh_left
- quality::sesh_right
- quality::sesh_to_neq
- quality::sesh_to_q_inv
- quality::symmetry
- quality::theory_eq_to_eqq
- quality::theory_eq_to_excm_q_with_excm_eq
- quality::to_eq
- quality::to_eq_aq
- quality::to_eq_q
- quality::transitivity
- qubit::decide
- qubit::decide_tauto_excm
- qubit::eq_q_qu
- qubit::eq_qu_q
- qubit::eq_sesh_inv
- qubit::eq_to_eq_inv
- qubit::from_eq
- qubit::from_eq_q
- qubit::in_arg
- qubit::inv_to_sesh
- qubit::normalize
- qubit::rev_normalize
- qubit::sesh_to_inv
- qubit::to_eq
- qubit::to_eq_q
- queenity::in_left_arg
- queenity::in_right_arg
- queenity::nsq_left
- queenity::nsq_left_theory
- queenity::seshatic
- queenity::sq_right
- queenity::to_imply
- queenity::to_sesh
- queenity::transitivity
- sd::in_left_arg
- sd::in_right_arg
- sd::lift_q
- sd::not_left
- sd::not_right
- sd::not_sd
- sd::para_eq_to_sd
- sd::symmetry
- sd::tauto_eq_to_nsd
- sd::to_eqq
- sd::to_not_tauto_eq
- univalence::eq_lift
- univalence::eq_univ_to_eqq
- univalence::eqq_eq_q
- univalence::eqq_to_univ
- univalence::from_hom_eq_2
- univalence::higher
- univalence::hom_eq_q
- univalence::hom_eq_refl
- univalence::hom_eq_symmetry
- univalence::hom_eq_transitivity
- univalence::hom_to_univ
- univalence::q_to_hom_eq_2
- univalence::to_hom_eq_2
- univalence::univ_eq_q
- univalence::univ_to_eqq
Type Definitions
- And
- Dneg
- Eq
- ExcM
- Iff
- Imply
- Not
- Or
- ava_modal::Nec
- con_qubit::Caq
- con_qubit::Cq
- existence::CrossCatus
- existence::CrossEq
- existence::E
- existence::EqNN
- existence::NN
- fun::App2
- fun::Comp
- fun::IsVar
- fun::LamFst
- fun::LamId
- fun::LamSnd
- fun::Par
- fun::ParInv
- fun::SymNorm1
- fun::SymNorm2
- fun::Tup3
- fun::bool_alg::All
- fun::bool_alg::Any
- fun::bool_alg::Eqb
- fun::bool_alg::FEqb
- fun::bool_alg::FIdb
- fun::bool_alg::Idb
- fun::bool_alg::Xor
- fun::dep::DepFun
- fun::dep::DepFunTy
- fun::dep::DepLam
- fun::dep::DepLamTy
- fun::dep::DepTup
- fun::dep::DepTupTy
- fun::feq::Equal
- fun::fun_ext::FunExt
- fun::fun_ext::FunExtAppEq
- fun::fun_ext::FunExtTy
- fun::id::Id
- fun::inv::Injective
- fun::inv::Inv
- fun::inv::SplitEpic
- fun::inv::SplitMonic
- fun::inv::Surjective
- fun::list::Concat
- fun::list::Cons
- fun::list::Len
- fun::list::List
- fun::list::Nil
- fun::natc::Addc
- fun::natc::Mulc
- fun::natc::Sc
- fun::natp::Add
- fun::natp::Even
- fun::natp::IsZero
- fun::natp::Mul
- fun::natp::Odd
- fun::natp::One
- fun::natp::Succ
- fun::natp::Two
- fun::phott::IsContr
- fun::phott::IsGroupoid
- fun::phott::IsHProp
- fun::phott::IsNGroupoid
- fun::phott::IsProp
- fun::phott::IsSet
- fun::real::AddReal
- fun::real::AddRealLam
- fun::real::AddRealTy
- fun::real::Aleph0Real
- fun::real::Aleph0RealLam
- fun::real::Aleph0RealTy
- fun::real::RealDef
- fun::real::RealRange
- hooo::Exists
- hooo::Para
- hooo::Pow
- hooo::PowEq
- hooo::Tauto
- hooo::Theory
- hooo::Uniform
- hott::IsContr
- hott::IsGroupoid
- hott::IsNGroupoid
- hott::IsProp
- hott::IsSet
- mid::Down
- mid::Mid
- mid::MidCatuskoti
- mid::Subordinate
- mid::Up
- mid::Virtual
- modal::NNPos
- modal::Nec
- modal::Pos
- modal::StrongPos
- nat::One
- nat::Three
- nat::Two
- nat::Zero
- path_semantics::Inc
- path_semantics::IncLevel
- path_semantics::LN
- path_semantics::Max
- path_semantics::MaxMax
- path_semantics::MaxMin
- path_semantics::Maxi
- path_semantics::Min
- path_semantics::MinMax
- path_semantics::MinMin
- path_semantics::Mixi
- path_semantics::Normalise
- path_semantics::PAndFst
- path_semantics::PAndSnd
- path_semantics::POrFst
- path_semantics::POrSnd
- path_semantics::PSem
- path_semantics::PSemNaive
- path_semantics::PSemNaiveNorm
- path_semantics::PSemTy
- path_semantics::PSemTyImply
- path_semantics::ty::Ty
- quality::Aq
- quality::EqAq
- quality::EqQ
- quality::Q
- quality::Seshatic
- qubit::Qu
- sd::Sd
- univalence::EqUniv
- univalence::Hom
- univalence::HomEq
- univalence::HomEq2
- univalence::HomEq3
- univalence::Univ