Data.Relation.Binary.Subset.Propositional.Properties.filter⁺
foundation.homotopies._.compute-ind-htpy
foundation.equivalences.coh-unit-laws-equiv
foundation.functoriality-propositional-truncation.id-map-trunc-Prop
foundation.functoriality-coproduct-types._.equiv-mutually-exclusive-coprod
trees.polynomial-endofunctors.coh-refl-htpy-polynomial-endofunctor
foundation.uniqueness-image._.htpy-map-hom-equiv-slice-uniqueness-im
foundation.uniqueness-image._.tetrahedron-hom-equiv-slice-uniqueness-im
foundation.functoriality-set-truncation._.htpy-map-hom-slice-trunc-im-Set
foundation.functoriality-set-truncation._.tetrahedron-map-hom-slice-trunc-im-Set
univalent-combinatorics.2-element-types._.is-not-identity-swap-2-Element-Type
foundation.unordered-pairs._.eq-Eq-refl-unordered-pair
MGS.Equivalence-Induction.𝔾-≃-equation
MGS.More-FunExt-Consequences.EM-is-subsingleton
foundation.unordered-pairs.preserves-refl-htpy-unordered-pair
MGS.Equivalence-Constructions.Eq-Eq-cong
foundation.unordered-pairs.id-equiv-standard-unordered-pair
MGS.Embeddings.Emb→fun
trees.morphisms-algebras-polynomial-endofunctors._.refl-htpy-hom-algebra-polynomial-endofunctor
MGS.Universe-Lifting._.q
UF.Equiv-FunExt.prop-＝-≃-⇔
trees.morphisms-algebras-polynomial-endofunctors._.is-contr-total-htpy-hom-algebra-polynomial-endofunctor
trees.w-types.htpy-hom-𝕎-Alg
UF.FunExt-Properties.naive-funext-gives-funext₀
graph-theory.morphisms-undirected-graphs._.refl-htpy-hom-Undirected-Graph
UF.UA-FunExt._._.h
graph-theory.morphisms-undirected-graphs._.is-contr-total-htpy-hom-Undirected-Graph
UF.PairFun.pair-fun-embedding
graph-theory.equivalences-undirected-graphs._.edge-standard-unordered-pair-vertices-id-equiv-Undirected-Graph
UF.UniverseEmbedding.hSet-embeddings-are-embeddings
graph-theory.equivalences-undirected-graphs._.is-contr-total-htpy-equiv-Undirected-Graph
UF.Size._.Set-Replacement
Lifting.IdentityViaSIP.𝓛-Id
foundation.partitions._.is-section-map-inv-compute-block-partition
Lifting.IdentityViaSIP.𝓛-Id·
foundation.partitions._.is-retraction-map-inv-compute-block-partition
Lifting.Size._.e
foundation.partitions._.is-emb-inhabited-subtype-block-partition
InjectiveTypes.Blackboard.injective._.e
foundation.partitions._.compute-is-in-block-partition
foundation.partitions._.is-contr-block-containing-element-partition
foundation.partitions._.is-in-block-class-partition
foundation.partitions._.compute-total-block-partition
TypeTopology.SquashedCantor._.fg
foundation.partitions.partition-Set-Indexed-Σ-Decomposition
foundation.set-quotients._.is-section-equivalence-class-set-quotient
foundation.set-quotients._.is-retraction-equivalence-class-set-quotient