idris-error-3.idr

infixr 1 ~>

Relation_Arrow : Type -> Type
Relation_Arrow ob = (source, target: ob) -> Type

class RelationClass (ob: Type) where
  (~>) : Relation_Arrow ob

record RelationRecord : Type where
  MkRelation : (recOb: Type) -> (recInst: RelationClass recOb) -> RelationRecord

IsProductMorphism' : (RelationClass l, RelationClass r) => Relation_Arrow (l, r)
IsProductMorphism' (lS, rS) (lT, rT) = ((lS ~> lT), (rS ~> rT))

IsProductMorphism : (rL, rR: RelationRecord) -> Relation_Arrow ((recOb rL), (recOb rR))
IsProductMorphism rL rR = IsProductMorphism' @{recInst rL} @{recInst rR}