the total fibers (=fibers of the gap map) can be computed as iterated fibers between fibers.
I have renamed the term equiv-domain-sum-of-fibers which according to our naming scheme should be called equiv-sum-of-fibers-domain. I have added a formula is-equiv-domain-sum-of-fibers for its inverse.
In a commutative square
the total fibers (=fibers of the gap map) can be computed as iterated fibers between fibers.
I have renamed the term
equiv-domain-sum-of-fibers
which according to our naming scheme should be calledequiv-sum-of-fibers-domain
. I have added a formulais-equiv-domain-sum-of-fibers
for its inverse.