diff --git a/libs/agda-stdlib b/libs/agda-stdlib index 2033814..de23244 160000 --- a/libs/agda-stdlib +++ b/libs/agda-stdlib @@ -1 +1 @@ -Subproject commit 2033814d1f118401a37484390fdb5b75b83e6bb4 +Subproject commit de23244a73d6dab55715fd5a107a5de805c55764 diff --git a/libs/cubical b/libs/cubical index 19990b0..a83f5f4 160000 --- a/libs/cubical +++ b/libs/cubical @@ -1 +1 @@ -Subproject commit 19990b03b95f76210362a6e55b94181a5481f158 +Subproject commit a83f5f4c63e5dfd8143ac03163868c63a56802de diff --git a/proposal/macros.tex b/proposal/macros.tex index aec0c67..a092514 100644 --- a/proposal/macros.tex +++ b/proposal/macros.tex @@ -6,8 +6,8 @@ \newcommand{\bN}{\mathbb{N}} \newcommand{\bC}{\mathbb{C}} \newcommand{\bX}{\mathbb{X}} -\newcommand{\to}{\rightarrow}} -\newcommand{\mto}{\mapsto}} +\newcommand{\to}{\rightarrow} +\newcommand{\mto}{\mapsto} \newcommand{\UU}{\ensuremath{\mathcal{U}}\xspace} \let\type\UU \newcommand{\nomen}[1]{\emph{#1}} diff --git a/proposal/planning.tex b/proposal/planning.tex new file mode 100644 index 0000000..91d7cc6 --- /dev/null +++ b/proposal/planning.tex @@ -0,0 +1,72 @@ +\section{Planning report} +% +I have already implemented multiple essential building blocks for a +formalization of core-category theory. These concepts include: +% +\begin{itemize} +\item +Categories +\item +Functors +\item +Products +\item +Exponentials +\item +Natural transformations +\item +Concrete Categories +\subitem +Sets +\subitem +Cat +\subitem +Functor +\end{itemize} +% +Will all these things already in place it's my assessment that I am ahead of +schedule at this point.\footnote{I have omitted a lot of other things that + follow easily from the above, e.g. a cartesian-closed category is simply one + that has all products and exponentials.} + +Here is a plan for my thesis work organized on a week-by-week basis. +% +\begin{center} +\centering +\begin{tabular}{@{}lll@{}} +Goal & Deadline & Risk 1-5 \\ \hline +Yoneda embedding & Feb 2nd & 3 \\ +Categories with families & Feb 9th & 4 \\ +Presheafs $\Rightarrow$ CwF's & Feb 16th & 2 \\ +Cubical Category & Feb 23rd & 3 \\ +Writing seminar & Mar 2nd & \\ +Kan condition & Mar 9th & 4 \\ +Thesis outline and backlog & Mar 16th & 2 \\ +Half-time report & Mar 23rd & 2 \\ + & Mar 30th & \\ + & Apr 6th & \\ + & Apr 13th & \\ + & Apr 20th & \\ +Thesis draft & Apr 27th & 2 \\ +Writing seminar 2 & May 4th & \\ +Presentation & May 11th & \\ +Attend 1st presentation & May 18th & \\ +Attend 2nd presentation & May 25th & \\ +\end{tabular} +\end{center} +% +The first half part of my thesis-work will be focused on implementing core +elements of my Agda implementation. These core elements have been highlighted in +the above table. The elements noted there are the essential bits and pieces I +need to reach the ambitious goal of getting an implementation of a categorical +model for Cubical Type Theory. Along the way I will also have formalized +additional elements of more ``pure'' category theory. I will thus reach my goal +of formalizing (parts of) category theory. + +The high risk-factors for CwF's and the Kan-condition is due to this being +somewhat uncharted territory for me at this point. + +It's my plan that I will have formalized the core concepts needed around the +deadline for the half-time report which is due by March 23rd. Around this point +I will have a clearer idea of what additional things I need for a model of +category theory. diff --git a/proposal/proposal.tex b/proposal/proposal.tex index 7237479..c6cb67d 100644 --- a/proposal/proposal.tex +++ b/proposal/proposal.tex @@ -12,6 +12,7 @@ \usepackage{parskip} \usepackage{multicol} \usepackage{amsmath,amssymb} +\usepackage[toc,page]{appendix} % \setlength{\parskip}{10pt} % \usepackage{tikz} @@ -279,4 +280,7 @@ The thesis shall conclude with a discussion about the benefits of Cubical Agda. \nocite{cubical-demo} \nocite{coquand-2013} \bibliography{refs} +\begin{appendices} +\input{planning.tex} +\end{appendices} \end{document} diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda index b398aa9..42d63ab 100644 --- a/src/Cat/Categories/Rel.agda +++ b/src/Cat/Categories/Rel.agda @@ -1,7 +1,7 @@ {-# OPTIONS --cubical #-} module Cat.Categories.Rel where -open import Cubical.PathPrelude +open import Cubical open import Cubical.GradLemma open import Agda.Primitive open import Data.Product renaming (proj₁ to fst ; proj₂ to snd) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 98750cf..181512c 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -1,6 +1,6 @@ module Cat.Categories.Sets where -open import Cubical.PathPrelude +open import Cubical open import Agda.Primitive open import Data.Product open import Data.Product renaming (proj₁ to fst ; proj₂ to snd) diff --git a/src/Cat/Category/Bij.agda b/src/Cat/Category/Bij.agda index 0892f55..c611c6c 100644 --- a/src/Cat/Category/Bij.agda +++ b/src/Cat/Category/Bij.agda @@ -2,7 +2,7 @@ module Cat.Category.Bij where -open import Cubical.PathPrelude hiding ( Id ) +open import Cubical hiding ( Id ) open import Cubical.FromStdLib module _ {A : Set} {a : A} {P : A → Set} where diff --git a/src/Cat/Category/Free.agda b/src/Cat/Category/Free.agda index ff06743..5686356 100644 --- a/src/Cat/Category/Free.agda +++ b/src/Cat/Category/Free.agda @@ -1,7 +1,7 @@ module Cat.Category.Free where open import Agda.Primitive -open import Cubical.PathPrelude hiding (Path) +open import Cubical hiding (Path) open import Data.Product open import Cat.Category as C diff --git a/src/Cat/Category/Pathy.agda b/src/Cat/Category/Pathy.agda index e33a2ca..2764999 100644 --- a/src/Cat/Category/Pathy.agda +++ b/src/Cat/Category/Pathy.agda @@ -3,7 +3,7 @@ module Cat.Category.Pathy where open import Level -open import Cubical.PathPrelude +open import Cubical {- module _ {ℓ ℓ'} {A : Set ℓ} {x : A} diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index 6edaca1..ff7d0ec 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -4,7 +4,7 @@ module Cat.Category.Properties where open import Agda.Primitive open import Data.Product -open import Cubical.PathPrelude +open import Cubical open import Cat.Category open import Cat.Functor @@ -58,35 +58,35 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where open Exponential private Catℓ = Cat ℓ ℓ + prshf = presheaf {ℂ = ℂ} - -- Exp : Set (lsuc (lsuc ℓ)) - -- Exp = Exponential (Cat (lsuc ℓ) ℓ) - -- Sets (Opposite ℂ) + -- Exp : Set (lsuc (lsuc ℓ)) + -- Exp = Exponential (Cat (lsuc ℓ) ℓ) + -- Sets (Opposite ℂ) - _⇑_ : (A B : Catℓ .Object) → Catℓ .Object - A ⇑ B = (exponent A B) .obj - where - open HasExponentials (Cat.hasExponentials ℓ) + _⇑_ : (A B : Catℓ .Object) → Catℓ .Object + A ⇑ B = (exponent A B) .obj + where + open HasExponentials (Cat.hasExponentials ℓ) - -- private - -- -- I need `Sets` to be a `Category ℓ ℓ` but it simlpy isn't. - -- Setz : Category ℓ ℓ - -- Setz = {!Sets!} - -- :func*: : ℂ .Object → (Setz ⇑ Opposite ℂ) .Object - -- :func*: A = {!!} + module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where + :func→: : NaturalTransformation (prshf A) (prshf B) + :func→: = (λ C x → (ℂ ._⊕_ f x)) , λ f₁ → funExt λ x → lem + where + lem = (ℂ .isCategory) .IsCategory.assoc + module _ {c : ℂ .Object} where + eqTrans : (:func→: (ℂ .𝟙 {c})) .proj₁ ≡ (Fun .𝟙 {o = prshf c}) .proj₁ + eqTrans = funExt λ x → funExt λ x → ℂ .isCategory .IsCategory.ident .proj₂ + eqNat : (i : I) → Natural (prshf c) (prshf c) (eqTrans i) + eqNat i f = {!!} - -- prsh = presheaf {ℂ = ℂ} - -- k = prsh {!!} - -- :func*:' : ℂ .Object → Presheaf ℂ - -- :func*:' = prsh - -- module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where - -- open import Cat.Categories.Fun - -- :func→:' : NaturalTransformation (prsh A) (prsh B) + :ident: : (:func→: (ℂ .𝟙 {c})) ≡ (Fun .𝟙 {o = prshf c}) + :ident: i = eqTrans i , eqNat i yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = Sets {ℓ}}) yoneda = record - { func* = presheaf {ℂ = ℂ} - ; func→ = {!!} - ; ident = {!!} + { func* = prshf + ; func→ = :func→: + ; ident = :ident: ; distrib = {!!} }