Readme.txt

The following files contains developments in Coq .


PropasTypesUtf8Notation.v

This file contains notations in UTF8 for propositions
as types notions at the Set level. Author: Olov Wilander 2012.

PropasTypesBasics_mod.v

A collection of basic definition and lemmas for Propositions
as types at the Set level. Author: Olov Wilander 2012

SwedishSetoids_mod.v
SwedishSetoids_mod2.v

This contains definitions and results relating to setoids
where the equivalence relation has truth values in Set 
(and not in Prop as in the standard Coq library). The binary 
sum, binary product and the coequalizer constructions for
the category of setoids  are established. Author:
Olov Wilander 2012. Modification 2 uses a different 
record structure for setoids to optimize speed.


CZF_pure.v

The Aczel model of CZF formalized. Main author:
Olov Wilander 2012. (Some tactics do not work
in Coq 8.4.)

CZF_pure_plus_REA.v

The Aczel model of CZF formalized extended with
verification of REA. Author: Erik Palmgren 2013
(Some tactics do not work in Coq 8.4.)

CZFU_extension.v

The Aczel model of CZFU (CZF with atoms) and results about
V-representable setoids.  formalized. Author:
Olov Wilander 2012. (Some tactics do not work
in Coq 8.4.)


CZF_and_set_categories.v
CZF_and_set_categories_corrected.v

This contains the constructions of the two categories
of sets and a proof of their isomorphisms as described
in  the paper "Constructing categories and setoids of
setoids in type theory" by Erik Palmgren and Olov Wilander
2013.  (Some tactics do not work in Coq 8.4.)


CZF&setoids.pdf

The paper "Constructing categories and setoids of
setoids in type theory" by Erik Palmgren and Olov Wilander
2013.


families_of_setoids_and_LCCC.v

Contains proofs for the fact that the setoids form a locally 
cartesian closed pretopos and in particular a locally 
cartesian closed category. Categories are here defined 
without assuming equality on objects (so called e-categories).
The proof is using Pi- and Sigma-constructions for
families of setoids. Author: Erik Palmgren 2012.

CategoricalUniverse.v
CategoricalUniverse_v2.v

Contains a construction of a category of setoids and has equality on 
objects, and which is closed under pullbacks. This described in  
revised versions of the paper "Constructing categories and setoids of
setoids in type theory" by Erik Palmgren and Olov Wilander
2013. Version 2 (E.P.) became considerably faster by reformatting the
main records structures. 


Author: Erik Palmgren 2013, based on a formalization of
Olov Wilander of an extensional universe of setoids.

Generators.v

Shows that in (Cat_from_family F) the terminal object is a strong
generators whenever it is represented. (See "Constructing 
categories and setoids ofsetoids in type theory" 
by Erik Palmgren and Olov Wilander 2013.

Author: Erik Palmgren 2013.