agda/examples/outdated-and-incorrect/cat/Product.agda

module Product where

open import Base
open import Category
open import Unique
open import Dual

module Prod (ℂ : Cat) where

  private
    ℂ' = η-Cat ℂ
    open module C = Cat ℂ'
    open module U = Uniq ℂ'

  data _×_ (A B : Obj) : Set1 where
    prod : (AB : Obj)
           (π₀ : AB ─→ A)
           (π₁ : AB ─→ B) ->
           ((X : Obj)(f : X ─→ A)(g : X ─→ B) ->
            ∃! \(h : X ─→ AB) -> π₀ ∘ h == f /\ π₁ ∘ h == g
           ) -> A × B

  Product : {A B : Obj} -> A × B -> Obj
  Product (prod AB _ _ _) = AB

  π₀ : {A B : Obj}(p : A × B) -> Product p ─→ A
  π₀ (prod _ p _ _) = p

  π₁ : {A B : Obj}(p : A × B) -> Product p ─→ B
  π₁ (prod _ _ q _) = q

module Sum (ℂ : Cat) = Prod (η-Cat ℂ op)
    renaming ( _×_     to _+_
             ; prod    to sum
             ; Product to Sum
             ; π₀      to inl
             ; π₁      to inr
             )