updates

src/CubicalHott/Theorem7-1-11.agda

@@ -12,7 +12,7 @@ open import Cubical.Data.Nat
 open import Data.Unit
 
 lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n)
-lemma zero (A , a , Acontr) (B , b , Bcontr) i = A≡B i , a≡b i , eq where
+lemma zero (A , a , Acontr) (B , b , Bcontr) i = A≡B i , a≡b i , λ y j → wtf i y j where
   eqv1 : A ≃ B
   eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr)
 
@@ -22,8 +22,20 @@ lemma zero (A , a , Acontr) (B , b , Bcontr) i = A≡B i , a≡b i , eq where
   a≡b : PathP (λ i → A≡B i) a b
   a≡b j = glue (λ { (j = i0) → a ; (j = i1) → b }) b
 
-  eq : (y : A≡B i) → a≡b i ≡ y
-  eq y j = {!   !}
+  eqv2 : ((y : A) → a ≡ y) ≡ ((y : B) → b ≡ y)
+  eqv2 = λ i → (y : A≡B i) → a≡b i ≡ y
+
+  T1 = λ { (i = i0) → ((y : A) → a ≡ y) ; (i = i1) → ((y : B) → b ≡ y) }
+  e1 = λ { (i = i0) → pathToEquiv eqv2 ; (i = i1) → idEquiv ((y : B) → b ≡ y) }
+  Uhh = primGlue ((y : B) → b ≡ y) T1 e1
+      
+  uhh : Uhh
+  uhh = glue {T = T1} {e = e1} (λ { (i = i0) → Acontr ; (i = i1) → Bcontr }) λ y j → {! Bcontr y j  !}
+
+  wtf : PathP (λ i → (y : A≡B i) → a≡b i ≡ y) Acontr Bcontr
+  wtf = λ i y j → {!   !}
+
+
     -- a≡b i ≡ y
     -- ———— Boundary (wanted) —————————————————————————————————————
     -- i = i0 ⊢ λ i₁ → Acontr y i₁
@@ -40,7 +52,7 @@ lemma zero (A , a , Acontr) (B , b , Bcontr) i = A≡B i , a≡b i , eq where
   --   in {!   !}
 
 
-lemma (suc zero) (A , A-prop) (B , B-prop) x y i j = {!   !} where
+lemma (suc zero) (A , A-prop) (B , B-prop) x y i j = {!   !}
 
 lemma (suc (suc n)) x y = {!   !}
 

src/ThesisWork/Pi3S2/Step1.agda

@@ -4,6 +4,7 @@ module ThesisWork.Pi3S2.Step1 where
 
 open import Agda.Primitive
 open import Cubical.Data.Sigma
+open import Cubical.Data.Nat
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Equiv.Properties
 open import Cubical.Foundations.Isomorphism
@@ -11,8 +12,33 @@ open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.Prelude
 open import Cubical.Homotopy.Loopspace
 
+-- open import ThesisWork.Pi3S2.Lemma4-1-5 renaming (lemma to lemma4-1-5)
+
+fiberF : {l : Level} → {X∙ Y∙ : Pointed l} → (f : X∙ →∙ Y∙) → Pointed l
+fiberF {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) = 
+  fiber f y , x , f-eq
+  -- fiber f y , x , f-eq
+
 arrow∙ : {l : Level} → Type (lsuc l)
 arrow∙ {l} = Σ (Pointed l) (λ X → Σ (Pointed l) (λ Y → X →∙ Y))
 
 F : {l : Level} → arrow∙ {l} → arrow∙ {l}
-F x @ (X , Y , f) = {! fiber   !} , X , {!  fst !}
+F (X∙ @ (X , x) , Y∙ @ (Y , y) , f∙ @ (f , f-eq)) = fiberF f∙ , X∙ , fst , refl
+
+F⁻ : {l : Level} → (n : ℕ) → arrow∙ {l} → arrow∙ {l}
+F⁻ zero x = x
+F⁻ (suc n) x = F (F⁻ n x)
+
+-- Given a pointed map f∙ : X∙ →∙ Y∙, we define its fiber sequence
+-- A : ℕ → Type by Aₙ :≡ p₂(Fⁿ(X , y , f))
+
+A : {l : Level} → {X∙ Y∙ : Pointed l} → (f∙ : X∙ →∙ Y∙) → ℕ → Pointed l
+A {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) n =
+  let it = F⁻ n (X∙ , Y∙ , f∙) in
+  fst (snd it)
+
+f⁻ : {l : Level} → {X∙ Y∙ : Pointed l} → (f∙ : X∙ →∙ Y∙) → (n : ℕ) → fst (A f∙ (suc n)) → fst (A f∙ n)
+f⁻ {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ n a =
+  let it = F⁻ n (X∙ , Y∙ , f∙) in
+  {!  snd (snd it) !}
+  

src/ThesisWork/Pi3S2/SuccStr.agda

@@ -21,4 +21,14 @@ module _ where
 
   -- (ℤ , λ n . n + 1)
   ℤ-SuccStr : (i : ℤ) → (n : ℕ) → ℤ
-  ℤ-SuccStr = SuccStr ℤ zsuc
+  ℤ-SuccStr = SuccStr ℤ zsuc
+
+module _ where
+  open import Data.Fin
+  open import Data.Product
+
+  ℕ-k-SuccStr : (k : ℕ) → (ℕ × Fin k) → ℕ → (ℕ × Fin k)
+  ℕ-k-SuccStr k = SuccStr (ℕ × Fin k) inc where
+    inc : (ℕ × Fin k) → (ℕ × Fin k)
+    inc (n , k) with suc k
+    inc (n , k) | x = {!   !}

talks/2024-grads/main.tex

@@ -1,5 +1,4 @@
-
-\documentclass[a4paper]{beamer}
+\documentclass[a4paper,xcolor={dvipsnames}]{beamer}
 \useoutertheme{miniframes}
 % \usetheme{Darmstadt}
 
@@ -51,7 +50,7 @@
 
     \item What does the current state of the ecosystem look like?
     \begin{itemize}
-      \item Coq, Lean, Agda, ...
+      \item Rocq (Coq), Lean, Agda, ...
     \end{itemize}
   \end{itemize}
 \end{frame}
@@ -76,9 +75,10 @@
 \end{frame}
 
 \begin{frame}
-  \frametitle{Martin-L{\"o}f type theory}
+  \frametitle{Important features of Martin-L{\"o}f type theory}
 
   \begin{itemize}
+    \item Universes: $\mathsf{Type}_0, \mathsf{Type}_1, \mathsf{Type}_2, \dots$
     \item Inductive types
     \\
     For example, $\mathbb{N}$ is defined with one of 2 constructors: $\mathsf{zero}$ and $\mathsf{suc}$.
@@ -91,8 +91,7 @@
       \TrinaryInfC{$ \Gamma \vdash \mathsf{ind}_{\mathbb{N}} (c_0 , x . y . c_s , n) : C $}
     \end{prooftree}
 
-    \item \emph{Dependent types}, or $\Pi$-types:
-    $$ \mathsf{Vec} : (A : \mathsf{Type}) \rightarrow (n : \mathbb{N}) \rightarrow \mathsf{Type} $$
+    \item \emph{Dependent types}, or $\Pi$-types: $ \mathsf{Vec} : (A : \mathsf{Type}) \rightarrow (n : \mathbb{N}) \rightarrow \mathsf{Type} $
 
     \item \emph{Dependent sums}, or $\Sigma$-types
     \item The identity type, $\mathsf{Id}_A(x, y)$, for some $x, y : A$
@@ -107,11 +106,14 @@
 \begin{frame}
   \frametitle{Homotopy type theory}
 
+  \newcommand{\htcolor}[1]{\textcolor{Melon}{####1}}
+  \newcommand{\ttcolor}[1]{\textcolor{Periwinkle}{####1}}
+
   \begin{itemize}
-    \item A \textcolor{orange}{"homotopy"}, from algebraic topology, is a way to continuously deform one path into another ($A \times [0, 1] \rightarrow B$)
-    \item In type theory, we can imagine two functions \textcolor{blue}{$f, g : A \rightarrow B$} as being homotopic if we can inhabit $h : (x : A) \rightarrow \mathsf{Id}_B (f(x), g(x))$
+    \item A \htcolor{"homotopy"}, from algebraic topology, is a way to continuously deform one path into another ($A \times [0, 1] \rightarrow B$)
+    \item In type theory, we can imagine two functions \ttcolor{$f, g : A \rightarrow B$} as being homotopic if we can inhabit $h : (x : A) \rightarrow \mathsf{Id}_B (f(x), g(x))$
     \item Note: assume all functions are continuous.
-    \item Interpret \textcolor{orange}{paths between points in a space} as the \textcolor{blue}{identity type $\mathsf{Id}$}
+    \item Interpret \htcolor{paths between points in a space} as the \ttcolor{identity type $\mathsf{Id}$}
   \end{itemize}
 \end{frame}
 
@@ -138,8 +140,7 @@
   \frametitle{Univalence axiom?}
 
   \begin{itemize}
-    \item Unfortunately, univalence does not compute
-    \item Neither does function extensionality
+    \item Unfortunately, univalence does not compute in the "base" version of homotopy type theory, also known as Book HoTT
   \end{itemize}
 \end{frame}
 
@@ -269,6 +270,14 @@
 
 \section{Conclusion}
 
+\begin{frame}
+  \frametitle{Other type theories}
+
+  \begin{itemize}
+    \item Calculus of inductive constructions (Impredicative prop)
+  \end{itemize}
+\end{frame}
+
 \begin{frame}
   \frametitle{Conclusion}