The source can be downloaded here:
http://people.csail.mit.edu/garland/LP/

It had FiniteMap object type:

FiniteMap (M, D, R): trait
% An M is a map from D's to R's.
introduces
{}: -> M
update: M, D, R -> M
apply: M, D -> R
defined: M, D -> Bool
asserts
M generated by {}, update
M partitioned by apply, defined
forall m: M, d, d1, d2: D, r: R
apply(update(m, d2, r), d1) ==
if d1 = d2 then r else apply(m, d1);
~defined({}, d);
defined(update(m, d2, r), d1) ==
d1 = d2 \/ defined(m, d1)
implies
Array1 (update for assign, apply for __[__],
M for A, D for I, R for E)
converts apply, defined
exempting forall d: D apply({}, d)
http://nms.lcs.mit.edu/Larch/handbook/FiniteMap.html

Basically a type generated from {} and update, whereby
{} being the empty function. Besides an apply function
it has also a defined predicate. The functions itself are

conceived partial. The apply might react like Dan-O-Matiks
function when outside domain, in that apply(m, d) has
neither provable the value a nor the value b, but nevertheless

the underlying simple typed language would make apply ?total?
on the full D. On the other hand defined is more precise, we
even have ~defined({}, d) provable. So I guess one would use

defined and not apply, in case one is interested which subset of
D corresponds to the domain of a give function. If the type is
not inductive from {} and update, it would also allow infinite

functions and their updates.

Univalency is rather revival of rewriting systems in
a wicked way. But this is only from glossing over it.
Historically, for example when going from Larch to

Isabelle/HOL, we see rather that first order equality
and rewriting was enhanced by higher order terms and
and a less termish view of propositions. Univalency

seems to make things termish again, and then allow
a horde of category theorists takle the problems that
originally were addressed by "hackers" such as Knuth.

LoL

Mostowski Collapse schrieb am Dienstag, 25. Januar 2022 um 00:39:54 UTC+1:
> The source can be downloaded here:
> http://people.csail.mit.edu/garland/LP/
>
> It had FiniteMap object type:
>
> FiniteMap (M, D, R): trait
> % An M is a map from D's to R's.
> introduces
> {}: -> M
> update: M, D, R -> M
> apply: M, D -> R
> defined: M, D -> Bool
> asserts
> M generated by {}, update
> M partitioned by apply, defined
> forall m: M, d, d1, d2: D, r: R
> apply(update(m, d2, r), d1) ==
> if d1 = d2 then r else apply(m, d1);
> ~defined({}, d);
> defined(update(m, d2, r), d1) ==
> d1 = d2 \/ defined(m, d1)
> implies
> Array1 (update for assign, apply for __[__],
> M for A, D for I, R for E)
> converts apply, defined
> exempting forall d: D apply({}, d)
> http://nms.lcs.mit.edu/Larch/handbook/FiniteMap.html
>
> Basically a type generated from {} and update, whereby
> {} being the empty function. Besides an apply function
> it has also a defined predicate. The functions itself are
>
> conceived partial. The apply might react like Dan-O-Matiks
> function when outside domain, in that apply(m, d) has
> neither provable the value a nor the value b, but nevertheless
>
> the underlying simple typed language would make apply ?total?
> on the full D. On the other hand defined is more precise, we
> even have ~defined({}, d) provable. So I guess one would use
>
> defined and not apply, in case one is interested which subset of
> D corresponds to the domain of a give function. If the type is
> not inductive from {} and update, it would also allow infinite
>
> functions and their updates.

I just wrote a "anti-rewriting" pamphlet:

Non-Normal Manifesto
Before we begin we should assure ourselves about
our motivation to introduce first order equality into our
automated theorem prover. Usually automated theorem
proves might not only have a notion of an equality s = t,
but also a notion of a rewriting rule s -> t, and a notion
of size |r| of a term r.

A normal proof is then defined as a proof where the (subst)
rule is only applied when not |t| > |s|. With such a notion
of a (subst) rule, might then come a notion of computation
by repeating this step. Ultimately we might then ask for
complete and terminating rewrite rules.

In our take of an automated theorem prover, we do avoid
notions that go beyond equality s = t, and henceforth do
not aim at normal proofs. We are rather interested in
finding short proofs, and a short proof might be a
non-normal proof. The below shows a non-normal proof:

1. f1(c1) = c2 ∧ c3 = f2(c2) ∧ f3(c3) = c4 ⇒ f3(f2(f1(c1))) = c4
2. f3(f2(f1(c1))) = c4 (T⇒2 1)
3. ¬(f1(c1) = c2 ∧ c3 = f2(c2) ∧ f3(c3) = c4) (T⇒1 1)
4. ¬(c3 = f2(c2) ∧ f3(c3) = c4) (F∧2 3)
5. ¬f1(c1) = c2 (F∧1 3)
6. ¬f3(c3) = c4 (F∧2 4)
7. ¬c3 = f2(c2) (F∧1 4)
8. ¬f3(f2(c2)) = c4 (F= 6, 7)
9. f3(f2(c2)) = c4 (F= 2, 5)
✓ (ax 9, 8)

If we measure the size of a term by its printing length, we see
that the first application of (F=) to ~c3 = f2(c2) and ~f3(c3) = c4
is non-normal since f2(c2) is larger than c3. On the other hand
the second application of (F=) to ~f1(c1) = c2
to f3(f2(f1(c1)) = c4 is normal.

Have Fun!

See also:

Regular Equality Proofs for Maslovs Method
https://twitter.com/dogelogch/status/1485940674608386051

Regular Equality Proofs for Maslovs Method
https://www.facebook.com/groups/dogelog

Mostowski Collapse schrieb am Dienstag, 25. Januar 2022 um 13:00:36 UTC+1:
> Univalency is rather revival of rewriting systems in
> a wicked way. But this is only from glossing over it.
> Historically, for example when going from Larch to
>
> Isabelle/HOL, we see rather that first order equality
> and rewriting was enhanced by higher order terms and
> and a less termish view of propositions. Univalency
>
> seems to make things termish again, and then allow
> a horde of category theorists takle the problems that
> originally were addressed by "hackers" such as Knuth.
>
> LoL
> Mostowski Collapse schrieb am Dienstag, 25. Januar 2022 um 00:39:54 UTC+1:
> > The source can be downloaded here:
> > http://people.csail.mit.edu/garland/LP/
> >
> > It had FiniteMap object type:
> >
> > FiniteMap (M, D, R): trait
> > % An M is a map from D's to R's.
> > introduces
> > {}: -> M
> > update: M, D, R -> M
> > apply: M, D -> R
> > defined: M, D -> Bool
> > asserts
> > M generated by {}, update
> > M partitioned by apply, defined
> > forall m: M, d, d1, d2: D, r: R
> > apply(update(m, d2, r), d1) ==
> > if d1 = d2 then r else apply(m, d1);
> > ~defined({}, d);
> > defined(update(m, d2, r), d1) ==
> > d1 = d2 \/ defined(m, d1)
> > implies
> > Array1 (update for assign, apply for __[__],
> > M for A, D for I, R for E)
> > converts apply, defined
> > exempting forall d: D apply({}, d)
> > http://nms.lcs.mit.edu/Larch/handbook/FiniteMap.html
> >
> > Basically a type generated from {} and update, whereby
> > {} being the empty function. Besides an apply function
> > it has also a defined predicate. The functions itself are
> >
> > conceived partial. The apply might react like Dan-O-Matiks
> > function when outside domain, in that apply(m, d) has
> > neither provable the value a nor the value b, but nevertheless
> >
> > the underlying simple typed language would make apply ?total?
> > on the full D. On the other hand defined is more precise, we
> > even have ~defined({}, d) provable. So I guess one would use
> >
> > defined and not apply, in case one is interested which subset of
> > D corresponds to the domain of a give function. If the type is
> > not inductive from {} and update, it would also allow infinite
> >
> > functions and their updates.