TypeAligned.Duo

Like 'Pair' but type-aligned.  Called "Duo" because they are NOT
two-of-a-kind ("pair", "double", "couple"), since the indexes may differ.

Definitions

record Duo : Rel a -> a -> a -> Type

  Two relationshpis / proofs that meet in the middle

Totality: total
Visibility: public export
Constructor: 

MkDuo : (1 _ : p x y) -> (1 _ : p y z) -> Duo p x z

Projections:

.fst : ({rec:0} : Duo p x z) -> p x ({rec:0} .y)

.snd : ({rec:0} : Duo p x z) -> p ({rec:0} .y) z

0 .y : Duo p x z -> a

Hint: 

Show (p x y) => Show (Duo p x y)

0 .y : Duo p x z -> a

Totality: total
Visibility: public export

.fst : ({rec:0} : Duo p x z) -> p x ({rec:0} .y)

Totality: total
Visibility: public export

.snd : ({rec:0} : Duo p x z) -> p ({rec:0} .y) z

Totality: total
Visibility: public export

fst : (two : Duo p x z) -> p x (two .y)

  Explicit prefix record projection

Totality: total
Visibility: export

snd : (two : Duo p x z) -> p (two .y) z

  Explicit prefix record projection

Totality: total
Visibility: export

eqMeetOnce : p x y -@ (p x y -@ Bool) -> (1 l : Duo p x z) -> (1 r : Duo p x z) -> (0 _ : l .y = r .y) -> Bool

  Linear 'eqMeet'

Totality: total
Visibility: export

eqMeet : (p x y -> p x y -> Bool) -> (l : Duo p x z) -> (r : Duo p x z) -> (0 _ : l .y = r .y) -> Bool

  Something like "Eq", but I'm not sure it's useful.

Totality: total
Visibility: export

mapReduceOnce : {0 f : a -> b} -> {0 q : Rel b} -> p x y -@ q (f x) (f y) -> q x y -@ (q y z -@ q x z) -> Duo p x y -@ q (f x) (f y)

  Linear 'mapReduce'

Totality: total
Visibility: export

mapOnce : {0 f : a -> b} -> p x y -@ q (f x) (f y) -> Duo p x y -@ Duo q (f x) (f y)

  Linear 'map'

Totality: total
Visibility: export

mapReduce : {0 f : a -> b} -> {0 q : Rel b} -> (p x y -> q (f x) (f y)) -> (q x y -> q y z -> q x z) -> Duo p x y -> q (f x) (f y)

  Reduce while changing relation

Totality: total
Visibility: export

map : {0 f : a -> b} -> (p x y -> q (f x) (f y)) -> Duo p x y -> Duo q (f x) (f y)

  Change inner relation

Totality: total
Visibility: export

reduceOnce : p x y -@ (p y z -@ p x z) -> Duo p x y -@ p x y

  Linear 'reduce'

Totality: total
Visibility: export

reduce : (p x y -> p y z -> p x z) -> Duo p x y -> p x y

  Reduce to inner relation

Totality: total
Visibility: export