Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 25th 2017

    In section 3.5 of the HoTT book it considers

    P:A𝒰\mathbb ZP : A \to \mathcal{U} is a family of mere propositions

    and then forms the dependent sum (x:A)P(x)\sum_{(x:A)} P(x). Then as to whether to call this a subtype, it says

    We may also refer to PP itself as a subset or subtype of AA; this is actually more correct, since the type (3.5.2) [the dependent sum] in isolation doesn’t remember its relationship to AA.

    What does ’in isolation’ mean here? Can the dependent sum be given without information about how it has been constructed, and so then with its projection to AA?

    I’m looking at this as I’m still tweaking my ’the structure’ paper, and was thinking that many uses of ’the’ arise when a PP above gives rise to a singleton (or contractible) (x:A)P(x)\sum_{(x:A)} P(x).

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 26th 2017

    Well, once we construct the dependent sum, it is just a type. Remembering how it was constructed is tantamount to remembering PP itself or the projection to AA.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 26th 2017

    For instance, every element of a set defines a singleton subset of that set. But as sets in isolation, each singleton is isomorphic to each other singleton. It’s only when we consider them together with their predicates or inclusions to the original set that they are distinguishable.

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 26th 2017

    Ah good, thanks. That makes splendid contact with something that was said at the last Bristol conference on Philosophy and HoTT.

    Recall that idea of mine that we might try to make sense of ’the structure of AA’ as arising from a contractible type

    Structure of AA := (X:Type)Equiv(A,X)\sum_{(X: Type)} Equiv(A,X).

    The objection was raised that this entails that all ’Structure of X’s are identical as each is contractible.

    So I could have P:TypeTypeP: Type \to Type, P(X)=Equiv(A,X)P(X) = Equiv(A, X). The dependent sum from this is my ’Structure of AA’ and is contractible, hence we can introduce the element

    the structure of AA: Structure of AA.

    Returning to the ordinary language case of a singleton subtype. Say I have a type CatCat, and a predicate S(x)S(x) := Sitting on this mat(x)(x)’ which applies to only one cat. Then the dependent sum ’Cat sitting on the mat’ is a singleton, so a candidate for ’the introduction’.

    But maybe I’d be better off remembering the projection to CatCat and arrange things so that ’the cat sitting on the mat’ is in fact an element of CatCat rather than of CatsittingonthismatCat\;sitting\;on\;this\;mat.

    So a general rule for ’the introduction’ could be that when we have P:ATypeP: A \to Type and the dependent sum is contractible as witnessed by (a,b)(a, b), a:Aa: A and b:P(b)b:P(b) (along with proof pp that any other element in the dependent sum is equal to (a,b)(a, b), then

    the AA that is PP := a:Aa: A.

    In the Structure case, this would give me ’the structure of AA’ as an element of TypeType, and I can choose any type equivalent to AA.

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 26th 2017
    • (edited Feb 26th 2017)

    Considering, say, the predicate on cats of being black. When I say ’The cat sitting on this mat is black’ am I coercing along the projection from the dependent sum, or is ’the cat sitting on this mat’ already just a cat?

    Coercion is maybe quite common anyway, and I’m further mapping that cat to ObjectObject where Black is first defined.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 26th 2017

    Makes sense.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 26th 2017

    There probably isn’t a unique way to analyze any English sentence to decide which maps are coercions and which aren’t.