Closure properties of acyclic maps and types

[tomdjong]

I also formalized that we have symmetric pushout squares (for pullbacks this was already in the library), i.e. the pushout of two maps f and g is also the pushout of g and f.

[fredrik-bakke]

Very nice pull request, you're picking up steam with these!

It's a bit unfortunate that you have results about acyclic types in the file about acyclic maps, but I see there's a dependency issue.

[tomdjong]

It's a bit unfortunate that you have results about acyclic types in the file about acyclic maps, but I see there's a dependency issue.

Yes, I agree. I have some ideas on how to resolve this, but I will check them when I meet with Egbert next week. For the moment, I would be happy to get all closure properties merged and then I can reorganize later.