Merge pull request #361 from Taneb/nasts-cartesian

Prove that Nat is cartesian and Natop is hence cocartesian

Author: JacquesCarette

src/Categories/Category/Instance/Nat.agda

@@ -5,22 +5,24 @@ module Categories.Category.Instance.Nat where
 
 open import Level
 
-open import Data.Fin.Base using (Fin; inject+; raise; splitAt; join)
+open import Data.Fin.Base using (Fin; inject+; raise; splitAt; join; remQuot; combine)
 open import Data.Fin.Properties
-open import Data.Nat.Base using (ℕ; _+_)
+open import Data.Nat.Base using (ℕ; _+_; _*_)
+open import Data.Product using (proj₁; proj₂; uncurry; <_,_>)
 open import Data.Sum using (inj₁; inj₂; [_,_]′)
 open import Data.Sum.Properties
 open import Relation.Binary.PropositionalEquality
-  using (_≗_; _≡_; refl; sym; trans; cong; module ≡-Reasoning; inspect; [_])
-open import Function using (id; _∘′_)
+  using (_≗_; _≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning)
+open import Function using (id; _∘′_; case_return_of_)
 
+open import Categories.Category.Cartesian using (Cartesian)
 open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
 open import Categories.Category.Cocartesian using (Cocartesian)
 open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory)
 open import Categories.Category.Core using (Category)
-open import Categories.Category.Duality using (Cocartesian⇒coCartesian)
+open import Categories.Category.Duality using (Cocartesian⇒coCartesian; coCartesian⇒Cocartesian)
 open import Categories.Object.Coproduct
-open import Categories.Object.Duality using (Coproduct⇒coProduct)
+open import Categories.Object.Duality using (Coproduct⇒coProduct; coProduct⇒Coproduct)
 open import Categories.Object.Product
 
 Nat : Category 0ℓ 0ℓ 0ℓ
@@ -60,7 +62,7 @@ Coprod m n = record
     uniq : {o : ℕ} {h : Fin (m + n) → Fin o} {f : Fin m → Fin o} {g : Fin n → Fin o} →
       h ∘′ inject+ n ≗ f → h ∘′ raise m ≗ g → (λ z → [ f , g ]′ (splitAt m z)) ≗ h
     uniq {_} {h} {f} {g} h≗f h≗g w = begin
-      [ f , g ]′ (splitAt m w)                         ≡⟨ [,]-cong (λ x → sym (h≗f x)) (λ x → sym (h≗g x)) (splitAt m w) ⟩
+      [ f , g ]′ (splitAt m w)                         ≡˘⟨ [,]-cong h≗f h≗g (splitAt m w) ⟩
       [ h ∘′ inject+ n , h ∘′ raise m ]′ (splitAt m w) ≡˘⟨ [,]-∘-distr h (splitAt m w) ⟩
       h ([ inject+ n , raise m ]′ (splitAt m w))       ≡⟨ cong h (join-splitAt m n w) ⟩
       h w                                              ∎
@@ -77,6 +79,36 @@ Nat-Cocartesian = record
   ; coproducts = record { coproduct = λ {m} {n} → Coprod m n }
   }
 
+Prod : (m n : ℕ) → Product Nat m n
+Prod m n = record
+  { A×B = m * n
+  ; π₁ = proj₁ ∘′ remQuot n
+  ; π₂ = proj₂ ∘′ remQuot {m} n
+  ; ⟨_,_⟩ = λ l r z → uncurry combine (< l , r > z)
+  ; project₁ = λ {_ f g} z → cong proj₁ (remQuot-combine (f z) (g z))
+  ; project₂ = λ {_ f g} z → cong proj₂ (remQuot-combine (f z) (g z))
+  ; unique = uniq
+  }
+  where
+    open ≡-Reasoning
+    uniq : {o : ℕ} {h : Fin o → Fin (m * n)} {f : Fin o → Fin m} {g : Fin o → Fin n} →
+      proj₁ ∘′ remQuot n ∘′ h ≗ f →  proj₂ ∘′ remQuot {m} n ∘′ h ≗ g → uncurry combine ∘′ < f , g > ≗ h
+    uniq {_} {h} {f} {g} h≗f h≗g w = begin
+      combine (f w) (g w)                                                 ≡˘⟨ cong₂ combine (h≗f w) (h≗g w) ⟩
+      combine (proj₁ (remQuot {m} n (h w))) (proj₂ (remQuot {m} n (h w))) ≡⟨ combine-remQuot {m} n (h w) ⟩
+      h w                                                                 ∎
+
+Nat-Cartesian : Cartesian Nat
+Nat-Cartesian = record
+  { terminal = record
+    { ⊤ = 1
+    ; ⊤-is-terminal = record
+      { !-unique = λ f x → case f x return (Fin.zero ≡_) of λ { Fin.zero → refl }
+      }
+    }
+  ; products = record {product = λ {m} {n} → Prod m n }
+  }
+
 -- And Natop is what is used a lot, so record some things here too
 Natop : Category 0ℓ 0ℓ 0ℓ
 Natop = Category.op Nat
@@ -89,3 +121,12 @@ Natop-Cartesian = record
   { U = Natop
   ; cartesian = Cocartesian⇒coCartesian Nat Nat-Cocartesian
   }
+
+Natop-Coprod : (m n : ℕ) → Coproduct Natop m n
+Natop-Coprod m n = coProduct⇒Coproduct Natop (Prod m n)
+
+Natop-Cocartesian : CocartesianCategory 0ℓ 0ℓ 0ℓ
+Natop-Cocartesian = record
+  { U = Natop
+  ; cocartesian = coCartesian⇒Cocartesian Natop Nat-Cartesian
+  }