## Formalisation for the paper ["Internal strict propositions using point-free equations"](paper.pdf).

Section 3:

* [lib.agda](lib.agda) contains the notion of point-free proposition and general properties.

Section 7:

* [Model](Model) is the setoid model with Π,Σ,⊥,⊤ and a sort TyP closed under Π,Σ,⊤. We don't prove most substitution rules.
* [ModelStrict](ModelStrict) is the strictification of this model (using the local universe method). We prove all substitution rules.

Other things:

* [hModel](hModel) is the partial definition of the setoid model using ordinary propositions (not point-free).
* [rModel](rModel) is the partial definition of the "unsaturated" setoid model where the relation is not a proposition.
* [GraphModel.agda](GraphModel.agda) is the formalisation of the category of graphs defined in an essentially algebraic way (as opposed to generalised algebraic). This means that there is a set of edges with `dom` and `cod` functions (as opposed to a family of edges indexed by pairs of vertices). When the equations for graph homomorphisms are defined in a point-free way, we should be able to prove the category laws without funext.
* [Isti](Isti) is a nicer formalisation of point-free propositions and parts of the setoid model.
* [todo.txt](todo.txt) has more things that could go in the paper and some further research ideas