From edf2393c2f7fcffdbe15a61818cb337cf3cbc786 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Wed, 16 Oct 2024 16:04:54 -0500 Subject: [PATCH] updates --- src/CubicalHott/Theorem7-1-11.agda | 20 +++++++++++++++---- src/ThesisWork/Pi3S2/Step1.agda | 28 ++++++++++++++++++++++++++- src/ThesisWork/Pi3S2/SuccStr.agda | 12 +++++++++++- talks/2024-grads/main.tex | 31 +++++++++++++++++++----------- 4 files changed, 74 insertions(+), 17 deletions(-) diff --git a/src/CubicalHott/Theorem7-1-11.agda b/src/CubicalHott/Theorem7-1-11.agda index 28bc184..e97f8bb 100644 --- a/src/CubicalHott/Theorem7-1-11.agda +++ b/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 = {! !} diff --git a/src/ThesisWork/Pi3S2/Step1.agda b/src/ThesisWork/Pi3S2/Step1.agda index c5f2f58..a90f88b 100644 --- a/src/ThesisWork/Pi3S2/Step1.agda +++ b/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 !} \ No newline at end of file +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) !} + \ No newline at end of file diff --git a/src/ThesisWork/Pi3S2/SuccStr.agda b/src/ThesisWork/Pi3S2/SuccStr.agda index 5a6d612..2cf9998 100644 --- a/src/ThesisWork/Pi3S2/SuccStr.agda +++ b/src/ThesisWork/Pi3S2/SuccStr.agda @@ -21,4 +21,14 @@ module _ where -- (ℤ , λ n . n + 1) ℤ-SuccStr : (i : ℤ) → (n : ℕ) → ℤ - ℤ-SuccStr = SuccStr ℤ zsuc \ No newline at end of file + ℤ-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 = {! !} \ No newline at end of file diff --git a/talks/2024-grads/main.tex b/talks/2024-grads/main.tex index b6db01a..31eea9d 100644 --- a/talks/2024-grads/main.tex +++ b/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}