1:31:42Agda Lecture 1: Introduction to Agda, dependent types and functions -- HoTTEST Summer School 2022
Intro
A 92-minute video from HoTTEST: “Agda Lecture 1: Introduction to Agda, dependent types and functions -- HoTTEST Summer School 2022”.
HoTTEST
2.89K subscribers on YouTube
Shorts, livestreams, trailers and promos are never listed. Unless a curator approved this channel in full, only individually picked videos appear.
1:31:42
1:41:54Agda Lecture 2: Basic MLTT Types -- HoTTEST Summer School 2022
A 102-minute video from HoTTEST: “Agda Lecture 2: Basic MLTT Types -- HoTTEST Summer School 2022”.
1:32:02Agda Lecture 3: Identity types, Σ-types & universes -- HoTTEST Summer School 2022
Advanced
A 92-minute video from HoTTEST: “Agda Lecture 3: Identity types, Σ-types & universes -- HoTTEST Summer School 2022”.
1:34:21Agda Lecture 6: Calculating the fundamental group of the circle -- HoTTEST Summer School 2022
Advanced
A 94-minute video from HoTTEST: “Agda Lecture 6: Calculating the fundamental group of the circle -- HoTTEST Summer School 2022”.
1:34:12Agda Lecture 7: Cubical Agda - an introduction -- HoTTEST Summer School 2022
Advanced
A 94-minute video from HoTTEST: “Agda Lecture 7: Cubical Agda - an introduction -- HoTTEST Summer School 2022”.
1:33:27Agda Lecture 8: Quotients and Higher Inductive Types in Cubical Agda -- HoTTEST Summer School 2022
Advanced
A 93-minute video from HoTTEST: “Agda Lecture 8: Quotients and Higher Inductive Types in Cubical Agda -- HoTTEST Summer School 2022”.
1:27:31Agda Lecture 9: Homogeneous composition and cubical univalence -- HoTTEST Summer School 2022
Advanced
A 88-minute video from HoTTEST: “Agda Lecture 9: Homogeneous composition and cubical univalence -- HoTTEST Summer School 2022”.
1:08:46Agda Problem Session 1: Introduction to Agda, types & functions (Astra) - HoTTEST Summer School 2022
A 69-minute video from HoTTEST: “Agda Problem Session 1: Introduction to Agda, types & functions (Astra) - HoTTEST Summer School 2022”.
58:24Agda Problem Session 1: Introduction to Agda, types & functions (Tom) -- HoTTEST Summer School 2022
Intro
A 58-minute video from HoTTEST: “Agda Problem Session 1: Introduction to Agda, types & functions (Tom) -- HoTTEST Summer School 2022”.
1:00:37Agda Problem Session 2: Basic MLTT Types (Astra) -- HoTTEST Summer School 2022
A 61-minute video from HoTTEST: “Agda Problem Session 2: Basic MLTT Types (Astra) -- HoTTEST Summer School 2022”.
1:05:02Agda Problem Session 2: Basic MLTT Types (Max) -- HoTTEST Summer School 2022
A 65-minute video from HoTTEST: “Agda Problem Session 2: Basic MLTT Types (Max) -- HoTTEST Summer School 2022”.
1:08:34Agda Problem Session 3: Identity types, Σ-types & universes (Astra) -- HoTTEST Summer School 2022
Advanced
A 69-minute video from HoTTEST: “Agda Problem Session 3: Identity types, Σ-types & universes (Astra) -- HoTTEST Summer School 2022”.
47:25Agda Problem Session 3: Identity types, Σ-types & universes (Johannes) -- HoTTEST Summer School 2022
Advanced
A 47-minute video from HoTTEST: “Agda Problem Session 3: Identity types, Σ-types & universes (Johannes) -- HoTTEST Summer School 2022”.
56:04Agda Problem Session 6: The fundamental group of the circle (Astra) -- HoTTEST Summer School 2022
Advanced
A 56-minute video from HoTTEST: “Agda Problem Session 6: The fundamental group of the circle (Astra) -- HoTTEST Summer School 2022”.
1:09:37Agda Problem Session 6: The fundamental group of the circle (Elisabeth) - HoTTEST Summer School 2022
Advanced
A 70-minute video from HoTTEST: “Agda Problem Session 6: The fundamental group of the circle (Elisabeth) - HoTTEST Summer School 2022”.
1:06:02Agda Problem Session 7: Cubical Agda - an introduction (Astra) -- HoTTEST Summer School 2022
Advanced
A 66-minute video from HoTTEST: “Agda Problem Session 7: Cubical Agda - an introduction (Astra) -- HoTTEST Summer School 2022”.
1:45:56Agda Problem Session 7: Cubical Agda - an introduction (Max) -- HoTTEST Summer School 2022
Advanced
A 106-minute video from HoTTEST: “Agda Problem Session 7: Cubical Agda - an introduction (Max) -- HoTTEST Summer School 2022”.
1:14:26Agda Problem Session 8: Quotients and Higher Inductive Types (Astra) -- HoTTEST Summer School 2022
Advanced
A 74-minute video from HoTTEST: “Agda Problem Session 8: Quotients and Higher Inductive Types (Astra) -- HoTTEST Summer School 2022”.
1:35:20Agda Problem Session 8: Quotients and Higher Inductive Types (Max)
Advanced
A 95-minute video from HoTTEST: “Agda Problem Session 8: Quotients and Higher Inductive Types (Max)”.
1:09:29Agda Problem Session 9: Homogeneous comp. & cubical univalence (Astra) -- HoTTEST Summer School 2022
A 69-minute video from HoTTEST: “Agda Problem Session 9: Homogeneous comp. & cubical univalence (Astra) -- HoTTEST Summer School 2022”.
1:46:25Agda Problem Session 9: Homogeneous comp. & cubical univalence (Axel) -- HoTTEST Summer School 2022
A 106-minute video from HoTTEST: “Agda Problem Session 9: Homogeneous comp. & cubical univalence (Axel) -- HoTTEST Summer School 2022”.
1:14:56Ambrus Kaposi, Quotient inductive-inductive types and higher friends
Advanced
A 75-minute video from HoTTEST: “Ambrus Kaposi, Quotient inductive-inductive types and higher friends”.
25:44Amélia Liao, Univalent Category Theory
Advanced
A 26-minute video from HoTTEST: “Amélia Liao, Univalent Category Theory”.
59:26Anders Mörtberg, Unifying cubical models of homotopy type theory
Advanced
A 59-minute video from HoTTEST: “Anders Mörtberg, Unifying cubical models of homotopy type theory”.
1:07:01Andrea Vezzosi, Cubical Agda and its extensions
Advanced
A 67-minute video from HoTTEST: “Andrea Vezzosi, Cubical Agda and its extensions”.
1:12:18Andreas Nuyts, Higher pro-arrows: Towards a model for naturality pretype theory
Advanced
A 72-minute video from HoTTEST: “Andreas Nuyts, Higher pro-arrows: Towards a model for naturality pretype theory”.
1:30:18Andrej Bauer, General type theories
Advanced
A 90-minute video from HoTTEST: “Andrej Bauer, General type theories”.
1:23:43Andrew Pitts, Axiomatizing cubical sets models of univalent foundations
Advanced
A 84-minute video from HoTTEST: “Andrew Pitts, Axiomatizing cubical sets models of univalent foundations”.
1:13:13Andrew Swan, Choice, collection and covering in cubical sets
A 73-minute video from HoTTEST: “Andrew Swan, Choice, collection and covering in cubical sets”.
1:16:25Andrew Swan, Double negation stable h-propositions in cubical sets
A 76-minute video from HoTTEST: “Andrew Swan, Double negation stable h-propositions in cubical sets”.
26:35Andrew Swan, Why cubical sets are different to simplicial sets
Advanced
A 27-minute video from HoTTEST: “Andrew Swan, Why cubical sets are different to simplicial sets”.
1:07:18Anja Petković, Equality checking for finitary type theories
Advanced
A 67-minute video from HoTTEST: “Anja Petković, Equality checking for finitary type theories”.
1:21:32Astra Kolomatskaia, Displayed Type Theory: indexed modalities and analytic higher structures
Advanced
A 82-minute video from HoTTEST: “Astra Kolomatskaia, Displayed Type Theory: indexed modalities and analytic higher structures”.
31:19Astra Kolomatskaia, Semi-simplicial types
Advanced
A 31-minute video from HoTTEST: “Astra Kolomatskaia, Semi-simplicial types”.
1:15:04Axel Ljungström, A formalisation of the Serre finiteness theorem
Advanced
A 75-minute video from HoTTEST: “Axel Ljungström, A formalisation of the Serre finiteness theorem”.
27:52Axel Ljungström, Calculating a Brunerie number
Advanced
A 28-minute video from HoTTEST: “Axel Ljungström, Calculating a Brunerie number”.