Add some stuff about the category of cubes

Also some feedback from Thierry

src/Cat.agda

@@ -1,8 +1,8 @@
 module Cat where
 
-import Cat.Cubical
 import Cat.Category
 import Cat.Functor
+import Cat.CwF
 import Cat.Category.Pathy
 import Cat.Category.Bij
 import Cat.Category.Free
@@ -11,3 +11,4 @@ import Cat.Categories.Sets
 import Cat.Categories.Cat
 import Cat.Categories.Rel
 import Cat.Categories.Fun
+import Cat.Categories.Cube

src/Cat/Categories/Cube.agda

@@ -0,0 +1,77 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module Cat.Categories.Cube where
+
+open import Level
+open import Data.Bool hiding (T)
+open import Data.Sum hiding ([_,_])
+open import Data.Unit
+open import Data.Empty
+open import Data.Product
+open import Cubical
+open import Function
+open import Relation.Nullary
+open import Relation.Nullary.Decidable
+
+open import Cat.Category hiding (Hom)
+open import Cat.Functor
+open import Cat.Equality
+open Equality.Data.Product
+
+-- See chapter 1 for a discussion on how presheaf categories are CwF's.
+
+-- See section 6.8 in Huber's thesis for details on how to implement the
+-- categorical version of CTT
+
+open Category hiding (_∘_)
+open Functor
+
+module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
+  -- Ns is the "namespace"
+  ℓo = (suc zero ⊔ ℓ)
+
+  FiniteDecidableSubset : Set ℓ
+  FiniteDecidableSubset = Ns → Dec ⊤
+
+  isTrue : Bool → Set
+  isTrue false = ⊥
+  isTrue true = ⊤
+
+  elmsof : FiniteDecidableSubset → Set ℓ
+  elmsof P = Σ Ns (λ σ → True (P σ)) -- (σ : Ns) → isTrue (P σ)
+
+  𝟚 : Set
+  𝟚 = Bool
+
+  module _ (I J : FiniteDecidableSubset) where
+    private
+      Hom' : Set ℓ
+      Hom' = elmsof I → elmsof J ⊎ 𝟚
+      isInl : {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} → A ⊎ B → Set
+      isInl (inj₁ _) = ⊤
+      isInl (inj₂ _) = ⊥
+
+      Def : Set ℓ
+      Def = (f : Hom') → Σ (elmsof I) (λ i → isInl (f i))
+
+      rules : Hom' → Set ℓ
+      rules f = (i j : elmsof I)
+        → case (f i) of λ
+          { (inj₁ (fi , _)) → case (f j) of λ
+            { (inj₁ (fj , _)) → fi ≡ fj → i ≡ j
+            ; (inj₂ _) → Lift ⊤
+            }
+          ; (inj₂ _) → Lift ⊤
+          }
+
+    Hom = Σ Hom' rules
+
+  -- The category of names and substitutions
+  ℂ : Category ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo)
+  ℂ = record
+    { Object = FiniteDecidableSubset
+    -- { Object = Ns → Bool
+    ; Arrow = Hom
+    ; 𝟙 = λ { {o} → inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} } }
+    ; _∘_ = {!!}
+    ; isCategory = {!!}
+    }

src/Cat/Categories/Fam.agda

@@ -11,7 +11,7 @@ open import Cat.Equality
 
 open Equality.Data.Product
 
-module _ {ℓa ℓb : Level} where
+module _ (ℓa ℓb : Level) where
   private
     Obj = Σ[ A ∈ Set ℓa ] (A → Set ℓb)
     Arr : Obj → Obj → Set (ℓa ⊔ ℓb)

src/Cat/Categories/Fun.agda

@@ -76,6 +76,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
       𝔻 [ H .func→ f ∘ (θ ∘nt η) A ]     ∎
       where
         open IsCategory (𝔻 .isCategory)
+
     NatComp = _:⊕:_
 
   private

src/Cat/Category.agda

@@ -22,6 +22,7 @@ open import Cubical
 
 syntax ∃!-syntax (λ x → B) = ∃![ x ] B
 
+-- All projections must be `isProp`'s
 record IsCategory {ℓ ℓ' : Level}
   (Object : Set ℓ)
   (Arrow  : Object → Object → Set ℓ')
@@ -40,7 +41,11 @@ record Category (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
   -- adding no-eta-equality can speed up type-checking.
   no-eta-equality
   field
+    -- Need something like:
+    -- Object : Σ (Set ℓ) isGroupoid
     Object : Set ℓ
+    -- And:
+    -- Arrow  : Object → Object → Σ (Set ℓ') isSet
     Arrow  : Object → Object → Set ℓ'
     𝟙      : {o : Object} → Arrow o o
     _∘_    : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
@@ -59,6 +64,8 @@ _[_,_] = Arrow
 _[_∘_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → {A B C : ℂ .Object} → (g : ℂ [ B , C ]) → (f : ℂ [ A , B ]) → ℂ [ A , C ]
 _[_∘_] = _∘_
 
+
+
 module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} where
   module _ { A B : ℂ .Object } where
     Isomorphism : (f : ℂ .Arrow A B) → Set ℓ'
@@ -180,3 +187,19 @@ record CartesianClosed {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ
   field
     {{hasProducts}}     : HasProducts ℂ
     {{hasExponentials}} : HasExponentials ℂ
+
+module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+  unique = isContr
+
+  IsInitial : ℂ .Object → Set (ℓa ⊔ ℓb)
+  IsInitial I = {X : ℂ .Object} → unique (ℂ .Arrow I X)
+
+  IsTerminal : ℂ .Object → Set (ℓa ⊔ ℓb)
+  -- ∃![ ? ] ?
+  IsTerminal T = {X : ℂ .Object} → unique (ℂ .Arrow X T)
+
+  Initial : Set (ℓa ⊔ ℓb)
+  Initial = Σ (ℂ .Object) IsInitial
+
+  Terminal : Set (ℓa ⊔ ℓb)
+  Terminal = Σ (ℂ .Object) IsTerminal

src/Cat/Category/Properties.agda

@@ -49,9 +49,14 @@ epi-mono-is-not-iso f =
   in {!!}
 -}
 
-module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
-  open import Cat.Category
-  open Category
+open import Cat.Category
+open Category
+open import Cat.Functor
+open Functor
+
+module _ {ℓ : Level} {ℂ : Category ℓ ℓ}
+  {isSObj : isSet (ℂ .Object)}
+  {isz2 : ∀ {ℓ} → {A B : Set ℓ} → isSet (Sets [ A , B ])} where
   open import Cat.Categories.Cat using (Cat)
   open import Cat.Categories.Fun
   open import Cat.Categories.Sets
@@ -82,7 +87,23 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
 
       eqNat : (λ i → Natural (prshf c) (prshf c) (eqTrans i))
         [(λ _ → funExt (λ _ → ℂ.assoc)) ≡ identityNatural (prshf c)]
-      eqNat = {!!}
+      eqNat = λ i {A} {B} f →
+        let
+         open IsCategory (Sets .isCategory)
+         lemm : (Sets [ eqTrans i B ∘ prshf c .func→ f ]) ≡
+           (Sets [ prshf c .func→ f ∘ eqTrans i A ])
+         lemm = {!!}
+         lem : (λ _ → Sets [ Functor.func* (prshf c) A , prshf c .func* B ])
+                [ Sets [ eqTrans i B ∘ prshf c .func→ f ]
+                ≡ Sets [ prshf c .func→ f ∘ eqTrans i A ] ]
+         lem
+          = isz2 _ _ lemm _ i
+            -- (Sets [ eqTrans i B ∘ prshf c .func→ f ])
+            -- (Sets [ prshf c .func→ f ∘ eqTrans i A ])
+            -- lemm
+            -- _ i
+        in
+          lem
       -- eqNat = λ {A} {B} i ℂ[B,A] i' ℂ[A,c] →
       --   let
       --     k : ℂ [ {!!} , {!!} ]

src/Cat/Cubical.agda

@@ -1,69 +0,0 @@
-{-# OPTIONS --allow-unsolved-metas #-}
-module Cat.Cubical where
-
-open import Agda.Primitive
-open import Data.Bool
-open import Data.Product
-open import Data.Sum
-open import Data.Unit
-open import Data.Empty
-open import Data.Product
-open import Function
-open import Cubical
-
-open import Cat.Category
-open import Cat.Functor
-open import Cat.Categories.Fam
-
--- See chapter 1 for a discussion on how presheaf categories are CwF's.
-
--- See section 6.8 in Huber's thesis for details on how to implement the
--- categorical version of CTT
-
-open Category hiding (_∘_)
-open Functor
-
-module CwF {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
-  Contexts = ℂ .Object
-  Substitutions = ℂ .Arrow
-
-  record CwF : Set {!ℓa ⊔ ℓb!} where
-    field
-      Terms : Functor (Opposite ℂ) Fam
-
-module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
-  -- Ns is the "namespace"
-  ℓo = (lsuc lzero ⊔ ℓ)
-
-  FiniteDecidableSubset : Set ℓ
-  FiniteDecidableSubset = Ns → Bool
-
-  isTrue : Bool → Set
-  isTrue false = ⊥
-  isTrue true = ⊤
-
-  elmsof : (Ns → Bool) → Set ℓ
-  elmsof P = (σ : Ns) → isTrue (P σ)
-
-  𝟚 : Set
-  𝟚 = Bool
-
-  module _ (I J : FiniteDecidableSubset) where
-    private
-      themap : Set {!!}
-      themap = elmsof I → elmsof J ⊎ 𝟚
-      rules : (elmsof I → elmsof J ⊎ 𝟚) → Set
-      rules f = (i j : elmsof I) → {!!}
-
-    Mor = Σ themap rules
-
-  -- The category of names and substitutions
-  ℂ : Category ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo)
-  ℂ = record
-    -- { Object = FiniteDecidableSubset
-    { Object = Ns → Bool
-    ; Arrow = Mor
-    ; 𝟙 = {!!}
-    ; _∘_ = {!!}
-    ; isCategory = {!!}
-    }

src/Cat/CwF.agda

@@ -0,0 +1,55 @@
+module Cat.CwF where
+
+open import Agda.Primitive
+open import Data.Product
+
+open import Cat.Category
+open import Cat.Functor
+open import Cat.Categories.Fam
+
+open Category
+open Functor
+
+module _ {ℓa ℓb : Level} where
+  record CwF : Set (lsuc (ℓa ⊔ ℓb)) where
+    -- "A category with families consists of"
+    field
+      -- "A base category"
+      ℂ : Category ℓa ℓb
+    -- It's objects are called contexts
+    Contexts = ℂ .Object
+    -- It's arrows are called substitutions
+    Substitutions = ℂ .Arrow
+    field
+      -- A functor T
+      T : Functor (Opposite ℂ) (Fam ℓa ℓb)
+      -- Empty context
+      [] : Terminal ℂ
+    Type : (Γ : ℂ .Object) → Set ℓa
+    Type Γ = proj₁ (T .func* Γ)
+
+    module _ {Γ : ℂ .Object} {A : Type Γ} where
+
+      module _ {A B : ℂ .Object} {γ : ℂ [ A , B ]} where
+        k : Σ (proj₁ (func* T B) → proj₁ (func* T A))
+          (λ f →
+          {x : proj₁ (func* T B)} →
+          proj₂ (func* T B) x → proj₂ (func* T A) (f x))
+        k = T .func→ γ
+        k₁ : proj₁ (func* T B) → proj₁ (func* T A)
+        k₁ = proj₁ k
+        k₂ : ({x : proj₁ (func* T B)} →
+          proj₂ (func* T B) x → proj₂ (func* T A) (k₁ x))
+        k₂ = proj₂ k
+
+      record ContextComprehension : Set (ℓa ⊔ ℓb) where
+        field
+          Γ&A : ℂ .Object
+          proj1 : ℂ .Arrow Γ&A Γ
+          -- proj2 : ????
+
+        -- if γ : ℂ [ A , B ]
+        -- then T .func→ γ (written T[γ]) interpret substitutions in types and terms respectively.
+        -- field
+        --   ump : {Δ : ℂ .Object} → (γ : ℂ [ Δ , Γ ])
+        --     → (a : {!!}) → {!!}