Merge pull request #339 from Trebor-Huang/ccf

Add bundled CCCs and basic def. for CC functors.

src/Categories/Category/CartesianClosed/Bundle.agda

@@ -0,0 +1,23 @@
+{-# OPTIONS --without-K --safe #-}
+
+-- Bundled version of a Cartesian Closed Category
+module Categories.Category.CartesianClosed.Bundle where
+
+open import Level
+
+open import Categories.Category.Core using (Category)
+open import Categories.Category.CartesianClosed using (CartesianClosed)
+open import Categories.Category.Cartesian.Bundle
+
+record CartesianClosedCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
+  field
+    U         : Category o ℓ e  -- U for underlying
+    cartesianClosed : CartesianClosed U
+
+  open Category U public
+
+  cartesianCategory : CartesianCategory o ℓ e
+  cartesianCategory = record
+    { U = U
+    ; cartesian = CartesianClosed.cartesian cartesianClosed
+    }

src/Categories/Functor/CartesianClosed.agda

@@ -0,0 +1,44 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Categories.Functor.CartesianClosed where
+
+open import Level
+
+open import Categories.Category.CartesianClosed.Bundle using (CartesianClosedCategory)
+open import Categories.Category.CartesianClosed using (CartesianClosed)
+open import Categories.Functor using (Functor; _∘F_)
+open import Categories.Functor.Cartesian using (IsCartesianF)
+
+import Categories.Morphism as M
+
+private
+  variable
+    o ℓ e o′ ℓ′ e′ : Level
+
+record IsCartesianClosedF (C : CartesianClosedCategory o ℓ e) (D : CartesianClosedCategory o′ ℓ′ e′)
+  (F : Functor (CartesianClosedCategory.U C) (CartesianClosedCategory.U D)) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
+  private
+    module C = CartesianClosedCategory C using (cartesianCategory; cartesianClosed)
+    module D = CartesianClosedCategory D using (cartesianCategory; cartesianClosed; _⇒_; _∘_; U)
+    module CC = CartesianClosed C.cartesianClosed using (_^_; eval′)
+    module DC = CartesianClosed D.cartesianClosed using (_^_; λg)
+  field
+    F-cartesian : IsCartesianF C.cartesianCategory D.cartesianCategory F
+  open Functor F
+  open IsCartesianF F-cartesian
+  F-mor : ∀ A B → F₀ (A CC.^ B) D.⇒ F₀ A DC.^ F₀ B
+  F-mor A B = DC.λg (F₁ CC.eval′ D.∘ ×-iso.to (A CC.^ B) B)
+  field
+    F-closed : ∀ {A B} → M.IsIso D.U (F-mor A B)
+
+record CartesianClosedF (C : CartesianClosedCategory o ℓ e) (D : CartesianClosedCategory o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
+  private
+    module C = CartesianClosedCategory C
+    module D = CartesianClosedCategory D
+
+  field
+    F                 : Functor C.U D.U
+    isCartesianClosed : IsCartesianClosedF C D F
+
+  open Functor F public
+  open IsCartesianClosedF isCartesianClosed public