Adding product

[bond15]

No description provided.

[vcvpaiva]

this is not the product?

[vcvpaiva]

the category DialSets does not have a "par" connective, the operation can be defined (as you have it) but it's not a bifunctor, I think.

[vcvpaiva]

hi,
this bit of code is not right:
+⅋ : DialSet → DialSet → DialSet
+(U ⋆ X ⇒2∋ α) ⅋ (V ⋆ Y ⇒2∋ β) =

• (U × V) ⋆
• X ⊎ Y ⇒2∋
• λ{ ((u , v) , inj₁ x) → α (u , x)

• ; ((u , v) , inj₂ y) → β (v , y)}
  

we do not have a "par" connective in DialSets.

[bond15]

I thought this matched the comment here. Or is this a different operation?

×ₚ : DialSet → DialSet → DialSet
a ×ₚ b = record { U × V ; X + Y; choose(alpha, beta) }
-- want to choose a relation for a pair ((u,v), s), where s= (x, o) or (y, 1). if s=(x, 0) choose alpha, otherwise choose beta

[bond15]

the x\_p name is an artifact from Poly.agda

[vcvpaiva]

This is indeed a different operation, not par=multiplicative disjunction, but oplus=additivie disjunction, which also is not a connective in DialSets. maybe we could have a 15 min chat?

…

On Mon, May 16, 2022 at 11:29 AM bond15 ***@***.***> wrote: I thought this matched the comment here. Or is this a different operation? *×ₚ* : DialSet → DialSet → DialSet a ×ₚ b = record { U × V ; X + Y; choose(alpha, beta) } -- want to choose a relation for a pair ((u,v), s), where s= (x, o) or (y, 1). if s=(x, 0) choose alpha, otherwise choose beta — Reply to this email directly, view it on GitHub <#3 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAIZ3HZDQJEEGIFJLI6LN2DVKKHXLANCNFSM5WCIR7RA> . You are receiving this because you commented.Message ID: ***@***.***>

[bond15]

I'm available now. I can email a zoom link

[vcvpaiva]

please do send the zoom link

…

On Mon, May 16, 2022 at 11:37 AM bond15 ***@***.***> wrote: I'm available now. I can email a zoom link — Reply to this email directly, view it on GitHub <#3 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAIZ3H44DD2WWH5ERMQFY4TVKKIU7ANCNFSM5WCIR7RA> . You are receiving this because you commented.Message ID: ***@***.***>