Next Meetup

[fredefox] Univalent Categories: A formalization of cat. theory in Cubical Agda
ABSTRACT: The usual notion of propositional equality in intensional type-theory is restrictive. For instance it does not admit functional extensionality or univalence. This poses a severe limitation on both what is _provable_ and the _re-usability_ of proofs. Recent developments have, however, resulted in cubical type theory which permits a constructive proof of these two important notions. The programming language Agda has been extended with capabilities for working in such a cubical setting. This thesis will explore the usefulness of this extension in the context of category theory. The thesis will motivate and explain why propositional equality in cubical Agda is more expressive than in standard Agda. Alternative approaches to Cubical Agda will be presented and their pros and cons will be explained. It will emphasize why it is useful to have a constructive interpretation of univalence. As an example of this two formulations of monads will be presented: Namely monaeds in the monoidal form an monads in the Kleisli form. Finally the thesis will explain the challenges that a developer will face when working with cubical Agda and give some techniques to overcome these difficulties. It will also try to suggest how future work can help alleviate some of these challenges. BIO: Frederik Hanghøj Iversen Work experience: 2018 | Haskell Developer | Gothenburg University. Maintainer of MULLE 2017 | Teachers Assistant | Chalmers University of Technology 2015 - 2016 | Netcompany A/S | Developer 2013 - 2015 | IT Minds | Developer 2014 - 2015 | Copenhagen University and DTU | Teachers Assistant Education: 2016 - 2018 | Masters Degree, Computer Science | Chalmers University of Technology 2010 - 2014 | Bachelors Degree, Computer Science | Aarhus University --- We have set up a collaboration with Prosa, who generously offered to provide a location for our regular meetups. Please see Prosa's Calendar for more details: Prosa Calendar ( The ADA meeting room fits about 25 people and if we need more space, we can use the canteen (PASCAL), which has a capacity of at most 50 (fire regulation). Regards, Ramón and Joakim

Needs a location


What we're about

På Dansk:

Vi er et fællesskab af funktionelle programmeringsentusiaster, nybegyndere, fagfolk og forskere.

Mødegruppe for Funktionelle Københavnere formål er at få flere software projekter til at tage udgangspunkt i funktionelle programmeringssprog.

Vi har primært fokus på F# og Haskell, men andre funktionelle programmeringssprog som Scala, Lisp, Erlang, Clojure, OCaml, osv. er mere end velkommen.

Vi forventer at mødes minimum 12 gange om året, hvis ikke flere, for at udveksle erfaringer ved bruget af de funktionelle programmeringssprog i software projekter som skulle være i/eller på vej til produktion.

Bemarkning: Vi er sprog agnostisk, selvom F# vises i gruppens navn og vi anvender Haskells logo.

In English:

We're a community of functional programming enthusiasts, newbies, professionals and researchers.

F#unctional Copenhageners Meetup Group goal is to get more software projects to be based on functional programming languages.

We mainly focus on F# and Haskell, but other functional programming languages ​​like Scala, Lisp, Erlang, Clojure, OCaml, etc. are more than welcome.

We expect to meet at least twelve times a year, if not more, to share experiences with regards of the use of functional programming languages ​​in software projects that are in / or heading to production.

Remark: We are language agnostic, even though F# appears in our name and we use Haskells logo.

Members (988)

Photos (44)