DefinitionsHasMulticoequalizer, HasMultiequalizer, desc, isoCoequalizer, multicofork, sigmaπ, π, Multicofork, desc, mk, ext, isColimitToLinearOrder, isoOfπ, ofLinearOrder, ofSigmaCofork, ofπ, toLinearOrder, toSigmaCofork, π, MulticospanIndex, fst, fstPiMap, fstPiMapOfIsLimit, left, multicospan, multiforkEquivPiFork, multiforkEquivPiForkOfIsLimit, multiforkOfParallelHomsEquivFork, ofParallelHoms, ofPiForkFunctor, parallelPairDiagram, parallelPairDiagramOfIsLimit, right, snd, sndPiMap, sndPiMapOfIsLimit, toPiForkFunctor, MulticospanShape, L, R, fst, prod, snd, isoEqualizer, multifork, ι, ιPi, Multifork, mk, ext, isLimitEquivOfIsos, isoOfι, ofPiFork, ofι, toPiFork, ι, MultispanIndex, SymmStruct, iso, fst, fstSigmaMap, fstSigmaMapOfIsColimit, left, multicoforkEquivSigmaCofork, multicoforkEquivSigmaCoforkOfIsColimit, multispan, ofSigmaCoforkFunctor, parallelPairDiagram, parallelPairDiagramOfIsColimit, right, snd, sndSigmaMap, sndSigmaMapOfIsColimit, toLinearOrder, toLinearOrderMultispanIso, toSigmaCoforkFunctor, MultispanShape, L, R, fst, ofLinearOrder, prod, snd, WalkingMulticospan, comp, functorExt, instInhabitedHom, instInhabitedOfL, instSmallCategory, WalkingMultispan, comp, arrowEquiv, equiv, functorExt, inclusionOfLinearOrder, instInhabitedHom, instInhabitedOfL, instSmallCategory, instUniqueHom, instUniqueLOfLinearOrderBool, multicoequalizer, multiequalizer | 102 |
Theoremscondition, condition_assoc, hom_ext, hom_ext_iff, instEpiSigmaπ, instHasCoequalizerFstSigmaMapSndSigmaMap, multicofork_ι_app_right, multicofork_ι_app_right', multicofork_π, ι_sigmaπ, ι_sigmaπ_assoc, π_desc, π_desc_assoc, fac, fac_assoc, hom_ext, mk_desc, condition, condition_assoc, ext_hom_hom, ext_inv_hom, fst_app_right, isoOfπ_hom_hom, isoOfπ_inv_hom, ofSigmaCofork_pt, ofSigmaCofork_ι_app_left, ofSigmaCofork_ι_app_right, ofSigmaCofork_ι_app_right', ofSigmaCofork_π, ofπ_pt, ofπ_ι_app, sigma_condition, sigma_condition_assoc, snd_app_right, snd_app_right_assoc, toSigmaCofork_pt, toSigmaCofork_π, π_comp_hom, π_comp_hom_assoc, π_eq_app_right, fstPiMapOfIsLimit_proj, fstPiMapOfIsLimit_proj_assoc, fstPiMap_π, fstPiMap_π_assoc, multicospan_map, multicospan_obj, multiforkEquivPiForkOfIsLimit_counitIso, multiforkEquivPiForkOfIsLimit_functor, multiforkEquivPiForkOfIsLimit_inverse, multiforkEquivPiForkOfIsLimit_unitIso, multiforkEquivPiFork_counitIso_hom_app_hom, multiforkEquivPiFork_counitIso_inv_app_hom, multiforkEquivPiFork_functor_map_hom, multiforkEquivPiFork_functor_obj_pt, multiforkEquivPiFork_functor_obj_π_app, multiforkEquivPiFork_inverse_map_hom, multiforkEquivPiFork_inverse_obj_pt, multiforkEquivPiFork_inverse_obj_π_app, multiforkEquivPiFork_unitIso_hom_app_hom, multiforkEquivPiFork_unitIso_inv_app_hom, multiforkOfParallelHomsEquivFork_functor_obj_ι, multiforkOfParallelHomsEquivFork_inverse_obj_ι, ofParallelHoms_fst, ofParallelHoms_left, ofParallelHoms_right, ofParallelHoms_snd, ofPiForkFunctor_map_hom, ofPiForkFunctor_obj, parallelPairDiagramOfIsLimit_map, parallelPairDiagramOfIsLimit_obj, parallelPairDiagram_map, parallelPairDiagram_obj, sndPiMapOfIsLimit_proj, sndPiMapOfIsLimit_proj_assoc, sndPiMap_π, sndPiMap_π_assoc, toPiForkFunctor_map_hom, toPiForkFunctor_obj, prod_L, prod_R, prod_fst, prod_snd, condition, condition_assoc, hom_ext, hom_ext_iff, instHasEqualizerFstPiMapSndPiMap, instMonoιPi, lift_ι, lift_ι_assoc, multifork_ι, multifork_π_app_left, ιPi_π, ιPi_π_assoc, fac, fac_assoc, hom_ext, mk_lift, app_left_eq_ι, app_right_eq_ι_comp_fst, app_right_eq_ι_comp_snd, app_right_eq_ι_comp_snd_assoc, condition, condition_assoc, ext_hom_hom, ext_inv_hom, hom_comp_ι, hom_comp_ι_assoc, isoOfι_hom_hom, isoOfι_inv_hom, ofPiFork_pt, ofPiFork_ι, ofPiFork_π_app_left, ofPiFork_π_app_right, ofι_pt, ofι_π_app, pi_condition, pi_condition_assoc, toPiFork_pt, toPiFork_π_app_one, toPiFork_π_app_zero, ι_ofι, fst_eq_snd, iso_hom_fst, iso_hom_fst_assoc, iso_hom_snd, iso_hom_snd_assoc, inj_fstSigmaMapOfIsColimit, inj_fstSigmaMapOfIsColimit_assoc, inj_sndSigmaMapOfIsColimit, inj_sndSigmaMapOfIsColimit_assoc, multicoforkEquivSigmaCoforkOfIsColimit_counitIso, multicoforkEquivSigmaCoforkOfIsColimit_functor, multicoforkEquivSigmaCoforkOfIsColimit_inverse, multicoforkEquivSigmaCoforkOfIsColimit_unitIso, multicoforkEquivSigmaCofork_counitIso_hom_app_hom, multicoforkEquivSigmaCofork_counitIso_inv_app_hom, multicoforkEquivSigmaCofork_functor_map_hom, multicoforkEquivSigmaCofork_functor_obj_pt, multicoforkEquivSigmaCofork_functor_obj_ι_app, multicoforkEquivSigmaCofork_inverse_map_hom, multicoforkEquivSigmaCofork_inverse_obj_pt, multicoforkEquivSigmaCofork_inverse_obj_ι_app, multicoforkEquivSigmaCofork_unitIso_hom_app_hom, multicoforkEquivSigmaCofork_unitIso_inv_app_hom, multispan_map_fst, multispan_map_snd, multispan_obj_left, multispan_obj_right, ofSigmaCoforkFunctor_map_hom, ofSigmaCoforkFunctor_obj, parallelPairDiagramOfIsColimit_map, parallelPairDiagramOfIsColimit_obj, toLinearOrderMultispanIso_hom_app, toLinearOrderMultispanIso_inv_app, toLinearOrder_fst, toLinearOrder_left, toLinearOrder_right, toLinearOrder_snd, toSigmaCoforkFunctor_map_hom, toSigmaCoforkFunctor_obj, ι_fstSigmaMap, ι_fstSigmaMap_assoc, ι_sndSigmaMap, ι_sndSigmaMap_assoc, ofLinearOrder_L, ofLinearOrder_R, ofLinearOrder_fst, ofLinearOrder_snd, prod_L, prod_R, prod_fst, prod_snd, comp_eq_comp, id_eq_id, functorExt_hom_app, functorExt_inv_app, comp_eq_comp, id_eq_id, functorExt_hom_app, functorExt_inv_app, inclusionOfLinearOrder_map, inclusionOfLinearOrder_obj, instIsEmptyHomRightLeft, instLocallySmall, instSmallOfLOfR, instSubsingletonHomLeft, instSubsingletonHomRight | 188 |