Notes from the meeting

[Bas Spitters]

I have just returned home from an amazing time.
Thanks to all of you for the very pleasant atmosphere and open collaboration!
I'll miss it. I hope we can keep it up via the internet.

Here are my notes of the meeting, please expand, make the open problems more precise if you want.
http://uf-ias-2012.wikispaces.com/Notes

[Andrej Bauer]

I would like to put Ljubljana to the list of places where people are interested in a new proof assistant. If you will have us.

Next academic year Chris Stone (of Harper-Stone singleton kinds) will be spending in Ljubljana. We're planning to work on a proof assistant.

[Hugo Herbelin]

Hi,

Is point 2 of the list referring to an inductively-generated,
constructive, dependently-typed notion of simplicial types, similar to
the semi-simplicial types construction described on
http://uf-ias-2012.wikispaces.com/Semi-simplicial+types? If yes, then
I'm continuing working on it, injecting degeneracies on the fly, as
already discussed, and using (strict) equations for ensuring the
"ds=sd" constraints, as proposed by PLL. My time is however limited
and, even if the global picture is now stable, there are a couple of
details still to clarify before to reasonably make it public (the
approach remains anyway quite different from a presheaf approach!).

By the way, I join Dan G. and Bas to express how uniquely memorable,
educational, "enrichissant" was my term at IAS (Fall in my case,
then). Thanks to everyone and, specially, to the organizers.

Hugo

> --
> You received this message because you are subscribed to the Google Groups "IAS
> Univalent Foundations" group.
> To unsubscribe from this group and stop receiving emails from it, send an email
> to univalent-founda...@googlegroups.com.
> To post to this group, send email to univalent-...@googlegroups.com.
> Visit this group at http://groups.google.com/group/univalent-foundations?hl=en.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>