Merge branch 'dev'

libs/agda-stdlib

@@ -1 +1 @@
-Subproject commit 2033814d1f118401a37484390fdb5b75b83e6bb4
+Subproject commit de23244a73d6dab55715fd5a107a5de805c55764

libs/cubical

@@ -1 +1 @@
-Subproject commit 19990b03b95f76210362a6e55b94181a5481f158
+Subproject commit a83f5f4c63e5dfd8143ac03163868c63a56802de

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}}

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.

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}

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)

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)

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

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

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}

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 = {!!}
     }