truncation in nLab

propositionsetobjecttype predicatefamily of setsdisplay morphismdependent type proofelementgeneralized elementterm/program cut rulecomposition of classifying morphisms / pullback of display mapssubstitution introduction rule for implicationcounit for hom-tensor adjunctionlambda elimination rule for implicationunit for hom-tensor adjunctionapplication cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type falseempty setinitial objectempty type proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition logical conjunctioncartesian productproductproduct type disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of) implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition) negationfunction set into empty setinternal hom into initial objectfunction type into empty type universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions) existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of) logical equivalencebijection setobject of isomorphismsequivalence type support setsupport object/(-1)-truncationpropositional truncation/bracket type n-image of morphism into terminal object/n-truncationn-truncation modality equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation equivalence class/quotient setquotientquotient type inductioncolimitinductive type, W-type, M-type higher inductionhigher colimithigher inductive type -0-truncated higher colimitquotient inductive type coinductionlimitcoinductive type presettype without identity types set of truth valuessubobject classifiertype of propositions domain of discourseuniverseobject classifiertype universe modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science) linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation proof netstring diagramquantum circuit (absence of) contraction rule(absence of) diagonalno-cloning theorem synthetic mathematicsdomain specific embedded programming language