Egbert Rijke: Programming with the univalence axiom in Agda

Datum objave: 10. 6. 2022
Obvestilo vsem študentom FMF
torek
14
junij
Ura:
15.00
Lokacija:
Učilnica P.02 in na daljavo.
Računalniška delavnica.

When we formalize a concept in a proof assistant, we automatically obtain the type of all objects in that concept. For example, by defining groups we obtain the type of all groups, by defining trees we obtain the type of all trees, by defining partitions of a set we obtain the type of all of them, and so on. Once we define a concept, we are often interested in how many such objects there are of a given finite cardinality. In order to do this, we first have to figure out how to distinguish between such objects. The univalence axiom is useful here. The univalence axiom asserts that two equivalent types can be identified. This axiom is strong enough to immediately characterize the identity types of all objects in a concept. We will use this to construct some interesting combinatorial sequences.

Delavnica bo potekala v angleškem jeziku. Za delavnico si morate namestiti:

  • dokazovalnik Agda (različico 2.6.2) - navodila za namestitev lahko najdete med gradivi predmega [Logika v računalništvu]. Priporočamo metodo, ki uporabi program za nameščanje Stack. Najprej si namestite Stack, prek njega pa še Agdo.
  • VSCode razširitev agda-mode - razširitev predlaga uporabo eksperimentalno podporo za Language server protocol, vendar je ne uporabite, ker je delovanje počasno in nezanesljivo. Namesto tega bo razširitev z Agdo komunicirala prek Emacsa, ki ga bo samodejno naložil Stack.
  • zgoraj omenjeno knjižnico agda-unimath. Knjižnico si prenesite na svoj računalnik, nato pa pojdite v eno od datotek, npr. /src/foundation-core/functions.lagda.md ter v VSCode pritisnite Ctrl-C Ctrl-L, da preverite, ali se je datoteka uspešno naložila.

PRIJAVE in več informacij o računalniških delavnicah lahko najdete na spletni učilnici.