TypeAligned.Trio

Trio because they are NOT three-of-a-kind ("triple", "triad") since the indexes may differ.

Definitions

record Trio : Rel a -> a -> a -> Type

  Three relationships / proofs that link up

Totality: total
Visibility: public export
Constructor: 

MkTrio : (1 _ : p w x) -> (1 _ : p x y) -> (1 _ : p y z) -> Trio p w z

Projections:

.fst3 : ({rec:0} : Trio p w z) -> p w ({rec:0} .x)

.snd3 : ({rec:0} : Trio p w z) -> p ({rec:0} .x) ({rec:0} .y)

.thrd : ({rec:0} : Trio p w z) -> p ({rec:0} .y) z

0 .x : Trio p w z -> a

0 .y : Trio p w z -> a

Hint: 

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

0 .y : Trio p w z -> a

Totality: total
Visibility: public export

0 .x : Trio p w z -> a

Totality: total
Visibility: public export

.fst3 : ({rec:0} : Trio p w z) -> p w ({rec:0} .x)

Totality: total
Visibility: public export

.snd3 : ({rec:0} : Trio p w z) -> p ({rec:0} .x) ({rec:0} .y)

Totality: total
Visibility: public export

.thrd : ({rec:0} : Trio p w z) -> p ({rec:0} .y) z

Totality: total
Visibility: public export

head : (three : Trio p w z) -> p w (three .x)

  Explicit prefix record projection

Totality: total
Visibility: export

fst3 : (three : Trio p w z) -> p w (three .x)

  Explicit prefix record projection

Totality: total
Visibility: export

snd3 : (three : Trio p w z) -> p (three .x) (three .y)

  Explicit prefix record projection

Totality: total
Visibility: export

thrd : (three : Trio p w z) -> p (three .y) z

  Explicit prefix record projection

Totality: total
Visibility: export

last : (three : Trio p w z) -> p (three .y) z

  Explicit prefix record projection

Totality: total
Visibility: export

tail : (three : Trio p w z) -> Duo p (three .x) z

  Drop first relationship

Totality: total
Visibility: export

init : (three : Trio p w z) -> Duo p w (three .y)

  Drop last relationship

Totality: total
Visibility: export

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

  Linear 'eqMeet'

Totality: total
Visibility: export

eqMeet : (p x y -> p x y -> Bool) -> (l : Trio p w z) -> (r : Trio p w z) -> (0 _ : l .x = r .x) -> (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) -> Trio 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) -> Trio p x y -@ Trio 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) -> Trio p x y -> q (f x) (f y)

  Reduce while changing inner relation

Totality: total
Visibility: export

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

  Change inner relation

Totality: total
Visibility: export

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

  Linear 'reduce'

Totality: total
Visibility: export

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

  Reduce to inner relation

Totality: total
Visibility: export