Started to write the report, created toc and files

.gitignore

@@ -3,3 +3,4 @@
 \#*\#
 .\#*
 *.kate-swp
+/report/build/

report/Bilibibio.bib

@@ -0,0 +1,30 @@
+@article{RedFreeNorm1995,
+	doi = {10.1007/3-540-60164-3_27},
+	url = {https://doi.org/10.1007\%2F3-540-60164-3_27},
+	year = 1995,
+	publisher = {Springer Berlin Heidelberg},
+	pages = {182--199},
+	author = {Thorsten Altenkirch and Martin Hofmann and Thomas Streicher},
+	title = {Categorical reconstruction of a reduction free normalization proof},
+	booktitle = {Category Theory and Computer Science}
+}
+@article{NBE2016,
+	title={Normalisation by Evaluation for Dependent Types},
+	author={Thorsten Altenkirch and Ambrus Kaposi},
+	booktitle={International Conference on Formal Structures for Computation and Deduction},
+	year={2016}
+}
+@phdthesis{AltenkirschThesis1993,
+	title={Constructions, inductive types and strong normalization},
+	author={Thorsten Altenkirch},
+	booktitle={CST},
+	year={1993}
+}
+@unpublished{TaoOfTypes,
+	title={The Tao of Types},
+	author={Thorsten Altenkirsch}
+}
+@inproceedings{folSogatKaposi2023,
+	title={Why is equality interesting?},
+	author={Ambrus Kaposi},
+	url={https://akaposi.github.io/pres_wld.pdf}}

report/M1Report.tex

@@ -0,0 +1,57 @@
+% !TeX spellcheck = fr_FR
+\documentclass[10pt,a4paper]{article}
+
+\include{./header.tex}
+
+\title{Completeness Proof for different logical frameworks
+	\\[1ex] \large Notes on my 3 month internship at Faculty of Informatics (ELTE, Budapest)}
+\hypersetup{pdftitle={Completeness Proof for different kinds of logical frameworks}}
+\author{Samy Avrillon, supervised by
+	\\[1ex] Ambrus Kaposi (ELTE, Budapest)
+	\\[1ex] and Thorsten Altenkirsch (University of Notthingham, United Kingdom)}
+
+\begin{document}
+	
+	\doparttoc
+	\maketitle
+	
+	\hsep
+	
+	\tableofcontents
+	
+	\newpage
+	
+	\section{Introduction}
+		\subsection{Introduction to the problem}
+		\subsection{Motivation}
+		\subsection{Structure of this report}
+	\section{A first account of Completeness and Normalization}
+		\subsection{Normalization for ZOL}
+		\subsection{Normalization for IFOL}
+		\subsection{Merging the two proofs}
+	\section{Predicate Logic}
+		\subsection{SOGAT Presentation of FFOL}
+		\subsection{Turning a SOGAT Presentation into a GAT}
+	\section{Implementing the Syntax}
+		\subsection{Separated Contexts}
+		\subsection{Transport Hell}
+	%\section{Completeness and Normalization for FFOL}
+	
+	\section{Summary}
+	
+	
+	\section{Bibliography}
+	\begingroup
+	\renewcommand{\section}[2]{}%
+	\printbibliography
+	\endgroup
+	
+	\newpage
+	\addappheadtotoc
+	\appendix
+	\addtocontents{toc}{\protect\setcounter{tocdepth}{-1}}
+	\appendixpage
+	
+	\section{Agda Code}
+	
+\end{document} 

report/header.tex

@@ -0,0 +1,110 @@
+% Loading packages
+\usepackage[T1]{fontenc}
+\usepackage[utf8]{inputenc}
+\usepackage{hyperref}
+\hypersetup{
+	colorlinks=true,
+	linkcolor=blue,
+	filecolor=magenta,      
+	urlcolor=cyan
+}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{bbm}
+\usepackage{stmaryrd}
+\usepackage[main=english]{babel}
+\usepackage{csquotes}
+\usepackage{listings}
+\usepackage{lstautogobble}
+\usepackage{algorithm2e}
+\usepackage{svg}
+\usepackage{tikz}
+\usepackage{multirow}
+\usepackage{multicol}
+\usepackage{tcolorbox}
+\usepackage{mdframed}
+\usepackage{proof}
+\usepackage{biblatex}
+\usepackage{xparse}
+\usepackage{cprotect}
+\usepackage{titlesec}
+\usepackage{xpatch}
+\usepackage{enumitem}
+\usepackage{amsfonts}
+\usepackage{mathtools}
+\usepackage[page,header]{appendix}
+\usepackage{minitoc}
+
+\usepackage{geometry}
+
+\usepackage{csquotes}
+\usepackage[lighttt]{lmodern}
+\usetikzlibrary{shapes.geometric,positioning}
+
+% Macros caractères globales
+\newcommand{\pgrph}{\P}
+\newcommand{\hsep}{\vspace{.2cm}\centerline{\rule{0.8\linewidth}{.05pt}}\vspace{.4cm}}
+\renewcommand{\P}{\mathbb{P}}
+\newcommand{\E}{\mathbb{E}}
+\newcommand{\1}{\scalebox{1.2}{$\mathbbm{1}$}}
+\newcommand{\floor}[1]{\left\lfloor#1\right\rfloor}
+\newcommand{\littleO}{o}
+\newcommand{\bigO}{\mathcal{O}}
+\newcommand{\longdash}{\:\textrm{---}\:}
+\newcommand\hole{\left[\raisebox{-0.25ex}{\scalebox{1.2}{$\cdot$}}\right]}
+\newcommand\bracket[1]{\!\left[#1\right]}
+\newcommand{\ssi}{\quad\text{\underline{ssi}}\quad}
+\newcommand\eng[1]{\textit{\foreignlanguage{english}{#1}}}
+\newcommand\spacebar{\;|\;}
+\def\nDownarrow{\not\mspace{1mu}\Downarrow}
+\let\pprec\preccurlyeq
+
+\DeclareUnicodeCharacter{03BB}{$\lambda$}
+\DeclareUnicodeCharacter{03B1}{$\alpha$}
+\DeclareUnicodeCharacter{03C0}{$\pi$}
+
+% Création des environnement globaux
+\newtheorem{theorem}{Théorème}
+\newtheorem{definition}{Definition}
+\newtheorem{property}{Propriété}
+
+\newcounter{rule}
+\addto\extrasfrench{%
+	\renewcommand{\figureautorefname}{\textsc{Figure}}
+	\renewcommand{\sectionautorefname}{Section}
+	\renewcommand{\subsectionautorefname}{Sous-section}
+	\renewcommand{\appendixautorefname}{Annexe}
+	\renewcommand{\theoremautorefname}{Théorème}
+	\providecommand\propertyautorefname{Propriété}
+	\providecommand\ruleautorefname{règle}
+}
+
+% Commandes logiques globales
+\newcommand{\ifnullthenelse}[3]{
+	\ifnum\value{#1}=0
+	#2
+	\else
+	#3
+	\fi
+}
+
+%%% Commande \newtag permettant de changer le label d'une equation
+\makeatletter
+\newcommand\newtag[2]{#1\def\@currentlabel{#1}\label{#2}}
+\makeatother
+
+
+% Macros caractères spécifiques au document
+
+% Création des environnements spécifiques au document
+
+
+%%% Subparaghaphs box
+\newtcbox{\subparaghaphbox}{nobeforeafter,tcbox raise base, arc=9pt, outer arc=9pt, boxsep=2pt,left=2pt,right=2pt,top=2pt,bottom=2pt,boxrule=1pt,colback=white!85!orange}
+\newcommand{\subparaghaphboxedcontent}[1]{\subparaghaphbox{#1}\newline}
+%\titleclass{\mathcases}{straight}[\subparagraph]
+\titleformat{\subparagraph}[runin]{\normalfont\normalsize\bfseries}{}{0em}{\subparaghaphboxedcontent}
+\titlespacing*{\subparagraph}{0pt}{3.25ex plus 1ex minus .2ex}{0.5em}
+
+
+\addbibresource{Bilibibio.bib}