Added Agda code in latex, plus beginning of an introduction

.gitignore

@@ -4,3 +4,6 @@
 .\#*
 *.kate-swp
 /report/build/
+/report/agda/
+/report/agda.sty
+/latex

FFOL.lagda

@@ -1,3 +1,4 @@
+\begin{code}
 {-# OPTIONS --prop --rewriting #-}
 
 open import PropUtil
@@ -19,7 +20,8 @@ module FFOL where
       Con : Set ℓ¹
       Sub : Con → Con → Set ℓ⁵ -- It makes a category
       _∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ
-      ∘-ass : {Γ Δ Ξ Ψ : Con}{α : Sub Γ Δ}{β : Sub Δ Ξ}{γ : Sub Ξ Ψ} → (γ ∘ β) ∘ α ≡ γ ∘ (β ∘ α)
+      ∘-ass : {Γ Δ Ξ Ψ : Con}{α : Sub Γ Δ}{β : Sub Δ Ξ}{γ : Sub Ξ Ψ}
+        → (γ ∘ β) ∘ α ≡ γ ∘ (β ∘ α)
       id : {Γ : Con} → Sub Γ Γ
       idl : {Γ Δ : Con} {σ : Sub Γ Δ} →  (id {Δ}) ∘ σ ≡ σ
       idr : {Γ Δ : Con} {σ : Sub Γ Δ} →  σ ∘ (id {Γ}) ≡ σ
@@ -29,9 +31,10 @@ module FFOL where
 
       -- Functor Con → Set called Tm
       Tm : Con → Set ℓ²
-      _[_]t : {Γ Δ : Con} → Tm Γ → Sub Δ Γ → Tm Δ -- The functor's action on morphisms
+      _[_]t : {Γ Δ : Con} → Tm Γ → Sub Δ Γ → Tm Δ -- Action on morphisms
       []t-id : {Γ : Con} → {x : Tm Γ} → x [ id {Γ} ]t ≡ x
-      []t-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {t : Tm Γ} → t [ β ∘ α ]t ≡ (t [ β ]t) [ α ]t
+      []t-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ}{β : Sub Δ Γ} → {t : Tm Γ}
+        → t [ β ∘ α ]t ≡ (t [ β ]t) [ α ]t
 
       -- Tm : Set⁺
       _▹ₜ : Con → Con
@@ -41,56 +44,67 @@ module FFOL where
       πₜ²∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ² (σ ,ₜ t) ≡ t
       πₜ¹∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ¹ (σ ,ₜ t) ≡ σ
       ,ₜ∘πₜ : {Γ Δ : Con} → {σ : Sub Δ (Γ ▹ₜ)} → (πₜ¹ σ) ,ₜ (πₜ² σ) ≡ σ
-      ,ₜ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{t : Tm Γ} → (σ ,ₜ t) ∘ δ ≡ (σ ∘ δ) ,ₜ (t [ δ ]t)
+      ,ₜ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{t : Tm Γ}
+        → (σ ,ₜ t) ∘ δ ≡ (σ ∘ δ) ,ₜ (t [ δ ]t)
 
       -- Functor Con → Set called For
       For : Con → Set ℓ³
-      _[_]f : {Γ Δ : Con} → For Γ → Sub Δ Γ → For Δ -- The functor's action on morphisms
+      _[_]f : {Γ Δ : Con} → For Γ → Sub Δ Γ → For Δ -- Action on morphisms
       []f-id : {Γ : Con} → {F : For Γ} → F [ id {Γ} ]f ≡ F
-      []f-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ} → F [ β ∘ α ]f ≡ (F [ β ]f) [ α ]f
+      []f-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ}
+        → F [ β ∘ α ]f ≡ (F [ β ]f) [ α ]f
 
       -- Functor Con × For → Prop called Pf or ⊢
       _⊢_ : (Γ : Con) → For Γ → Prop ℓ⁴
-      _[_]p : {Γ Δ : Con} → {F : For Γ} → Γ ⊢ F → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) -- The functor's action on morphisms
+      -- Action on morphisms
+      _[_]p : {Γ Δ : Con} → {F : For Γ} → Γ ⊢ F → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f)
       -- Equalities below are useless because Γ ⊢ F is in prop
-      -- []p-id : {Γ : Con} → {F : For Γ} → {prf : Γ ⊢ F} → prf [ id {Γ} ]p ≡ prf
+      -- []p-id : {Γ : Con} → {F : For Γ} → {prf : Γ ⊢ F}
-      -- []p-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ} → {prf : Γ ⊢ F} → prf [ α ∘ β ]p ≡ (prf [ β ]p) [ α ]p
+      --  → prf [ id {Γ} ]p ≡ prf
+      -- []p-∘ : {Γ Δ Ξ : Con}{α : Sub Ξ Δ}{β : Sub Δ Γ}{F : For Γ}{prf : Γ ⊢ F}
+      --  → prf [ α ∘ β ]p ≡ (prf [ β ]p) [ α ]p
 
       -- → Prop⁺
       _▹ₚ_ : (Γ : Con) → For Γ → Con
-      πₚ¹ : {Γ Δ : Con} → {F : For Γ} → Sub Δ (Γ ▹ₚ F) → Sub Δ Γ
+      πₚ¹ : {Γ Δ : Con}{F : For Γ} → Sub Δ (Γ ▹ₚ F) → Sub Δ Γ
-      πₚ² : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ (Γ ▹ₚ F)) → Δ ⊢ (F [ πₚ¹ σ ]f)
+      πₚ² : {Γ Δ : Con}{F : For Γ} → (σ : Sub Δ (Γ ▹ₚ F)) → Δ ⊢ (F [ πₚ¹ σ ]f)
-      _,ₚ_ : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) → Sub Δ (Γ ▹ₚ F)
+      _,ₚ_ : {Γ Δ : Con}{F : For Γ} → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) → Sub Δ (Γ ▹ₚ F)
-      ,ₚ∘πₚ : {Γ Δ : Con} → {F : For Γ} → {σ : Sub Δ (Γ ▹ₚ F)} → (πₚ¹ σ) ,ₚ (πₚ² σ) ≡ σ
+      ,ₚ∘πₚ : {Γ Δ : Con}{F : For Γ}{σ : Sub Δ (Γ ▹ₚ F)} → (πₚ¹ σ) ,ₚ (πₚ² σ) ≡ σ
-      πₚ¹∘,ₚ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {F : For Γ} → {prf : Δ ⊢ (F [ σ ]f)} → πₚ¹ (σ ,ₚ prf) ≡ σ
+      πₚ¹∘,ₚ : {Γ Δ : Con}{σ : Sub Δ Γ}{F : For Γ}{prf : Δ ⊢ (F [ σ ]f)}
+        → πₚ¹ (σ ,ₚ prf) ≡ σ
       -- Equality below is useless because Γ ⊢ F is in Prop
-      -- πₚ²∘,ₚ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {F : For Γ} → {prf : Δ ⊢ (F [ σ ]f)} → πₚ² (σ ,ₚ prf) ≡ prf
+      -- πₚ²∘,ₚ : {Γ Δ : Con}{σ : Sub Δ Γ}{F : For Γ}{prf : Δ ⊢ (F [ σ ]f)}
-      ,ₚ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{F : For Ξ}{prf : Γ ⊢ (F [ σ ]f)} → (σ ,ₚ prf) ∘ δ ≡ (σ ∘ δ) ,ₚ (substP (λ F → Δ ⊢ F) (≡sym []f-∘) (prf [ δ ]p))
+      -- → πₚ² (σ ,ₚ prf) ≡ prf
+      ,ₚ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{F : For Ξ}{prf : Γ ⊢ (F [ σ ]f)}
+        → (σ ,ₚ prf) ∘ δ ≡ (σ ∘ δ) ,ₚ (substP (λ F → Δ ⊢ F) (≡sym []f-∘) (prf [ δ ]p))
 
       
       {-- FORMULAE CONSTRUCTORS --}
       -- Formulas with relation on terms
       R : {Γ : Con} → (t u : Tm Γ) → For Γ
-      R[] : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t u : Tm Γ} → (R t u) [ σ ]f ≡ R (t [ σ ]t) (u [ σ ]t)
+      R[] : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t u : Tm Γ}
+        → (R t u) [ σ ]f ≡ R (t [ σ ]t) (u [ σ ]t)
 
       -- Implication
       _⇒_ : {Γ : Con} → For Γ → For Γ → For Γ
-      []f-⇒ : {Γ Δ : Con} → {F G : For Γ} → {σ : Sub Δ Γ} → (F ⇒ G) [ σ ]f ≡ (F [ σ ]f) ⇒ (G [ σ ]f)
+      []f-⇒ : {Γ Δ : Con} → {F G : For Γ} → {σ : Sub Δ Γ}
+        → (F ⇒ G) [ σ ]f ≡ (F [ σ ]f) ⇒ (G [ σ ]f)
 
       -- Forall
       ∀∀ : {Γ : Con} → For (Γ ▹ₜ) → For Γ
-      []f-∀∀ : {Γ Δ : Con} → {F : For (Γ ▹ₜ)} → {σ : Sub Δ Γ} → (∀∀ F) [ σ ]f ≡ (∀∀ (F [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f))
+      []f-∀∀ : {Γ Δ : Con} → {F : For (Γ ▹ₜ)} → {σ : Sub Δ Γ}
+        → (∀∀ F) [ σ ]f ≡ (∀∀ (F [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f))
 
       {-- PROOFS CONSTRUCTORS --}
       -- Again, we don't have to write the _[_]p equalities as Proofs are in Prop
       
       -- Lam & App
-      lam : {Γ : Con} → {F : For Γ} → {G : For Γ} → (Γ ▹ₚ F) ⊢ (G [ πₚ¹ id ]f) → Γ ⊢ (F ⇒ G)
+      lam : {Γ : Con}{F G : For Γ} → (Γ ▹ₚ F) ⊢ (G [ πₚ¹ id ]f) → Γ ⊢ (F ⇒ G)
-      app : {Γ : Con} → {F G : For Γ} → Γ ⊢ (F ⇒ G) → Γ ⊢ F → Γ ⊢ G
+      app : {Γ : Con}{F G : For Γ} → Γ ⊢ (F ⇒ G) → Γ ⊢ F → Γ ⊢ G
 
       -- ∀i and ∀e
-      ∀i : {Γ : Con} → {F : For (Γ ▹ₜ)} → (Γ ▹ₜ) ⊢ F → Γ ⊢ (∀∀ F)
+      ∀i : {Γ : Con}{F : For (Γ ▹ₜ)} → (Γ ▹ₜ) ⊢ F → Γ ⊢ (∀∀ F)
-      ∀e : {Γ : Con} → {F : For (Γ ▹ₜ)} → Γ ⊢ (∀∀ F) → {t : Tm Γ} → Γ ⊢ ( F [(id {Γ}) ,ₜ t ]f)
+      ∀e : {Γ : Con}{F : For (Γ ▹ₜ)} → Γ ⊢ (∀∀ F) → {t : Tm Γ} → Γ ⊢ ( F [(id {Γ}) ,ₜ t ]f)
 
 
     -- Examples
@@ -363,3 +377,4 @@ module FFOL where
     -- (((∀ x . A (x)) ⇒ B)⇒ B) ⇒ ∀ x . ((A (x) ⇒ B) ⇒ B)
     ex5 : {A : For (⊤ₛ ▹ₜ)} → {B : For ⊤ₛ} → ⊤ₛ ⊢ ((((∀∀ A) ⇒ B) ⇒ B) ⇒ (∀∀ ((A ⇒ (B [ πₜ¹ id ]f)) ⇒ (B [ πₜ¹ id ]f))))
     ex5 ◇◇ h t h' = h (λ h'' → h' (h'' t))
+\end{code}

FFOLInitial.lagda

@@ -1,3 +1,4 @@
+\begin{code}
 {-# OPTIONS --prop --rewriting #-}
 
 open import PropUtil
@@ -219,8 +220,8 @@ module FFOLInitial where
   
 
   -- We now can create Renamings, a subcategory from (Conp,Subp) that
-  -- A renaming from a context Γₚ to a context Δₚ means that when they are seen as lists,
+  -- A renaming from a context Γₚ to a context Δₚ means when they are seen
-  -- that every element of Γₚ is an element of Δₚ
+  -- as lists, that every element of Γₚ is an element of Δₚ
   -- In other words, we can prove Γₚ from Δₚ using only proof variables (var)
   data Ren : Conp Γₜ → Conp Γₜ → Set₁ where
     zeroRen : Ren ◇p Γₚ
@@ -722,24 +723,26 @@ module FFOLInitial where
       (substP (λ X → (M FFOL.▹ₚ (M FFOL.▹ₜ) (mCon (con Γₜ Γₚ))) X ≡ (M FFOL.▹ₜ) ((M FFOL.▹ₚ mCon (con Γₜ Γₚ)) (mFor A)))
         (≡tran
           (coeshift {!!})
-          (cong (λ X → subst (FFOL.For M) _ (FFOL._[_]f M (mFor A) (mSub (sub (wkₜσₜ idₜ) X)))) (≡sym (coecoe-coe {eq1 = ?} {x = idₚ {Δₚ = Γₚ}}))))
+          (cong (λ X → subst (FFOL.For M) _ (FFOL._[_]f M (mFor A) (mSub (sub (wkₜσₜ idₜ) X)))) (≡sym (coecoe-coe {eq1 = {!!}} {x = idₚ {Δₚ = Γₚ}}))))
         {!!})
       (cong (M FFOL.▹ₜ) (≡sym (e▹ₚ {con Γₜ Γₚ})))
     -- substP (λ X → FFOL._▹ₚ_ M X (mFor {Γ = ?} (A [ wkₜσₜ idₜ ]f)) ≡ (FFOL._▹ₜ M (mCon (con Γₜ (Γₚ ▹p⁰ A))))) (≡sym (e▹ₜ {Γ = con Γₜ Γₚ})) ?
     
-
-
-    {-
-    
-
     m⊢ {Γ}{A}(var pvzero) = {!substP (λ X → FFOL._⊢_ M X (mFor A)) (≡sym e▹ₚ) ?!}
     m⊢ (var (pvnext pv)) = {!!}
     m⊢ (app pf pf') = FFOL.app M (m⊢ pf) (m⊢ pf')
     m⊢ (lam pf) = FFOL.lam M {!m⊢ pf!}
     m⊢ (p∀∀e pf) = {!FFOL.∀e M (m⊢ pf)!}
     m⊢ {Γ}{∀∀ A}(p∀∀i pf) = FFOL.∀i M (substP (λ X → FFOL._⊢_ M X (subst (FFOL.For M) (≡sym e▹ₜ) (mFor A))) e▹ₜ {!m⊢ pf!})
-
+    
     e[]f = {!!}
+    e▹ₚ = {!!}
+
+
+    {-
+    
+
+
     
 
     e∘ : {Γ Δ Ξ : Con}{δ : Sub Δ Ξ}{σ : Sub Γ Δ} → mSub (δ ∘ σ) ≡ FFOL._∘_ M (mSub δ) (mSub σ)
@@ -779,7 +782,7 @@ module FFOLInitial where
     
   --mor : (M : FFOL) → Morphism ffol M
   --mor M = record {InitialMorphism M}
-
+\end{code}
 
 
 

Makefile

@@ -0,0 +1,57 @@
+define extract
+	cat $(1) | grep -A5000 -m1 $(3) | grep -B5000 -m1 $(4) | head -n -1 | sed 's/\\>\[6\]/\\>\[0\]/g' > $(2)
+endef
+
+all: report/build/M1Report.pdf
+
+latex/FFOL.tex: FFOL.lagda
+	agda --latex $<
+	cp latex/agda.sty report/agda.sty
+latex/FFOLInitial.tex: FFOLInitial.lagda
+	agda --latex --allow-unsolved-metas $<
+	cp latex/agda.sty report/agda.sty
+
+report/build/M1Report.pdf: agda-tex-FFOL agda-tex-FIni
+	$(cd report/; latexmk -pdf -xelatex -silent -shell-escape -outdir=build/ -synctex=1 "M1Report")
+
+agda-tex-FIni: latex/FFOLInitial.tex
+	mkdir -p report/agda
+	@$(call extract,latex/FFOLInitial.tex,report/agda/ICont.tex,'Term\\ contexts\\ are\\ isomorphic\\ to\\ Nat','\\>\[0\]\\<')
+	@$(call extract,latex/FFOLInitial.tex,report/agda/ITm.tex,'A\\ term\\ variable\\ is\\ a\\ de-bruijn','\\>\[0\]\\<')
+	@$(call extract,latex/FFOLInitial.tex,report/agda/IFor.tex,'Now\\ we\\ can\\ define\\ formul','\\>\[0\]\\<')
+	@$(call extract,latex/FFOLInitial.tex,report/agda/ISubt.tex,'Then\\ we\\ define\\ term\\ substitutions','\\>\[0\]\\<')
+	@$(call extract,latex/FFOLInitial.tex,report/agda/ISubtT.tex,'We\\ now\\ define\\ the\\ action\\ of\\ term\\ substitutions','\\>\[0\]\\<')
+	@$(call extract,latex/FFOLInitial.tex,report/agda/ISubtF.tex,'We\\ can\\ now\\ subst\\ on\\ formul','\\AgdaEmptyExtraSkip')
+	@$(call extract,latex/FFOLInitial.tex,report/agda/IIdCompT.tex,'We\\ now\\ can\\ define\\ identity\\ and\\ composition\\ of\\ term\\ substitutions','\\AgdaEmptyExtraSkip')
+	@$(call extract,latex/FFOLInitial.tex,report/agda/IConp.tex,'We\\ can\\ now\\ define\\ proof\\ contexts','\\>\[0\]\\<')
+	@$(call extract,latex/FFOLInitial.tex,report/agda/ISubtC.tex,'The\\ actions\\ of\\ Subt'"'"'s\\ is\\ extended\\ to\\ contexts','This\\ Conp\\ is\\ indeed\\ a\\ functor')
+	@$(call extract,latex/FFOLInitial.tex,report/agda/IConpTp.tex,'We\\ can\\ also\\ add\\ a\\ term\\ that\\ will\\ not\\ be\\ used','We\\ show\\ how\\ it\\ interacts\\ with')
+	@cat latex/FFOLInitial.tex | grep -A5000 -m1 'With\\ those\\ contexts,\\ we\\ have\\ everything\\ to\\ define\\ proofs' | grep -B5000 -m1 "AgdaEmptyExtraSkip" | head -n -1 | sed 's/\\>\[6\]/\\>\[0\]/g' > report/agda/IPf.tex
+	@$(call extract,latex/FFOLInitial.tex,report/agda/IRen.tex,'We\\ now\\ can\\ create\\ Renamings','\\>\[0\]\\<')
+	@$(call extract,latex/FFOLInitial.tex,report/agda/ISubp.tex,'But\\ we\\ need\\ something\\ stronger\\ than\\ just\\ renamings','They\\ are\\ indeed\\ stronger\\ than\\ renamings')
+	@$(call extract,latex/FFOLInitial.tex,report/agda/ISubtP.tex,'\\>\[2\]\\AgdaOperator{\\AgdaFunction{\\AgdaUnderscore{}\[\\AgdaUnderscore{}\]pv','\\>\[0\]\\<')
+	@$(call extract,latex/FFOLInitial.tex,report/agda/ISubtS.tex,'\\>\[2\]\\AgdaOperator{\\AgdaFunction{\\AgdaUnderscore{}\[\\AgdaUnderscore{}\]σ','\\AgdaEmptyExtraSkip')
+	@$(call extract,latex/FFOLInitial.tex,report/agda/ISubpP.tex,'\\>\[2\]\\AgdaOperator{\\AgdaFunction{\\AgdaUnderscore{}\[\\AgdaUnderscore{}\]p}}','\\>\[0\]\\<')
+	@$(call extract,latex/FFOLInitial.tex,report/agda/IIdCompP.tex,'We\\ can\\ now\\ define\\ identity\\ and\\ composition\\ on\\ proof\\ substitutions','\\AgdaEmptyExtraSkip')
+	@cat latex/FFOLInitial.tex | grep -A5000 -m1 'We\\ can\\ now\\ merge\\ the\\ two\\ notions\\ of\\ contexts,\\ substitutions,\\ and\\ everything' | grep -B5000 -m1 '\\>\[0\]\\<' > report/agda/ICon.tex
+	@cat latex/FFOLInitial.tex | grep -A5000 -B1 -m1 '\\AgdaRecord{Sub}\\AgdaSpace{}%' | grep -B5000 -m1 '\\AgdaEmptyExtraSkip' > report/agda/ISub.tex
+	@$(call extract,latex/FFOLInitial.tex,report/agda/IIdComp.tex,'(Con,Sub)\\ is\\ a\\ category\\ with\\ an\\ initial\\ object','\\>\[2\]\\AgdaOperator{\\AgdaFunction{\\AgdaUnderscore{}')
+	@$(call extract,latex/FFOLInitial.tex,report/agda/ICExt.tex,'We\\ have\\ our\\ two\\ context\\ extension\\ operators','\\AgdaEmptyExtraSkip')
+
+agda-tex-FFOL: latex/FFOL.tex
+	mkdir -p report/agda
+	@$(call extract,latex/FFOL.tex,report/agda/Con.tex,'\\>\[6\]\\AgdaField{Con}',"AgdaEmptyExtraSkip")
+	@$(call extract,latex/FFOL.tex,report/agda/Tm.tex,'\\>\[6\]\\AgdaField{Tm}',"AgdaEmptyExtraSkip")
+	@$(call extract,latex/FFOL.tex,report/agda/Tm+.tex,'\\>\[6\]\\AgdaOperator{\\AgdaField{\\AgdaUnderscore{}▹ₜ}}',"AgdaEmptyExtraSkip")
+	@$(call extract,latex/FFOL.tex,report/agda/For.tex,'\\>\[6\]\\AgdaField{For}',"AgdaEmptyExtraSkip")
+	@$(call extract,latex/FFOL.tex,report/agda/Pf.tex,'\\>\[6\]\\AgdaOperator{\\AgdaField{\\AgdaUnderscore{}⊢\\AgdaUnderscore{}}}',"AgdaEmptyExtraSkip")
+	@$(call extract,latex/FFOL.tex,report/agda/Pf+.tex,'\\>\[6\]\\AgdaOperator{\\AgdaField{\\AgdaUnderscore{}▹ₚ\\AgdaUnderscore{}}}',"AgdaEmptyExtraSkip")
+	@$(call extract,latex/FFOL.tex,report/agda/R.tex,'\\>\[6\]\\AgdaField{R}',"AgdaEmptyExtraSkip")
+	@$(call extract,latex/FFOL.tex,report/agda/Imp.tex,'\\>\[6\]\\AgdaOperator{\\AgdaField{\\AgdaUnderscore{}⇒\\AgdaUnderscore{}}}',"AgdaEmptyExtraSkip")
+	@$(call extract,latex/FFOL.tex,report/agda/Forall.tex,'\\>\[6\]\\AgdaField{∀∀}',"AgdaEmptyExtraSkip")
+	@$(call extract,latex/FFOL.tex,report/agda/LamApp.tex,'\\>\[6\]\\AgdaField{lam}',"AgdaEmptyExtraSkip")
+	@$(call extract,latex/FFOL.tex,report/agda/ForallR.tex,'\\>\[6\]\\AgdaField{∀i}',"AgdaEmptyExtraSkip")
+
+.PHONY: clean agda-tex agda-tex-FFOL
+clean:
+	rm -fr *.agdai report/agda latex report/build

report/M1Report.tex

@@ -1,4 +1,4 @@
-% !TeX spellcheck = fr_FR
+% !TeX spellcheck = en_US
 \documentclass[10pt,a4paper]{article}
 
 \include{./header.tex}
@@ -21,8 +21,17 @@
 	
 	\newpage
 	
+	
 	\section{Introduction}
+	
+		In the first place, i was supposed to do this internship in Nottingham (UK) with Thorsten Altenkirsh. But, because of administrative issues, i was not able to go there, and Thorsten Altenkirsh contacted Ambrus Kaposi in Budapest, whose university agreed to accept me. Therefore, i went to Budapest and i did the internship under the physical supervision of Ambrus Kaposi, and the remote supervision of Thorsten Altenkirsch.
+		
+		The original subject of the internship was \enquote{Developping a simplified account of normalization by evaluation using the theory of categories with families}. But there was a lot to do, starting with learning how to use Agda.
+		
 		\subsection{Introduction to the problem}
+			What i do call a \enquote{logic} is a set of definitions containing formulæ and a notion of provability of those formulæ, plus a set of operators/equalities to construct or reduce these rules. I have studied the most common logical frameworks, that is, Propositional Logic, First-order logic with infinitary predicates, and Predicate Logic. For each of those logics, one can define a notion of \emph{model}. A model of a certain kind of logic is something that implements all of the logic's definitions, operators and equalities. From all of those models, one can extract the \emph{initial model}, also called \emph{syntax}. It is the smallest of all models, which means that from any model of that logic, we have a morphism from the syntax to that model.
+			
+			Then, our goal is for each logic to prove the completeness of a specific class of models. Completeness can be stated as such: \enquote{For any formula that is \emph{true} in all models of the specified class, then the formula has a proof in the syntax}. By being true in the model, one can understand that the formula has a proof from the model.
 		\subsection{Motivation}
 		\subsection{Structure of this report}
 	\section{A first account of Completeness and Normalization}
@@ -31,11 +40,158 @@
 		\subsection{Merging the two proofs}
 	\section{Predicate Logic}
 		\subsection{SOGAT Presentation of FFOL}
+		
+		\begin{tcolorbox}
+			\[
+			\begin{array}{lcl}
+				\Tm & : & \Set^+ \\
+				\\
+				\For & : & \Set \\
+				- \implies - & : & \For \rightarrow \For \rightarrow \For\\
+				\forall & : & (\Tm \rightarrow \For) \rightarrow \For \\
+				\R & : & \Tm \rightarrow \Tm \rightarrow \For\\
+				\\
+				\Pf & : & \For \rightarrow \Prop^+ \\
+				\lam & : & (\Pf A \rightarrow \Pf B) \rightarrow \Pf (A \implies B)\\
+				\app & : & \Pf (A \implies B) \rightarrow (\Pf A \rightarrow \Pf B)\\
+				\foralli & : & (t : \Tm \rightarrow^+ A\;t) \rightarrow \Pf (\forall A)\\
+				\foralle & : & \Pf (\forall A) \rightarrow (t : \Tm) \rightarrow \Pf (A\;t)\\
+			\end{array}
+			\]
+		\end{tcolorbox}
+	
 		\subsection{Turning a SOGAT Presentation into a GAT}
+			\begin{tcolorbox}
+				\agda{agda/Con.tex}
+			\end{tcolorbox}
+	
+			\begin{tcolorbox}
+				\agda{agda/Tm.tex}
+			\end{tcolorbox}
+	
+			\begin{tcolorbox}
+				\agda{agda/Tm+.tex}
+			\end{tcolorbox}
+	
+			\begin{tcolorbox}
+				\agda{agda/For.tex}
+			\end{tcolorbox}
+	
+			\begin{tcolorbox}
+				\agda{agda/Pf.tex}
+			\end{tcolorbox}
+	
+			\begin{tcolorbox}
+				\agda{agda/Pf+.tex}
+			\end{tcolorbox}
+	
+			\begin{tcolorbox}
+				\agda{agda/R.tex}
+			\end{tcolorbox}
+	
+			\begin{tcolorbox}
+				\agda{agda/Imp.tex}
+			\end{tcolorbox}
+	
+			\begin{tcolorbox}
+				\agda{agda/Forall.tex}
+			\end{tcolorbox}
+	
+			\begin{tcolorbox}
+				\agda{agda/LamApp.tex}
+			\end{tcolorbox}
+	
+			\begin{tcolorbox}
+				\agda{agda/ForallR.tex}
+			\end{tcolorbox}
+			
 	\section{Implementing the Syntax}
 		\subsection{Separated Contexts}
+		
+			\begin{tcolorbox}
+				\agda{agda/ICont.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/IFor.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/ISubt.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/ITm.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/ISubtT.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/ISubTF.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/IIdCompT.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/IConp.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/ISubtC.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/IConpTp.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/IPf.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/IRen.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/ISubp.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/ISubtP.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/ISubtS.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/ISubpP.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/IIdCompP.tex}
+			\end{tcolorbox}
+			\begin{tcolorbox}
+				\agda{agda/ICon.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/ISub.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/IIdComp.tex}
+			\end{tcolorbox}
+		
+			\begin{tcolorbox}
+				\agda{agda/ICExt.tex}
+			\end{tcolorbox}
+		
 		\subsection{Transport Hell}
-	%\section{Completeness and Normalization for FFOL}
 	
 	\section{Summary}
 	

report/header.tex

@@ -1,6 +1,5 @@
-% Loading packages
+% Loading packages 
-\usepackage[T1]{fontenc}
+\usepackage{autofe}
-\usepackage[utf8]{inputenc}
 \usepackage{hyperref}
 \hypersetup{
 	colorlinks=true,
@@ -16,7 +15,6 @@
 \usepackage{csquotes}
 \usepackage{listings}
 \usepackage{lstautogobble}
-\usepackage{algorithm2e}
 \usepackage{svg}
 \usepackage{tikz}
 \usepackage{multirow}
@@ -34,6 +32,7 @@
 \usepackage{mathtools}
 \usepackage[page,header]{appendix}
 \usepackage{minitoc}
+\usepackage{mathtools}
 
 \usepackage{geometry}
 
@@ -59,9 +58,6 @@
 \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}
@@ -95,7 +91,46 @@
 
 
 % Macros caractères spécifiques au document
+\newcommand\Tm{\operatorname{Tm}}
+\newcommand\Set{\operatorname{Set}}
+\newcommand\For{\operatorname{For}}
+\newcommand\Prop{\operatorname{Prop}}
+\newcommand\R{\operatorname{R}}
+\newcommand\lam{\operatorname{lam}}
+\newcommand\app{\operatorname{app}}
+\newcommand\foralli{\operatorname{\operatorname{\forall i}}}
+\newcommand\foralle{\operatorname{\operatorname{\forall e}}}
+\newcommand\Pf{\operatorname{Pf}\;}
 
+% Agda Config
+\usepackage{agda}
+\usepackage{newunicodechar}
+\newunicodechar{∘}{\ensuremath{\mathnormal{\circ}}}
+\newunicodechar{≡}{\ensuremath{\mathnormal{\equiv}}}
+\newunicodechar{◇}{\ensuremath{\mathnormal{\diamond}}}
+\newunicodechar{α}{\ensuremath{\mathnormal{\alpha}}}
+\newunicodechar{β}{\ensuremath{\mathnormal{\beta}}}
+\newunicodechar{γ}{\ensuremath{\mathnormal{\gamma}}}
+\newunicodechar{δ}{\ensuremath{\mathnormal{\delta}}}
+\newunicodechar{ε}{\ensuremath{\mathnormal{\varepsilon}}}
+\newunicodechar{σ}{\ensuremath{\mathnormal{\sigma}}}
+\newunicodechar{π}{\ensuremath{\mathnormal{\pi}}}
+\newunicodechar{▹}{\ensuremath{\mathnormal{\triangleright}}}
+\newunicodechar{⊢}{\ensuremath{\mathnormal{\vdash}}}
+\newunicodechar{⇒}{\ensuremath{\mathnormal{\Rightarrow}}}
+\newunicodechar{∀}{\ensuremath{\mathnormal{\forall}}}
+\newunicodechar{≈}{\ensuremath{\mathnormal{\approx}}}
+\newunicodechar{ₜ}{\ensuremath{{}_t}}
+\newunicodechar{ₚ}{\ensuremath{{}_p}}
+\newunicodechar{⁰}{\ensuremath{{}^0}}
+
+
+\newcommand\agda[1]{
+	\small
+	\begin{code}
+		\input{#1}
+	\end{code}
+}
 % Création des environnements spécifiques au document