--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/AgdaProduct.agda.replaced	Tue Sep 08 18:38:08 2020 +0900
@@ -0,0 +1,8 @@
+data _@$\times$@_ (A B : Set) : Set where
+  <_,_> : A @$\rightarrow$@ B @$\rightarrow$@ A @$\times$@ B
+
+fst : {A B : Set} @$\rightarrow$@ A @$\times$@ B @$\rightarrow$@ A
+fst < a , _ > = a
+
+snd : {A B : Set} @$\rightarrow$@ A @$\times$@ B @$\rightarrow$@ B
+snd < _ , b > = b