Videos on TYPE THEORY- 2020
lezione 1.
Motivation
lezione 2.
Origin
lezione 3.
Modern Origin
lezione 4.
Different meaning of type
lezione 5.
Examples of Types
lezione 6.
Judgements in Type theory
lezione 7.
Structural rules
lezione 8.
Singleton
lezione 9.
Sanitary checks
lezione 10.
schema generale regole tipi + regole di conservazione uguaglianza tipo singoletto
lezione 11.
Computability of judgements in type theory
lezione 12.
type of
the Natural Numbers
lezione 13 (prima parte)
esercizio somma di z con due per ricorsione
lezione 13.
(seconda parte)
esercizio: addizione per ricorsione
lezione 14
tipo delle liste di un tipo
lezione 15
tipo somma disgiunta binaria
lezione 16
esercizi su tipo uguaglianza proposizionale
lezione 17
tipo somma indiciata forte
lezione 19
usi del tipo somma indiciata per rappresentare assioma separazione e quantificazione esistenziale
addendum lezione 19
congiunzione come tipo prodotto cartesiano
lezione 20
tipo delle funzioni e tipo prodotto dipendente
addendum lezione 20
tipo vuoto
lezione 21
logic in Martin-Leof's type theory
lezione 22
principi di induzione dei tipi induttivi
esercizio
dimostrazione per induzione su addizione con zero
lezione 23.
tipo del primo universo
esercizio su universo:
zero diverso da uno proposizionalmente
lezione 24. 1.
peculiarita' della teoria di Martin-Loef (introduzione con def. di MLTT e frammenti)
lezione 24.2
Necessita' di un universo per formalizzare aritmetica
lezione 24.4
inconsistenza di MLTT con codice del primo universo in se stesso