agda-unimath

agda-unimath copied to clipboard

Shifts and unshifts of concepts around sequential colimits

3

This PR formalizes shifts of sequential diagrams, morphisms of sequential diagrams, cocones of sequential diagrams, homotopies of cocones of sequential diagrams, and unshifts of the last two. This machinery is...

VojtechStep

Rebase infrastructure for pushouts to span diagrams

24

In this PR I refactor the definitions of spans, morphisms of spans, and equivalences of spans (previously called homotopies of spans), and I will work on a better integration of...

EgbertRijke

Null maps, null types and null type families

1

Defines `Y`-null maps, `Y`-null types and `Y`-null type families, and establishes a few basic properties of these. Also formalizes the fiber condition for orthogonal maps. Part of #930. Depends on...

fredrik-bakke

Coherence triangles take arguments in the order `left -> right -> top`, but I would assume, given how other coherence diagrams take arguments in the order left-to-right top-to-bottom, that they...

fredrik-bakke

Progress on #930. Depends on #1042.

fredrik-bakke

I already formalized and documented parts of the paper. I'm assigning myself, because I would like to include this formalization effort in my master's thesis.

VojtechStep

Competing conventions for operations on propositions

5

The competing conventions are as follows: 1. use special binary operators taking values in types: `_⇔_ : Prop → Prop → UU` 2. use special binary operators taking values in...

fredrik-bakke

Let being an isomorphism be a property

4

In this pull request I am testing out whether it is sensible to let isomorphisms be a property in a uniformly defined manner across the library. Note: these changes are...

EgbertRijke

Create a `logic` namespace, and move the appropriate modules there.

fredrik-bakke

### Goals - [ ] Change definition names that use `UU` to use `Type` - [ ] Rename `UU` to `Type` - [ ] Rename `UUω` to `Large-Type`

fredrik-bakke