How to check if types match?

Stream: general

[Pieter Cuijpers]

I'm trying to add a 'bisimulation'-like property to the notion of a Prefunctor (i.e. Quiver morphism).
This lead me to the following attempt at a definition, which gives a type mismatch between map a and b:

structure LabelledQuiverPrefunctorBisim
  [Quiver χ₁] [Quiver χ₂] (f₁ : Quiver.Labelling χ₁ α) (f₂ : Quiver.Labelling χ₂ α)
  extends Prefunctor χ₁ χ₂ where
  label : ∀ (a : x ⟶ x'), f₁ a = f₂ (map a)
  bisim : ∀ (b : obj x ⟶ y'), ∃ (a : x ⟶ x'), (map a) = b

I think this is because = is only defined between a lhs and rhs that are proven to be of the same type?
But if so... how do I write that I expect an a to exist such that the types match?

(And if anyone happens to recognize the property as something categorical, I'm happy to take pointers ;-)

[Edward van de Meent]

presumably, you'd like to have "for all y', there exist x' with obj x' = y'" somewhere as an assumption. Then, you can write bisim as "(for all x and x',) for every b : obj x -> obj x', there is a : x -> x' with map a = b". that should typecheck and (i think) be equivalent to what you're writing...

[Edward van de Meent]

i.e. change it to this:

structure LabelledQuiverPrefunctorBisim
  [Quiver χ₁] [Quiver χ₂] (f₁ : Quiver.Labelling χ₁ α) (f₂ : Quiver.Labelling χ₂ α)
  extends Prefunctor χ₁ χ₂ where
  label : ∀ (a : x ⟶ x'), f₁ a = f₂ (map a)
  obj_surjective : ∀ y', ∃ x', obj x' = y'
  bisim : ∀ (b : obj x ⟶ obj x'), ∃ (a : x ⟶ x'), (map a) = b

it might be the case that obj_surjective is a thing that is already provable from previous context (as I'm not very familiar with the concepts used in the definition). If that's the case, feel free to drop it.

[Pieter Cuijpers]

I think it is not exactly what I need yet, but I can work with this. Thanks!

[Pieter Cuijpers]

I've changed it to:

structure LabelledQuiverPrefunctorBisim
  [Quiver χ₁] [Quiver χ₂] (f₁ : Quiver.Labelling χ₁ α) (f₂ : Quiver.Labelling χ₂ α)
  extends Prefunctor χ₁ χ₂ where
  label : ∀ (a : x ⟶ x'), f₁ a = f₂ (map a)
  full : ∀ (b : obj x ⟶ obj x'), ∃ (a : x ⟶ x'), (map a) = b
  bisim : ∀ (b : obj x ⟶ y'), ∃ x', (obj x') = y'

Categorically, that makes it a full prefunctor with a special future reflecting property on objects only. Nice insight.

[Edward van de Meent]

Pieter Cuijpers said:

I think it is not exactly what I need yet, but I can work with this. Thanks!

when you said this, i realised that indeed obj_injective is slightly too strong, good catch!

[Pieter Cuijpers]

It's actually kind of pretty how the type-checking problem forces me to do a separation of concerns here.
I'm starting to appreciate type theory more now :-)

[Pieter Cuijpers]

Hm... actually...
Suppose I have an x with obj x -> y and both obj x1 = y and obj x2 = y, then my original definition only forces one of these two to have an arrow: x -> x1 or x -> x2. The new definition would force both x->x1 and x->x2. So it's not the same...

[Pieter Cuijpers]

This seems to work, but I find it ugly:

structure LabelledQuiverPrefunctorBisim
  [Quiver χ₁] [Quiver χ₂] (f₁ : Quiver.Labelling χ₁ α) (f₂ : Quiver.Labelling χ₂ α)
  extends Prefunctor χ₁ χ₂ where
  label : ∀ (a : x ⟶ x'), f₁ a = f₂ (map a)
  bisim : ∀ (b : obj x ⟶ y'), ∃ a : { a : x ⟶ x' // obj x' = y'}, ((map a.val).cast rfl a.prop) = b

Also, VSCode underlines the second a in the bisim definition to indicate it is unused, but when I replace it with a _ it has problems with the Subtype notation. That's just a minor thing though.

[Ruben Van de Velde]

Maybe _a works in that position