TypeVec

Statistics

Metric	Count
Definitions `«term_⊗'_»`, `«term_⊗_»`, `«term_⊚_»`, `«term_⟹_»`, `TypeVec`, `inhabited`, `mp`, `mpr`, `inhabited`, `PredLast`, `PredLast'`, `RelLast`, `RelLast'`, `Subtype_`, `append1`, `append1Cases`, `appendFun`, `casesCons`, `casesNil`, `comp`, `const`, `diagSub`, `drop`, `dropFun`, `dropRepeat`, `fromAppend1DropLast`, `id`, `last`, `inhabited`, `lastFun`, `nilFun`, `ofRepeat`, `ofSubtype`, `ofSubtype'`, `prod`, `diag`, `fst`, `map`, `mk`, `snd`, `repeat`, `repeatEq`, `splitFun`, `subtypeVal`, `toAppend1DropLast`, `toSubtype`, `toSubtype'`, `typevecCasesCons₂`, `typevecCasesCons₃`, `typevecCasesNil₂`, `typevecCasesNil₃`, `«term_:::__1»`, `«term_:::_»`, `instInhabitedTypeVec`	54
Theorems `ext`, `ext_iff`, `append1_cases_append1`, `append1_drop_last`, `appendFun_aux`, `appendFun_comp`, `appendFun_comp'`, `appendFun_comp_id`, `appendFun_comp_splitFun`, `appendFun_id_id`, `appendFun_inj`, `append_prod_appendFun`, `casesCons_append1`, `casesNil_append1`, `comp_assoc`, `comp_id`, `const_append1`, `const_iff_true`, `const_nil`, `diag_sub_val`, `dropFun_RelLast'`, `dropFun_appendFun`, `dropFun_comp`, `dropFun_diag`, `dropFun_from_append1_drop_last`, `dropFun_id`, `dropFun_of_subtype`, `dropFun_prod`, `dropFun_splitFun`, `dropFun_subtypeVal`, `dropFun_toSubtype`, `drop_append1`, `drop_append1'`, `eq_nilFun`, `eq_of_drop_last_eq`, `fst_diag`, `fst_prod_mk`, `id_comp`, `id_eq_nilFun`, `lastFun_appendFun`, `lastFun_comp`, `lastFun_from_append1_drop_last`, `lastFun_of_subtype`, `lastFun_prod`, `lastFun_splitFun`, `lastFun_subtypeVal`, `lastFun_toSubtype`, `last_append1`, `nilFun_comp`, `prod_fst_mk`, `prod_id`, `prod_map_id`, `prod_snd_mk`, `repeatEq_iff_eq`, `repeat_eq_append1`, `repeat_eq_nil`, `snd_diag`, `snd_prod_mk`, `splitFun_comp`, `splitFun_inj`, `split_dropFun_lastFun`, `subsingleton0`, `subtypeVal_nil`, `subtypeVal_toSubtype`, `subtypeVal_toSubtype'`, `toSubtype'_of_subtype'`, `toSubtype_of_subtype`, `toSubtype_of_subtype_assoc`, `typevecCasesCons₂_appendFun`, `typevecCasesNil₂_appendFun`	70
Total	124

MvFunctor

Definitions

Name	Category	Theorems
`«term_⊗'_»` 📖	CompOp	—
`«term_⊗_»` 📖	CompOp	—
`«term_⊚_»` 📖	CompOp	—
`«term_⟹_»` 📖	CompOp	—

TypeVec

Definitions

Name	Category	Theorems
`PredLast` 📖	MathDef	1 math math: `MvFunctor.LiftP_PredLast_iff`
`PredLast'` 📖	CompOp	1 math math: `MvFunctor.LiftP_PredLast_iff`
`RelLast` 📖	MathDef	1 math math: `MvFunctor.LiftR_RelLast_iff`
`RelLast'` 📖	CompOp	4 math math: `MvQPF.liftR_map_last'`, `MvFunctor.LiftR_RelLast_iff`, `MvQPF.liftR_map_last`, `dropFun_RelLast'`
`Subtype_` 📖	CompOp	15 math math: `lastFun_toSubtype`, `toSubtype_of_subtype_assoc`, `toSubtype_of_subtype`, `dropFun_of_subtype`, `lastFun_subtypeVal`, `dropFun_subtypeVal`, `lastFun_of_subtype`, `subtypeVal_nil`, `MvFunctor.LiftP_def`, `MvFunctor.LiftR_def`, `toSubtype'_of_subtype'`, `diag_sub_val`, `dropFun_toSubtype`, `subtypeVal_toSubtype`, `subtypeVal_toSubtype'`
`append1` 📖	CompOp	38 math math: `MvQPF.liftR_map_last'`, `dropFun_from_append1_drop_last`, `MvFunctor.LiftR_RelLast_iff`, `lastFun_from_append1_drop_last`, `append1_cases_append1`, `appendFun_aux`, `MvPFunctor.wDest'_wMk`, `MvQPF.Fix.ind_aux`, `MvQPF.liftR_map_last`, `MvQPF.Cofix.dest_corec'`, `MvQPF.recF_eq'`, `appendFun_comp`, `MvQPF.Cofix.dest_corec`, `dropFun_RelLast'`, `append1_drop_last`, `drop_append1`, `last_append1`, `dropFun_appendFun`, `const_append1`, `MvPFunctor.M.dest_map`, `MvPFunctor.M.dest_corec`, `MvQPF.corec_roll`, `lastFun_appendFun`, `MvPFunctor.map_objAppend1`, `MvQPF.wrepr_wMk`, `MvPFunctor.M.dest_corec'`, `append_prod_appendFun`, `appendFun_comp_splitFun`, `MvQPF.corecF_eq`, `drop_append1'`, `MvQPF.recF_eq`, `appendFun_comp_id`, `MvFunctor.LiftP_PredLast_iff`, `repeat_eq_append1`, `casesCons_append1`, `MvQPF.Fix.rec_eq`, `appendFun_comp'`, `appendFun_id_id`
`append1Cases` 📖	CompOp	1 math math: `append1_cases_append1`
`appendFun` 📖	CompOp	23 math math: `MvQPF.liftR_map_last'`, `typevecCasesCons₂_appendFun`, `appendFun_aux`, `MvQPF.liftR_map_last`, `MvQPF.Cofix.dest_corec'`, `MvQPF.recF_eq'`, `appendFun_comp`, `MvQPF.Cofix.dest_corec`, `dropFun_appendFun`, `const_append1`, `MvPFunctor.M.dest_map`, `MvPFunctor.M.dest_corec`, `MvQPF.corec_roll`, `lastFun_appendFun`, `MvPFunctor.map_objAppend1`, `MvQPF.wrepr_wMk`, `append_prod_appendFun`, `appendFun_comp_splitFun`, `MvQPF.corecF_eq`, `appendFun_comp_id`, `MvQPF.Fix.rec_eq`, `appendFun_comp'`, `appendFun_id_id`
`casesCons` 📖	CompOp	1 math math: `casesCons_append1`
`casesNil` 📖	CompOp	1 math math: `casesNil_append1`
`comp` 📖	CompOp	30 math math: `toSubtype_of_subtype_assoc`, `toSubtype_of_subtype`, `LawfulMvFunctor.comp_map`, `lastFun_comp`, `MvQPF.comp_map`, `nilFun_comp`, `fst_prod_mk`, `MvPFunctor.w_map_wMk`, `appendFun_comp`, `MvPFunctor.map_eq`, `dropFun_comp`, `MvPFunctor.comp_map`, `MvPFunctor.comp_wPathCasesOn`, `splitFun_comp`, `MvFunctor.LiftR_def`, `comp_id`, `snd_diag`, `comp_assoc`, `MvPFunctor.map_objAppend1`, `toSubtype'_of_subtype'`, `id_comp`, `diag_sub_val`, `appendFun_comp_splitFun`, `fst_diag`, `appendFun_comp_id`, `subtypeVal_toSubtype`, `snd_prod_mk`, `MvFunctor.map_map`, `subtypeVal_toSubtype'`, `appendFun_comp'`
`const` 📖	CompOp	3 math math: `const_iff_true`, `const_append1`, `const_nil`
`diagSub` 📖	CompOp	1 math math: `diag_sub_val`
`drop` 📖	CompOp	14 math math: `dropFun_from_append1_drop_last`, `dropFun_of_subtype`, `dropFun_prod`, `lastFun_from_append1_drop_last`, `appendFun_aux`, `dropFun_diag`, `dropFun_subtypeVal`, `dropFun_comp`, `append1_drop_last`, `splitFun_comp`, `drop_append1`, `appendFun_comp_splitFun`, `drop_append1'`, `dropFun_id`
`dropFun` 📖	CompOp	13 math math: `dropFun_splitFun`, `dropFun_from_append1_drop_last`, `dropFun_of_subtype`, `dropFun_prod`, `appendFun_aux`, `dropFun_diag`, `dropFun_subtypeVal`, `dropFun_comp`, `dropFun_RelLast'`, `dropFun_appendFun`, `split_dropFun_lastFun`, `dropFun_toSubtype`, `dropFun_id`
`dropRepeat` 📖	CompOp	—
`fromAppend1DropLast` 📖	CompOp	2 math math: `dropFun_from_append1_drop_last`, `lastFun_from_append1_drop_last`
`id` 📖	CompOp	27 math math: `MvPFunctor.id_map`, `LawfulMvFunctor.id_map`, `MvQPF.liftR_map_last'`, `toSubtype_of_subtype`, `dropFun_from_append1_drop_last`, `MvFunctor.id_map`, `MvQPF.liftR_map_last`, `MvQPF.Cofix.dest_corec'`, `id_eq_nilFun`, `MvQPF.recF_eq'`, `MvQPF.Cofix.dest_corec`, `prod_id`, `MvPFunctor.M.dest_corec`, `comp_id`, `MvQPF.corec_roll`, `snd_diag`, `MvQPF.id_map`, `prod_map_id`, `MvQPF.wrepr_wMk`, `toSubtype'_of_subtype'`, `id_comp`, `MvQPF.corecF_eq`, `dropFun_id`, `fst_diag`, `appendFun_comp_id`, `MvQPF.Fix.rec_eq`, `appendFun_id_id`
`last` 📖	CompOp	14 math math: `lastFun_toSubtype`, `dropFun_from_append1_drop_last`, `lastFun_comp`, `lastFun_from_append1_drop_last`, `appendFun_aux`, `lastFun_of_subtype`, `lastFun_prod`, `append1_drop_last`, `splitFun_comp`, `last_append1`, `MvPFunctor.M.dest_corec'`, `appendFun_comp_splitFun`, `MvQPF.recF_eq`, `repeat_eq_append1`
`lastFun` 📖	CompOp	10 math math: `lastFun_toSubtype`, `lastFun_comp`, `lastFun_splitFun`, `lastFun_subtypeVal`, `lastFun_from_append1_drop_last`, `appendFun_aux`, `lastFun_of_subtype`, `lastFun_prod`, `lastFun_appendFun`, `split_dropFun_lastFun`
`nilFun` 📖	CompOp	7 math math: `eq_nilFun`, `nilFun_comp`, `repeat_eq_nil`, `subtypeVal_nil`, `typevecCasesNil₂_appendFun`, `id_eq_nilFun`, `const_nil`
`ofRepeat` 📖	CompOp	11 math math: `lastFun_toSubtype`, `toSubtype_of_subtype_assoc`, `toSubtype_of_subtype`, `dropFun_of_subtype`, `lastFun_of_subtype`, `const_iff_true`, `repeatEq_iff_eq`, `toSubtype'_of_subtype'`, `dropFun_toSubtype`, `subtypeVal_toSubtype`, `subtypeVal_toSubtype'`
`ofSubtype` 📖	CompOp	4 math math: `toSubtype_of_subtype_assoc`, `toSubtype_of_subtype`, `dropFun_of_subtype`, `lastFun_of_subtype`
`ofSubtype'` 📖	CompOp	1 math math: `toSubtype'_of_subtype'`
`prod` 📖	CompOp	17 math math: `dropFun_prod`, `repeat_eq_nil`, `dropFun_diag`, `lastFun_prod`, `fst_prod_mk`, `dropFun_RelLast'`, `prod_id`, `MvFunctor.LiftR_def`, `snd_diag`, `prod_map_id`, `toSubtype'_of_subtype'`, `append_prod_appendFun`, `diag_sub_val`, `fst_diag`, `repeat_eq_append1`, `snd_prod_mk`, `subtypeVal_toSubtype'`
`repeat` 📖	CompOp	7 math math: `dropFun_of_subtype`, `repeat_eq_nil`, `dropFun_subtypeVal`, `dropFun_RelLast'`, `const_append1`, `const_nil`, `repeat_eq_append1`
`repeatEq` 📖	CompOp	5 math math: `repeat_eq_nil`, `dropFun_RelLast'`, `repeatEq_iff_eq`, `diag_sub_val`, `repeat_eq_append1`
`splitFun` 📖	CompOp	9 math math: `dropFun_splitFun`, `lastFun_splitFun`, `MvPFunctor.wDest'_wMk`, `splitFun_comp`, `MvPFunctor.M.dest_corec'`, `split_dropFun_lastFun`, `appendFun_comp_splitFun`, `MvQPF.recF_eq`, `repeat_eq_append1`
`subtypeVal` 📖	CompOp	8 math math: `lastFun_subtypeVal`, `dropFun_subtypeVal`, `subtypeVal_nil`, `MvFunctor.LiftP_def`, `MvFunctor.LiftR_def`, `diag_sub_val`, `subtypeVal_toSubtype`, `subtypeVal_toSubtype'`
`toAppend1DropLast` 📖	CompOp	—
`toSubtype` 📖	CompOp	5 math math: `lastFun_toSubtype`, `toSubtype_of_subtype_assoc`, `toSubtype_of_subtype`, `dropFun_toSubtype`, `subtypeVal_toSubtype`
`toSubtype'` 📖	CompOp	2 math math: `toSubtype'_of_subtype'`, `subtypeVal_toSubtype'`
`typevecCasesCons₂` 📖	CompOp	1 math math: `typevecCasesCons₂_appendFun`
`typevecCasesCons₃` 📖	CompOp	—
`typevecCasesNil₂` 📖	CompOp	1 math math: `typevecCasesNil₂_appendFun`
`typevecCasesNil₃` 📖	CompOp	—
`«term_:::__1»` 📖	CompOp	—
`«term_:::_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`append1_cases_append1` 📖	mathematical	—	`append1Cases` `append1`	—	—
`append1_drop_last` 📖	mathematical	—	`append1` `drop` `last`	—	—
`appendFun_aux` 📖	mathematical	—	`appendFun` `drop` `append1` `last` `dropFun` `lastFun`	—	`eq_of_drop_last_eq`
`appendFun_comp` 📖	mathematical	—	`appendFun` `comp` `append1`	—	`eq_of_drop_last_eq`
`appendFun_comp'` 📖	mathematical	—	`comp` `append1` `appendFun`	—	`eq_of_drop_last_eq`
`appendFun_comp_id` 📖	mathematical	—	`appendFun` `id` `comp` `append1`	—	`eq_of_drop_last_eq`
`appendFun_comp_splitFun` 📖	mathematical	—	`comp` `append1` `appendFun` `splitFun` `drop` `last`	—	`splitFun_comp`
`appendFun_id_id` 📖	mathematical	—	`appendFun` `id` `append1`	—	`eq_of_drop_last_eq`
`appendFun_inj` 📖	—	`appendFun`	—	—	—
`append_prod_appendFun` 📖	mathematical	—	`appendFun` `prod` `prod.map` `append1`	—	`Arrow.ext`
`casesCons_append1` 📖	mathematical	—	`casesCons` `append1`	—	—
`casesNil_append1` 📖	mathematical	—	`casesNil` `Fin2.elim0`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	—
`const_append1` 📖	mathematical	—	`const` `append1` `appendFun` `repeat`	—	`Arrow.ext`
`const_iff_true` 📖	mathematical	—	`ofRepeat` `const`	—	`const.eq_1`
`const_nil` 📖	mathematical	—	`const` `nilFun` `repeat`	—	`Arrow.ext`
`diag_sub_val` 📖	mathematical	—	`comp` `Subtype_` `prod` `repeatEq` `subtypeVal` `diagSub` `prod.diag`	—	`Arrow.ext`
`dropFun_RelLast'` 📖	mathematical	—	`dropFun` `prod` `append1` `repeat` `RelLast'` `repeatEq`	—	—
`dropFun_appendFun` 📖	mathematical	—	`dropFun` `append1` `appendFun`	—	—
`dropFun_comp` 📖	mathematical	—	`dropFun` `comp` `drop`	—	—
`dropFun_diag` 📖	mathematical	—	`dropFun` `prod` `prod.diag` `drop`	—	—
`dropFun_from_append1_drop_last` 📖	mathematical	—	`dropFun` `append1` `drop` `last` `fromAppend1DropLast` `id`	—	—
`dropFun_id` 📖	mathematical	—	`dropFun` `id` `drop`	—	—
`dropFun_of_subtype` 📖	mathematical	—	`dropFun` `Subtype_` `ofRepeat` `ofSubtype` `drop` `repeat`	—	—
`dropFun_prod` 📖	mathematical	—	`dropFun` `prod` `prod.map` `drop`	—	—
`dropFun_splitFun` 📖	mathematical	—	`dropFun` `splitFun`	—	—
`dropFun_subtypeVal` 📖	mathematical	—	`dropFun` `Subtype_` `subtypeVal` `drop` `repeat`	—	—
`dropFun_toSubtype` 📖	mathematical	—	`dropFun` `ofRepeat` `Subtype_` `toSubtype` `Fin2.fs`	—	—
`drop_append1` 📖	mathematical	—	`drop` `append1`	—	—
`drop_append1'` 📖	mathematical	—	`drop` `append1`	—	`drop_append1`
`eq_nilFun` 📖	mathematical	—	`nilFun`	—	`Arrow.ext`
`eq_of_drop_last_eq` 📖	—	`dropFun` `lastFun`	—	—	—
`fst_diag` 📖	mathematical	—	`comp` `prod` `prod.fst` `prod.diag` `id`	—	—
`fst_prod_mk` 📖	mathematical	—	`comp` `prod` `prod.fst` `prod.map`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	—
`id_eq_nilFun` 📖	mathematical	—	`id` `nilFun`	—	`Arrow.ext`
`lastFun_appendFun` 📖	mathematical	—	`lastFun` `append1` `appendFun`	—	—
`lastFun_comp` 📖	mathematical	—	`lastFun` `comp` `last`	—	—
`lastFun_from_append1_drop_last` 📖	mathematical	—	`lastFun` `append1` `drop` `last` `fromAppend1DropLast`	—	—
`lastFun_of_subtype` 📖	mathematical	—	`lastFun` `Subtype_` `ofRepeat` `ofSubtype` `last`	—	—
`lastFun_prod` 📖	mathematical	—	`lastFun` `prod` `prod.map` `last`	—	—
`lastFun_splitFun` 📖	mathematical	—	`lastFun` `splitFun`	—	—
`lastFun_subtypeVal` 📖	mathematical	—	`lastFun` `Subtype_` `subtypeVal` `Fin2.fz`	—	—
`lastFun_toSubtype` 📖	mathematical	—	`lastFun` `ofRepeat` `Subtype_` `toSubtype` `last`	—	—
`last_append1` 📖	mathematical	—	`last` `append1`	—	—
`nilFun_comp` 📖	mathematical	—	`comp` `Fin2.elim0` `nilFun`	—	—
`prod_fst_mk` 📖	mathematical	—	`prod.fst`	—	—
`prod_id` 📖	mathematical	—	`prod.map` `id` `prod`	—	`Arrow.ext`
`prod_map_id` 📖	mathematical	—	`prod.map` `id` `prod`	—	`prod_id`
`prod_snd_mk` 📖	mathematical	—	`prod.snd`	—	—
`repeatEq_iff_eq` 📖	mathematical	—	`ofRepeat` `repeatEq`	—	`repeatEq.eq_2`
`repeat_eq_append1` 📖	mathematical	—	`repeatEq` `append1` `splitFun` `prod` `last` `repeat`	—	—
`repeat_eq_nil` 📖	mathematical	—	`repeatEq` `nilFun` `prod` `repeat`	—	`Arrow.ext`
`snd_diag` 📖	mathematical	—	`comp` `prod` `prod.snd` `prod.diag` `id`	—	—
`snd_prod_mk` 📖	mathematical	—	`comp` `prod` `prod.snd` `prod.map`	—	—
`splitFun_comp` 📖	mathematical	—	`splitFun` `comp` `drop` `last`	—	`eq_of_drop_last_eq`
`splitFun_inj` 📖	—	`splitFun`	—	—	`dropFun_splitFun` `lastFun_splitFun`
`split_dropFun_lastFun` 📖	mathematical	—	`splitFun` `dropFun` `lastFun`	—	`eq_of_drop_last_eq`
`subsingleton0` 📖	mathematical	—	`TypeVec`	—	—
`subtypeVal_nil` 📖	mathematical	—	`subtypeVal` `nilFun` `Subtype_`	—	—
`subtypeVal_toSubtype` 📖	mathematical	—	`comp` `ofRepeat` `Subtype_` `subtypeVal` `toSubtype`	—	`Arrow.ext`
`subtypeVal_toSubtype'` 📖	mathematical	—	`comp` `ofRepeat` `Subtype_` `prod` `subtypeVal` `toSubtype'`	—	`Arrow.ext`
`toSubtype'_of_subtype'` 📖	mathematical	—	`comp` `Subtype_` `prod` `ofRepeat` `toSubtype'` `ofSubtype'` `id`	—	`Arrow.ext` `Subtype.coe_eta`
`toSubtype_of_subtype` 📖	mathematical	—	`comp` `Subtype_` `ofRepeat` `toSubtype` `ofSubtype` `id`	—	`Arrow.ext`
`toSubtype_of_subtype_assoc` 📖	mathematical	—	`comp` `ofRepeat` `Subtype_` `toSubtype` `ofSubtype`	—	`comp_assoc` `toSubtype_of_subtype`
`typevecCasesCons₂_appendFun` 📖	mathematical	—	`typevecCasesCons₂` `appendFun`	—	—
`typevecCasesNil₂_appendFun` 📖	mathematical	—	`typevecCasesNil₂` `nilFun` `Fin2.elim0`	—	—

TypeVec.Arrow

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—
`mp` 📖	CompOp	—
`mpr` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	—	—	—	—
`ext_iff` 📖	—	—	—	—	`ext`

TypeVec.Curry

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—

TypeVec.last

Definitions

Name	Category	Theorems
`inhabited` 📖	CompOp	—

TypeVec.prod

Definitions

Name	Category	Theorems
`diag` 📖	CompOp	4 math math: `TypeVec.dropFun_diag`, `TypeVec.snd_diag`, `TypeVec.diag_sub_val`, `TypeVec.fst_diag`
`fst` 📖	CompOp	4 math math: `TypeVec.fst_prod_mk`, `TypeVec.prod_fst_mk`, `MvFunctor.LiftR_def`, `TypeVec.fst_diag`
`map` 📖	CompOp	7 math math: `TypeVec.dropFun_prod`, `TypeVec.lastFun_prod`, `TypeVec.fst_prod_mk`, `TypeVec.prod_id`, `TypeVec.prod_map_id`, `TypeVec.append_prod_appendFun`, `TypeVec.snd_prod_mk`
`mk` 📖	CompOp	—
`snd` 📖	CompOp	4 math math: `MvFunctor.LiftR_def`, `TypeVec.snd_diag`, `TypeVec.prod_snd_mk`, `TypeVec.snd_prod_mk`

(root)

Definitions

Name	Category	Theorems
`TypeVec` 📖	CompOp	1 math math: `TypeVec.subsingleton0`
`instInhabitedTypeVec` 📖	CompOp	—

---

← Back to Index