Miëtek Bak

It is now possible to deploy _gitit_ to Heroku with two clicks. Check out [my fork](https://github.com/mietek/gitit).

@pankajmore, @jgm: check out @master-q’s [success story](https://twitter.com/masterq_mogumog/status/532183331148804096). [Step-by-step instructions](https://halcyon.sh/examples/#gitit) will soon be available.

@thosgood: Since my last comment, I’ve generalised my work so that it’s possible to easily install Haskell applications on arbitrary platforms — not just on Heroku. The correct link is...

Please take a look at [`.profile.d/gitit.sh`](https://github.com/mietek/gitit/blob/master/.profile.d/gitit.sh). Almost all environment variables correspond directly to Gitit options, which are described in [`README.original.md`](https://github.com/mietek/gitit/blob/master/README.original.md#configuring-and-customizing-gitit). [`GITIT_GIT_URL`](https://github.com/mietek/gitit/blob/master/.profile.d/gitit.sh#L116) is the link to a _git_ repository which will...

Email sent.

@czwanzig: any updates?

It appears that we are [unlikely to get the 1971 version](https://www.reddit.com/r/dependent_types/comments/3s7ws5/looking_for_a_theory_of_types/cz54f8y?context=6): > I talked to Martin-Löf today. Unfortunately he does not want "A theory of types" to be published or...

The 1971 version is being reformulated by @pigworker: https://github.com/pigworker/Bi71

> I looked at `Function/`, opened `Function.Definitions` and found that it was re-exporting `Surjective` from `Function.Definitions.Core2`. Ah! Thank you. Unfortunately, I looked at [`Function.Surjection`](http://agda.github.io/agda-stdlib/Function.Surjection.html) and found myself in a never-ending...

> In the non-setoid (`_≡_`) case, it's not clear to me that it makes sense to distinguish between _surjective_ and _split-surjective._ We can't even state the distinction in MLTT. As...