\documentclass[12pt]{article}
\usepackage{amsmath, amssymb, amsthm, graphicx, epsfig, fancyhdr}
\title{Math 392A Overleaf Form}
\author {Parikshit Khanna}
\setlength{\headheight}{28pt}
\pagestyle{fancy}
\fancyhf{}
\fancyhead[R]{Parikshit Khanna \\ Math 392A}
\fancyfoot[R]{Homotopy Type Theory}
\begin{document}
\begin{center} \LARGE Homotopy Type Theory\end{center}
\begin{center} \large Under-graduate Project\end{center}
\textit{}
\begin{section} {Section 1 : Fundamentals}
\begin{subsection} {Proposition-as-Types}
The basic judgement of Type Theory,analogous to the proposition,A has a proof,is \textbf{a : A},where \\ A is the proposition \\a is the proof of the proposition A\\
A proposition can have multiple proofs,which can be expressed as \\\textbf{a,b : A},where a and b are different proofs of A.In Type Theory Proposition A is a type and its proofs,i.e a and b are called witnesses of A.A type having a witness is called an inhabited type while a proposition having no proof is termed as an uninhabited type.For instance while 1=2 is a valid proposition,it has no witness and hance an uninhabited type.
\end{subsection}
\begin{subsection} {Universes}\end{subsection}
\end{section}
\end{document}
