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

Discussion Tag Cloud

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).

nLab > Latest Changes: dependent type

Bottom of Page

1 to 10 of 10

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeOct 25th 2017

    the entries dependent type and indexed set did not know of each other.

    I have now cross-linked them minimally in their “Related entries”-sections. But this would deserve to be expanded on for exposition…

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeMay 21st 2022
    • (edited May 21st 2022)

    made “type family” (requested elsewhere) redirect here

    diff, v18, current

  3. added a section on the relation between families of types, families of elements, and functions, and how that results in the relation between type theory and category theory inside of dependent type theory itself.

    Anonymous

    diff, v22, current

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeJan 21st 2023
    • (edited Jan 21st 2023)

    you wrote (here):

    Given a family of types, x:A⊢B(x)x:A \vdash B(x), one could construct a family of elements z:∑ x:AB(x)⊢π 1(z):Az:\sum_{x:A} B(x) \vdash \pi_1(z):A via the rules for dependent sum types. Conversely, given a family of elements x:A⊢f(x):Bx:A \vdash f(x):B one could construct a family of types y:B⊢∑ x:Af(x)= Byy:B \vdash \sum_{x:A} f(x) =_B y as the family of fiber types of x:A⊢f(x):Bx:A \vdash f(x):B.

    \,

    This seems confusing to the point of being notationally wrong.

    I guess you mean to talk about these two functions:

    ∑Y:Type(Y→X) ⟶ ∏x:XType (Y,f) ↦ (x:X⊢fib x(f)) \array{ \underset{ Y \,\colon\, Type }{\sum} \big( Y \to X \big) &\longrightarrow& \underset{x \,\colon\, X}{\prod} Type \\ (Y,f) &\mapsto& \big( x \colon X \;\vdash\; fib_x(f) \big) }

    and

    ∏x:XType ⟶ ∑Y:Type(Y→X) (x:X⊢E(x)) ↦ (π 1:(∑x:XE(x))→X) \array{ \underset{x \,\colon\, X}{\prod} Type &\longrightarrow& \underset{ Y \,\colon\, Type }{\sum} \big( Y \to X \big) \\ \big( x \,\colon\, X \;\;\vdash\;\; E(x) \big) &\mapsto& \Big( \pi_1 \,\colon\, \big( \underset{x \,:\, X}{\sum} E(x) \big) \to X \Big) }

    ?

    diff, v23, current

  5. no, I mean syntactically, not relative to a universe.

    Anonymous

    diff, v24, current

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeJan 21st 2023

    I see, I was misled by expecting to read something else.

    Do you mind if we write “one can” or “there is” instead of “one could”?

  7. one could -> one can

    Anonymous

    diff, v25, current

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeJan 21st 2023

    Thanks.

    In addition, I have taken the liberty of adding whitespace and parenthesis to the formulas (here) in order to optically resolve the syntax tree.

    diff, v26, current

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJan 25th 2023
    • (edited Jan 25th 2023)

    I have added (here) the analogous discussion reflected in a type universe, with a reference to Theorem 4.8.3 in the HoTT book.

    Then I added (here) a joint lead-in paragraph for this and the previous discussion

    diff, v27, current

  10. fixed incorrect citation

    Ebuka Akubilo

    diff, v32, current

1 to 10 of 10

  1.