- data Union : (a -> Type) -> List a -> Type
An open union of families is an index picking a family out together with
a value in the family thus picked.
Totality: total
Constructor: - Element : (k : Nat) -> (0 _ : AtIndex t ts k) -> elt t -> Union elt ts
- decomp : Union elt (t :: ts) -> Either (Union elt ts) (elt t)
We can inspect an open union over a non-empty list of families to check
whether the value it contains belongs either to the first family or any
other in the tail.
Totality: total- decomp0 : Union elt [t] -> elt t
An open union over a singleton list is just a wrapper
Totality: total- inj : Member t ts => elt t -> Union elt ts
Given that equality of type families is not decidable, we have to
rely on the interface `Member` to automatically find the index of a
given family.
Totality: total- prj : Member t ts => Union elt ts -> Maybe (elt t)
Given that equality of type families is not decidable, we have to
rely on the interface `Member` to automatically find the index of a
given family.
Totality: total- split : Subset Nat (HasLength ss) -> Union elt (ss ++ ts) -> Either (Union elt ss) (Union elt ts)
By doing a bit of arithmetic we can figure out whether the union's value
came from the left or the right list used in the index.
Totality: total- weakenL : Subset Nat (HasLength ss) -> Union elt ts -> Union elt (ss ++ ts)
Inserting new union members on the left, requires shifting the index by
the number of members introduced. Note that this number is the only
thing we need to keep around at runtime.
Totality: total- weakenR : Union elt ts -> Union elt (ts ++ us)
Inserting new union members on the right leaves the index unchanged.
Totality: total