Permalink
Browse files

Merge branch 'master' into quotients

  • Loading branch information...
2 parents 870ee66 + 7fe57b1 commit e8bb3a43c748f27ff7790cdb3b44fb912d175b04 @copumpkin committed May 11, 2012
Showing with 32 additions and 0 deletions.
  1. +32 −0 Categories/Agda/Product.agda
@@ -0,0 +1,32 @@
+module Categories.Agda.Product where
+
+open import Categories.Category
+open import Categories.Agda
+import Categories.Object.Product as P
+import Categories.Object.BinaryProducts as BP
+
+open import Data.Product
+open import Relation.Binary.PropositionalEquality
+
+private
+ module Dummywhere
+ open P (Sets ℓ)
+ open BP (Sets ℓ)
+
+ binaryProducts : BinaryProducts
+ binaryProducts = record
+ { product = λ {A} {B} record
+ { A×B = A × B
+ ; π₁ = proj₁
+ ; π₂ = proj₂
+ ; ⟨_,_⟩ = <_,_>
+ ; commute₁ = refl
+ ; commute₂ = refl
+ ; universal = universal′
+ }
+ }
+ where
+ universal′ : {A B C : Set ℓ} {f : C A} {g : C B} {i : C A × B} (λ x proj₁ (i x)) ≡ f (λ x proj₂ (i x)) ≡ g (λ x f x , g x) ≡ i
+ universal′ refl refl = refl
+
+open Dummy public

0 comments on commit e8bb3a4

Please sign in to comment.