This repository has been archived by the owner. It is now read-only.
Permalink
Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
26 lines (22 sloc) 856 Bytes
\documentclass{article}
% You cannot compile this file with LaTeX directly. You should run
% "make doc", or if you do not have the make utility, you should run:
%
% coqdoc --latex -s --body-only -o univalence_body.tex univalence.v
% pdflatex univalence.tex
% pdflatex univalence.tex
% This file shows how to customize the output generated by coqdoc.
% We suppply our own header file, from which we include the file
% generated by coqdoc. This way we control the style of the document.
% See Makefile for the correct coqdoc incantation.
\usepackage[utf8]{inputenc}
\usepackage{fullpage}
\usepackage{coqdoc}
\usepackage{amsmath,amssymb}
\begin{document}
\author{Andrej Bauer \and Peter LeFanu Lumsdaine}
\title{A Coq proof that Univalence Axioms\\
implies Functional Extensionality}
\maketitle
\input{univalence_body.tex}
\end{document}