Have yoneda without having a category of categories

I did break some things in Cat.Categories.Cat but since this is
unprovable anyways it's not that big a deal.

src/Cat/Categories/Cat.agda

@@ -11,7 +11,7 @@ open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
 open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Category.Product
-open import Cat.Category.Exponential
+open import Cat.Category.Exponential hiding (_×_ ; product)
 open import Cat.Category.NaturalTransformation
 
 open import Cat.Equality
@@ -174,22 +174,19 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
     hasProducts = record { product = product }
 
 -- Basically proves that `Cat ℓ ℓ` is cartesian closed.
-module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
+module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
-  private
   open Data.Product
   open import Cat.Categories.Fun
 
-    Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ)
+  Categoryℓ = Category ℓ ℓ
-    Catℓ = Cat ℓ ℓ unprovable
-    module _ (ℂ 𝔻 : Category ℓ ℓ) where
   open Fun ℂ 𝔻 renaming (identity to idN)
   private
-        :obj: : Object Catℓ
-        :obj: = Fun
-
     :func*: : Functor ℂ 𝔻 × Object ℂ → Object 𝔻
     :func*: (F , A) = func* F A
 
+  prodObj : Categoryℓ
+  prodObj = Fun
+
   module _ {dom cod : Functor ℂ 𝔻 × Object ℂ} where
     private
       F : Functor ℂ 𝔻
@@ -226,7 +223,7 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
         result : 𝔻 [ func* F A , func* G B ]
         result = l
 
-      _×p_ = product unprovable
+  open CatProduct renaming (obj to _×p_) using ()
 
   module _ {c : Functor ℂ 𝔻 × Object ℂ} where
     private
@@ -244,7 +241,7 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
 
     :ident: : :func→: {c} {c} (NT.identity F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻
     :ident: = begin
-          :func→: {c} {c} (𝟙 (Product.obj (:obj: ×p ℂ)) {c}) ≡⟨⟩
+      :func→: {c} {c} (𝟙 (prodObj ×p ℂ) {c})    ≡⟨⟩
       :func→: {c} {c} (idN F , 𝟙 ℂ)             ≡⟨⟩
       𝔻 [ identityTrans F C ∘ func→ F (𝟙 ℂ)]    ≡⟨⟩
       𝔻 [ 𝟙 𝔻 ∘ func→ F (𝟙 ℂ)]                  ≡⟨ proj₂ 𝔻.isIdentity ⟩
@@ -262,7 +259,7 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
     H = H×C .proj₁
     C = H×C .proj₂
     -- Not entirely clear what this is at this point:
-        _P⊕_ = Category._∘_ (Product.obj (:obj: ×p ℂ)) {F×A} {G×B} {H×C}
+    _P⊕_ = Category._∘_ (prodObj ×p ℂ) {F×A} {G×B} {H×C}
     module _
       -- NaturalTransformation F G × ℂ .Arrow A B
       {θ×f : NaturalTransformation F G × ℂ [ A , B ]}
@@ -314,8 +311,9 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
           open Category 𝔻
           module H = Functor H
 
-      :eval: : Functor ((:obj: ×p ℂ) .Product.obj) 𝔻
+  eval : Functor (CatProduct.obj prodObj ℂ) 𝔻
-      :eval: = record
+  -- :eval: : Functor (prodObj ×p ℂ) 𝔻
+  eval = record
     { raw = record
       { func* = :func*:
       ; func→ = λ {dom} {cod} → :func→: {dom} {cod}
@@ -326,12 +324,16 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
       }
     }
 
-      module _ (𝔸 : Category ℓ ℓ) (F : Functor ((𝔸 ×p ℂ) .Product.obj) 𝔻) where
+  module _ (𝔸 : Category ℓ ℓ) (F : Functor (𝔸 ×p ℂ) 𝔻) where
-        open HasProducts (hasProducts {ℓ} {ℓ} unprovable) renaming (_|×|_ to parallelProduct)
+    -- open HasProducts (hasProducts {ℓ} {ℓ} unprovable) renaming (_|×|_ to parallelProduct)
 
     postulate
-          transpose : Functor 𝔸 :obj:
+      parallelProduct
-          eq : Catℓ [ :eval: ∘ (parallelProduct transpose (𝟙 Catℓ {A = ℂ})) ] ≡ F
+        : Functor 𝔸 prodObj → Functor ℂ ℂ
+        → Functor (𝔸 ×p ℂ) (prodObj ×p ℂ)
+      transpose : Functor 𝔸 prodObj
+      eq : F[ eval ∘ (parallelProduct transpose (identity {C = ℂ})) ] ≡ F
+      -- eq : F[ :eval: ∘ {!!} ] ≡ F
       -- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F
       -- eq' : (Catℓ [ :eval: ∘
       --   (record { product = product } HasProducts.|×| transpose)
@@ -344,20 +346,39 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
     -- :eval: ∘ (parallelProduct F~ (𝟙 Catℓ {o = ℂ}))] ≡ F) catTranspose =
     -- transpose , eq
 
-      postulate :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval:
+module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
-      -- :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval:
+  private
-      -- :isExponential: = {!catTranspose!}
+    Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ)
-      --   where
+    Catℓ = Cat ℓ ℓ unprovable
-      --     open HasProducts (hasProducts {ℓ} {ℓ} unprovable) using (_|×|_)
+  module _ (ℂ 𝔻 : Category ℓ ℓ) where
-      -- :isExponential: = λ 𝔸 F → transpose 𝔸 F , eq' 𝔸 F
+    open CatExponential ℂ 𝔻 using (prodObj ; eval)
+    -- Putting in the type annotation causes Agda to loop indefinitely.
+    -- eval' : Functor (CatProduct.obj prodObj ℂ) 𝔻
+    -- Likewise, using it below also results in this.
+    eval' : _
+    eval' = eval
+  --   private
+  --     -- module _ (ℂ 𝔻 : Category ℓ ℓ) where
+  --       postulate :isExponential: : IsExponential Catℓ ℂ 𝔻 prodObj :eval:
+  --       -- :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval:
+  --       -- :isExponential: = {!catTranspose!}
+  --       --   where
+  --       --     open HasProducts (hasProducts {ℓ} {ℓ} unprovable) using (_|×|_)
+  --       -- :isExponential: = λ 𝔸 F → transpose 𝔸 F , eq' 𝔸 F
 
-      -- :exponent: : Exponential (Cat ℓ ℓ) A B
+  --       -- :exponent: : Exponential (Cat ℓ ℓ) A B
-      :exponent: : Exponential Catℓ ℂ 𝔻
+    exponent : Exponential Catℓ ℂ 𝔻
-      :exponent: = record
+    exponent = record
-        { obj = :obj:
+      { obj = prodObj
-        ; eval = :eval:
+      ; eval = {!evalll'!}
-        ; isExponential = :isExponential:
+      ; isExponential = {!:isExponential:!}
       }
+      where
+        open HasProducts (hasProducts unprovable) renaming (_×_ to _×p_)
+        open import Cat.Categories.Fun
+        open Fun
+        -- _×p_ = CatProduct.obj -- prodObj ℂ
+        -- eval' : Functor CatP.obj 𝔻
 
   hasExponentials : HasExponentials Catℓ
-  hasExponentials = record { exponent = :exponent: }
+  hasExponentials = record { exponent = exponent }

src/Cat/Category/Exponential.agda

@@ -1,40 +1,44 @@
 module Cat.Category.Exponential where
 
 open import Agda.Primitive
-open import Data.Product
+open import Data.Product hiding (_×_)
 open import Cubical
 
 open import Cat.Category
 open import Cat.Category.Product
 
-open Category
-
 module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} where
-  open HasProducts hasProducts
+  open Category ℂ
-  open Product hiding (obj)
+  open HasProducts hasProducts public
-  private
-    _×p_ : (A B : Object ℂ) → Object ℂ
-    _×p_ A B = Product.obj (product A B)
 
-  module _ (B C : Object ℂ) where
+  module _ (B C : Object) where
-    IsExponential : (Cᴮ : Object ℂ) → ℂ [ Cᴮ ×p B , C ] → Set (ℓ ⊔ ℓ')
+    record IsExponential'
-    IsExponential Cᴮ eval = ∀ (A : Object ℂ) (f : ℂ [ A ×p B , C ])
+      (Cᴮ : Object)
+      (eval : ℂ [ Cᴮ × B , C ]) : Set (ℓ ⊔ ℓ') where
+      field
+        uniq
+          : ∀ (A : Object) (f : ℂ [ A × B , C ])
+          → ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.𝟙 ℂ ] ≡ f)
+
+    IsExponential : (Cᴮ : Object) → ℂ [ Cᴮ × B , C ] → Set (ℓ ⊔ ℓ')
+    IsExponential Cᴮ eval = ∀ (A : Object) (f : ℂ [ A × B , C ])
       → ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.𝟙 ℂ ] ≡ f)
 
     record Exponential : Set (ℓ ⊔ ℓ') where
       field
         -- obj ≡ Cᴮ
-        obj : Object ℂ
+        obj : Object
-        eval : ℂ [ obj ×p B , C ]
+        eval : ℂ [ obj × B , C ]
         {{isExponential}} : IsExponential obj eval
-      -- If I make this an instance-argument then the instance resolution
+
-      -- algorithm goes into an infinite loop. Why?
+      transpose : (A : Object) → ℂ [ A × B , C ] → ℂ [ A , obj ]
-      exponentialsHaveProducts : HasProducts ℂ
-      exponentialsHaveProducts = hasProducts
-      transpose : (A : Object ℂ) → ℂ [ A ×p B , C ] → ℂ [ A , obj ]
       transpose A f = proj₁ (isExponential A f)
 
 record HasExponentials {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {{_ : HasProducts ℂ}} : Set (ℓ ⊔ ℓ') where
+  open Category ℂ
   open Exponential public
   field
-    exponent : (A B : Object ℂ) → Exponential ℂ A B
+    exponent : (A B : Object) → Exponential ℂ A B
+
+  _⇑_ : (A B : Object) → Object
+  A ⇑ B = (exponent A B) .obj

src/Cat/Category/Monoid.agda

@@ -27,9 +27,10 @@ module _ (ℓa ℓb : Level) where
     open Category category public
     field
       {{hasProducts}} : HasProducts category
-      mempty  : Object
+      empty  : Object
       -- aka. tensor product, monoidal product.
-      mappend : Functor (category × category) category
+      append : Functor (category × category) category
+    open HasProducts hasProducts public
 
   record MonoidalCategory : Set ℓ where
     field
@@ -40,10 +41,10 @@ module _ {ℓa ℓb : Level} (ℂ : MonoidalCategory ℓa ℓb) where
   private
     ℓ = ℓa ⊔ ℓb
 
-  module MC = MonoidalCategory ℂ
+  open MonoidalCategory ℂ public
-  open HasProducts MC.hasProducts
+
   record Monoid : Set ℓ where
     field
-      carrier : MC.Object
+      carrier : Object
-      mempty  : MC.Arrow (carrier × carrier)  carrier
+      mempty  : Arrow empty carrier
-      mappend : MC.Arrow MC.mempty carrier
+      mappend : Arrow (carrier × carrier) carrier

src/Cat/Category/Product.agda

@@ -31,6 +31,7 @@ record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : Object ℂ) :
     proj₂ : ℂ [ obj , B ]
     {{isProduct}} : IsProduct ℂ proj₁ proj₂
 
+  -- | Arrow product
   _P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ])
     → ℂ [ X , obj ]
   _P[_×_] π₁ π₂ = proj₁ (isProduct π₁ π₂)
@@ -39,16 +40,21 @@ record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔
   field
     product : ∀ (A B : Object ℂ) → Product {ℂ = ℂ} A B
 
-  open Product
+  open Product hiding (obj)
 
-  _×_ : (A B : Object ℂ) → Object ℂ
+  module _ (A B : Object ℂ) where
-  A × B = Product.obj (product A B)
+    open Product (product A B)
-  -- The product mentioned in awodey in Def 6.1 is not the regular product of arrows.
+    _×_ : Object ℂ
-  -- It's a "parallel" product
+    _×_ = obj
-  _|×|_ : {A A' B B' : Object ℂ} → ℂ [ A , A' ] → ℂ [ B , B' ]
+
-    → ℂ [ A × B , A' × B' ]
+  -- | Parallel product of arrows
-  _|×|_ {A = A} {A' = A'} {B = B} {B' = B'} a b
+  --
-    = product A' B'
+  -- The product mentioned in awodey in Def 6.1 is not the regular product of
-      P[ ℂ [ a ∘ (product A B) .proj₁ ]
+  -- arrows. It's a "parallel" product
-      ×  ℂ [ b ∘ (product A B) .proj₂ ]
+  module _ {A A' B B' : Object ℂ} where
+    open Product (product A B) hiding (_P[_×_]) renaming (proj₁ to fst ; proj₂ to snd)
+    _|×|_ : ℂ [ A , A' ] → ℂ [ B , B' ] → ℂ [ A × B , A' × B' ]
+    a |×| b = product A' B'
+      P[ ℂ [ a ∘ fst ]
+      ×  ℂ [ b ∘ snd ]
       ]

src/Cat/Category/Yoneda.agda

@@ -15,7 +15,7 @@ open Equality.Data.Product
 -- category of categories (since it doesn't exist).
 open import Cat.Categories.Cat using (RawCat)
 
-module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat ℓ ℓ)) where
+module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
   private
     open import Cat.Categories.Fun
     open import Cat.Categories.Sets
@@ -24,15 +24,17 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat
     open Functor
     𝓢 = Sets ℓ
     open Fun (opposite ℂ) 𝓢
-    Catℓ : Category _ _
-    Catℓ = Cat.Cat ℓ ℓ unprovable
     prshf = presheaf ℂ
     module ℂ = Category ℂ
 
-    _⇑_ : (A B : Category.Object Catℓ) → Category.Object Catℓ
+    -- There is no (small) category of categories. So we won't use _⇑_ from
-    A ⇑ B = (exponent A B) .obj
+    -- `HasExponential`
-      where
+    --
-        open HasExponentials (Cat.hasExponentials ℓ unprovable)
+    --     open HasExponentials (Cat.hasExponentials ℓ unprovable) using (_⇑_)
+    --
+    -- In stead we'll use an ad-hoc definition -- which is definitionally
+    -- equivalent to that other one.
+    _⇑_ = Cat.CatExponential.prodObj
 
     module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where
       :func→: : NaturalTransformation (prshf A) (prshf B)