Сергей Орлов (os80) wrote in category_theory,
Сергей Орлов
os80
category_theory

Вопросы про identity types

Коллеги, может быть, вопрос не совсем в тему сообщества, но куда задать вопрос по теории типов — не знаю.
А так как началось всё с HoTT, про которую узнал тут, решил здесь и спросить.

Никак не могу понять, что такое identity types, которые "b =A c".
1. Может ли кто-то понятно объяснить с конкретными примерами, что это такое?
2. Знает ли кто-нибудь хороший paper на эту тему?
3. Читаю "Martin-Löf's Type Theory" by Nordström et al. Там на 8-й странице (вторая снизу формула) делается следующее утверждение: если a∈A, то a=a∈A. С учётом написанного там ранее, это у меня интерпретируется как "если 1 принадлежит натуральным числам, то доказательство того, что 1=1 тоже принадлежит натуральным числам". Но это же бред, товарищи, в каком месте я не прав?
Tags: beginners
Subscribe
  • Post a new comment

    Error

    default userpic

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 16 comments