Envelope-to: lojban-list-archive@lojban.org
Delivery-date: Thu, 01 Apr 2021 19:07:31 -0700
Received-SPF: pass (google.com: domain of kali9putra@yahoo.com designates 74.6.135.42 as permitted sender) client-ip=74.6.135.42;
Date: Fri, 2 Apr 2021 00:21:24 +0000 (UTC)
From: "'John E Clifford' via lojban" <lojban@googlegroups.com>
To: "lojban@googlegroups.com" <lojban@googlegroups.com>
Message-ID: <797745934.37318.1617322884561@mail.yahoo.com>
In-Reply-To: <872ff21c-712d-4a4b-8f4f-351d6ff549dan@googlegroups.com>
References: <ac15b0d5-c27c-4d8c-a459-4f80e9970bddn@googlegroups.com> <2d3e019b-5f57-4288-98a8-cc7fe3bf41a2n@googlegroups.com> <16ccd800-23f0-4c9f-9ee7-8c7f4f08223en@googlegroups.com> <5d8ed35bc26ecb99ee250fe535f68e01@staticfree.info> <872ff21c-712d-4a4b-8f4f-351d6ff549dan@googlegroups.com>
Subject: Re: [lojban] Re: Lojban is a logical failure
MIME-Version: 1.0
Content-Type: multipart/alternative; 
	boundary="----=_Part_37317_243919069.1617322884557"
Content-Length: 26883
Reply-To: lojban@googlegroups.com
Precedence: list
Mailing-list: list lojban@googlegroups.com; contact lojban+owners@googlegroups.com
X-Spam_score: -3.1
X-Spam_score_int: -30
X-Spam_bar: ---

------=_Part_37317_243919069.1617322884557
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

 Well, I don=E2=80=99t understand category theory or HOIL, but I do underst=
and that trying to make a natural language into a formal one will lead to a=
n incomplete and unparsible syste, as converting English into Loglan/Lojban=
 has done. =C2=A0Start with the parsible system and build the natural on it=
 and you get not only parsibility but also a guarantee that the parse is co=
rrect (something the Ls never had nor even though to have). =C2=A0It is lon=
g slogging work, if Loglan/Lojban is worthwhile , then ding it this way is =
worthwile. =C2=A0We=E2=80=99ve wasted 66 years already, so don=E2=80=99t wa=
ste any more. =C2=A0(The sad thing is that, when the work is done, Loglan/L=
ojban will be sooo close, but never able to bridge the gap.)
    On Thursday, April 1, 2021, 03:03:58 PM CDT, Corbin Simpson <mostawesom=
edude@gmail.com> wrote: =20
=20
 I'm not a math genius. I'm just some person who was told that Lojban is a =
logical language and decided to take "logical" seriously as an adjective.

For what it's worth, it sounds like you understand what's going on in terms=
 of social dynamics. To paraphrase your quote, I am rude to la gleki becaus=
e la gleki has disrespected me for years *and* because la gleki has refused=
 to study and work on understanding formal maths. I am happy to talk to any=
 of the 730+ members who have *not* spent the past few years being backhand=
ed and dismissive on IRC.

This isn't my first post to the list, either. I strongly recommend reading =
the posts from the past year, especially the ones where I went entirely una=
nswered [0][1][2]. You also should know that I am following the tradition o=
f Clifford in directly critiquing the goals and status of Lojban [3].

[0] https://groups.google.com/g/lojban/c/L8NFx18ZePc
[1] https://groups.google.com/g/lojban/c/F-mntSJHz7w
[2] https://groups.google.com/g/lojban/c/LwYwRLtsajs
[3] https://groups.google.com/g/lojban/c/gkIpyzNXykw
On Thursday, April 1, 2021 at 11:15:43 AM UTC-7 xxv wrote:

I'm just a lurker here, but you came in really hot and are now being=20
mean to people. Perhaps, IDK, be cool and we can work this whole thing=20
out together? Not everyone is a math genius like you.

"People may be rude to you because they are unhappy, someone hurt them=20
recently, you were disrespectful towards them, or because they were=20
never taught the correct way to act around people." [0]

[0] https://www.wikihow.com/Be-Cool

On 2021-04-01 13:14, Corbin Simpson wrote:
> You are literally standing in front of the detailed plan, complete
> with links and notes, built from years of conversation about the
> nature of Lojban and maths, and you have the audacity to ask "do we
> have a plan?" {mi'a} have a plan, and it's the one I just explained.
> {mi'o} have a different plan: you need to learn some maths and stop
> being so squeamish about working directly with logic itself.
>=20
> Start from the definition of a category. Every category gives a logic;
> the objects of the category are equivalence classes of propositions,
> and the modus-ponens of the logic is witnessed by the category's
> arrows. This is the foundation of categorical logic. From there, you
> can learn about type theory and topos theory.
>=20
> I have spoon-fed you for years on IRC, and in this moment, you are
> like Henry the 8th in "A Man for All Seasons" [0], a vain king who
> believes himself to be a master of both English and Latin, who stands
> in the mud without even thinking about it, and who demonstrates their
> lack of understanding every time they refuse to engage in
> self-directed study.
>=20
> [0] https://en.wikipedia.org/wiki/A_Man_for_All_Seasons
>=20
> On Thursday, April 1, 2021 at 10:02:48 AM UTC-7 gleki.is...@gmail.com
> wrote:
>=20
>> Em quinta-feira, 1 de abril de 2021 =C3=A0s 18:08:28 UTC+3,
>> mostawe...@gmail.com escreveu:
>>=20
>>> Hey all,
>>>=20
>>> Time for the sort-of-annual reminder that Lojban falls far short
>>> of its goals. I'll spell out an explicit recipe for achieving
>>> those goals.
>>>=20
>>> Suppose that Lojban were logical; that is, suppose that it has a
>>> logic [0]. A logic has three components:
>>>=20
>>> * A collection of letters which form a collection of words
>>> * A grammar which indicates whether a sequence of words is a
>>> well-formed sentence
>>> * A collection of rewrite rules which each match sequences of
>>> words within well-formed sentences and replace them with new
>>> sequences of words which are still well-formed
>>>=20
>>> We have two of three, for what it's worth. The failure is in this
>>> third component. If we had all three, then we might call Lojban a
>>> *type theory* [1]. In a type theory, we start with a sentence, and
>>> then apply rewrite rules to create new sentences. A sequence of
>>> rewrite rules, along with a starting sentence, is called a *proof*
>>> when the rules can be applied in sequence to the starting sentence
>>> in order to produce a new final sentence.
>>>=20
>>> The defining feature of type theory is types. A type is a
>>> collection of proofs, called *elements* of the type, which might
>>> be equivalent to each other. To show equivalence for two objects,
>>> we would need a pair of proofs which transform one object into
>>> another. We can also do this for two different proofs which lead
>>> to the same element in the same type, by transforming one proof
>>> into another, and so on. (This leads to [2].)
>>>=20
>>> Contrary to popular belief, types are emergent features of type
>>> theory; they do not have to be predefined. If we had a collection
>>> of rewrite rules for Lojban, then we could discover types within
>>> Lojban's existing corpus. A ready stream of examples comes from
>>> the fact that sets are like partial (*truncated*) types; they have
>>> elements and equivalence, but no proofs.
>>>=20
>>> In fact, this would give the native type theory [3][4][5] of
>>> Lojban. A native type theory is one which is generated directly
>>> from the three components I mentioned earlier, but ignoring any
>>> "types" which might be defined internally already. For example,
>>> {ctaipe} does not actually refer to Lojban's types. The native
>>> type theory could be directly put to use computationally:
>>>=20
>>> * To prove formal facts about Lojban utterances [6]
>>> * To optimize Lojban utterances, shortening or clarifying them [7]
>>> * To synthesize Lojban utterances which describe a
>>> partially-specified world [8]
>>>=20
>>> * To compile Lojban utterances into executable programs [9]
>>>=20
>>> Iterating on CLL has not produced the rewrite rules that we might
>>> desire. It sketches several rules and even gives some examples for
>>> the "logical" connectives, but it is far from complete. Similarly,
>>> la brismu suggests a handful of rewrite rules borrowed from CLL
>>> and other logics, but is missing the tense system, BAI,
>>> Lojban-in-Lojban grammar, mekso, and much more.
>>>=20
>>> Lojban only cosplays as a logical language. We could fix that, if
>>> we cared to learn the relevant maths.
>>=20
>> Do we have a plan? No deadlines but some plan might be needed. Where
>> to start from? Can we solve problems iteratively?
>>=20
>>> Peace,
>>>=20
>>> ~ C.
>>>=20
>>> [0] https://ncatlab.org/nlab/show/logic
>>>=20
>>> [1] https://ncatlab.org/nlab/show/type+theory
>>> [2] https://ncatlab.org/nlab/show/homotopy%20type%20theory
>>> [3]
>>>=20
>> https://golem.ph.utexas.edu/category/2021/02/native_type_theory.html
>>>=20
>>> [4]
>>>=20
>>=20
> https://golem.ph.utexas.edu/category/2021/03/native_type_theory_part_2.ht=
ml
>>>=20
>>> [5]
>>>=20
>>=20
> https://golem.ph.utexas.edu/category/2021/03/native_type_theory_part_3_1.=
html
>>> [6] http://us.metamath.org/
>>> [7] https://egraphs-good.github.io/
>>> [8] https://github.com/webyrd/Barliman
>>> [9] http://docs.idris-lang.org/en/latest/
>=20
> --
> You received this message because you are subscribed to the Google
> Groups "lojban" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to lojban+un...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/lojban/16ccd800-23f0-4c9f-9ee7-8c7f4f08=
223en%40googlegroups.com
> [1].
>=20
>=20
> Links:
> ------
> [1]
> https://groups.google.com/d/msgid/lojban/16ccd800-23f0-4c9f-9ee7-8c7f4f08=
223en%40googlegroups.com?utm_medium=3Demail&utm_source=3Dfooter


--=20
You received this message because you are subscribed to the Google Groups "=
lojban" group.
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to lojban+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/=
lojban/872ff21c-712d-4a4b-8f4f-351d6ff549dan%40googlegroups.com.
 =20

--=20
You received this message because you are subscribed to the Google Groups "=
lojban" group.
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to lojban+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/=
lojban/797745934.37318.1617322884561%40mail.yahoo.com.

------=_Part_37317_243919069.1617322884557
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<html><head></head><body><div class=3D"ydp80f1a78dyahoo-style-wrap" style=
=3D"font-family:Helvetica Neue, Helvetica, Arial, sans-serif;font-size:13px=
;"><div></div>
        <div dir=3D"ltr" data-setdir=3D"false">Well, I don=E2=80=99t unders=
tand category theory or HOIL, but I do understand that trying to make a nat=
ural language into a formal one will lead to an incomplete and unparsible s=
yste, as converting English into Loglan/Lojban has done. &nbsp;Start with t=
he parsible system and build the natural on it and you get not only parsibi=
lity but also a guarantee that the parse is correct (something the Ls never=
 had nor even though to have). &nbsp;It is long slogging work, if Loglan/Lo=
jban is worthwhile , then ding it this way is worthwile. &nbsp;We=E2=80=99v=
e wasted 66 years already, so don=E2=80=99t waste any more. &nbsp;(The sad =
thing is that, when the work is done, Loglan/Lojban will be sooo close, but=
 never able to bridge the gap.)</div><div><br></div>
       =20
        </div><div id=3D"yahoo_quoted_8227681113" class=3D"yahoo_quoted">
            <div style=3D"font-family:'Helvetica Neue', Helvetica, Arial, s=
ans-serif;font-size:13px;color:#26282a;">
               =20
                <div>
                    On Thursday, April 1, 2021, 03:03:58 PM CDT, Corbin Sim=
pson &lt;mostawesomedude@gmail.com&gt; wrote:
                </div>
                <div><br></div>
                <div><br></div>
                <div><div id=3D"yiv5265063655"><div><div>I'm not a math gen=
ius. I'm just some person who was told that Lojban is a logical language an=
d decided to take "logical" seriously as an adjective.<br clear=3D"none"></=
div><div><br clear=3D"none"></div><div>For what it's worth, it sounds like =
you understand what's going on in terms of social dynamics. To paraphrase y=
our quote, I am rude to la gleki because la gleki has disrespected me for y=
ears *and* because la gleki has refused to study and work on understanding =
formal maths. I am happy to talk to any of the 730+ members who have *not* =
spent the past few years being backhanded and dismissive on IRC.<br clear=
=3D"none"></div><div><br clear=3D"none"></div><div>This isn't my first post=
 to the list, either. I strongly recommend reading the posts from the past =
year, especially the ones where I went entirely unanswered [0][1][2]. You a=
lso should know that I am following the tradition of Clifford in directly c=
ritiquing the goals and status of Lojban [3].<br clear=3D"none"></div><div>=
<br clear=3D"none"></div><div>[0] https://groups.google.com/g/lojban/c/L8NF=
x18ZePc<br clear=3D"none"></div><div>[1] https://groups.google.com/g/lojban=
/c/F-mntSJHz7w<br clear=3D"none"></div><div>[2] https://groups.google.com/g=
/lojban/c/LwYwRLtsajs<br clear=3D"none"></div><div>[3] https://groups.googl=
e.com/g/lojban/c/gkIpyzNXykw<br clear=3D"none"></div><div class=3D"yiv52650=
63655gmail_quote"><div class=3D"yiv5265063655gmail_attr">On Thursday, April=
 1, 2021 at 11:15:43 AM UTC-7 xxv wrote:<br clear=3D"none"></div><blockquot=
e class=3D"yiv5265063655gmail_quote" style=3D"margin:0 0 0 0.8ex;border-lef=
t:1px solid rgb(204, 204, 204);padding-left:1ex;">I'm just a lurker here, b=
ut you came in really hot and are now being=20
<br clear=3D"none">mean to people. Perhaps, IDK, be cool and we can work th=
is whole thing=20
<br clear=3D"none">out together? Not everyone is a math genius like you.
<br clear=3D"none">
<br clear=3D"none">"People may be rude to you because they are unhappy, som=
eone hurt them=20
<br clear=3D"none">recently, you were disrespectful towards them, or becaus=
e they were=20
<br clear=3D"none">never taught the correct way to act around people." [0]
<br clear=3D"none">
<br clear=3D"none">[0] <a rel=3D"nofollow noopener noreferrer" shape=3D"rec=
t" target=3D"_blank" href=3D"https://www.wikihow.com/Be-Cool">https://www.w=
ikihow.com/Be-Cool</a>
<br clear=3D"none">
<br clear=3D"none">On 2021-04-01 13:14, Corbin Simpson wrote:
<br clear=3D"none">&gt; You are literally standing in front of the detailed=
 plan, complete
<br clear=3D"none">&gt; with links and notes, built from years of conversat=
ion about the
<br clear=3D"none">&gt; nature of Lojban and maths, and you have the audaci=
ty to ask "do we
<br clear=3D"none">&gt; have a plan?" {mi'a} have a plan, and it's the one =
I just explained.
<br clear=3D"none">&gt; {mi'o} have a different plan: you need to learn som=
e maths and stop
<br clear=3D"none">&gt; being so squeamish about working directly with logi=
c itself.
<br clear=3D"none">&gt;=20
<br clear=3D"none">&gt; Start from the definition of a category. Every cate=
gory gives a logic;
<br clear=3D"none">&gt; the objects of the category are equivalence classes=
 of propositions,
<br clear=3D"none">&gt; and the modus-ponens of the logic is witnessed by t=
he category's
<br clear=3D"none">&gt; arrows. This is the foundation of categorical logic=
. From there, you
<br clear=3D"none">&gt; can learn about type theory and topos theory.
<br clear=3D"none">&gt;=20
<br clear=3D"none">&gt; I have spoon-fed you for years on IRC, and in this =
moment, you are
<br clear=3D"none">&gt; like Henry the 8th in "A Man for All Seasons" [0], =
a vain king who
<br clear=3D"none">&gt; believes himself to be a master of both English and=
 Latin, who stands
<br clear=3D"none">&gt; in the mud without even thinking about it, and who =
demonstrates their
<br clear=3D"none">&gt; lack of understanding every time they refuse to eng=
age in
<br clear=3D"none">&gt; self-directed study.
<br clear=3D"none">&gt;=20
<br clear=3D"none">&gt; [0] <a rel=3D"nofollow noopener noreferrer" shape=
=3D"rect" target=3D"_blank" href=3D"https://en.wikipedia.org/wiki/A_Man_for=
_All_Seasons">https://en.wikipedia.org/wiki/A_Man_for_All_Seasons</a>
<br clear=3D"none">&gt;=20
<br clear=3D"none">&gt; On Thursday, April 1, 2021 at 10:02:48 AM UTC-7 <a =
rel=3D"nofollow noopener noreferrer" shape=3D"rect">gleki.is...@gmail.com</=
a>
<br clear=3D"none">&gt; wrote:
<br clear=3D"none">&gt;=20
<br clear=3D"none">&gt;&gt; Em quinta-feira, 1 de abril de 2021 =C3=A0s 18:=
08:28 UTC+3,
<br clear=3D"none">&gt;&gt; <a rel=3D"nofollow noopener noreferrer" shape=
=3D"rect">mostawe...@gmail.com</a> escreveu:
<br clear=3D"none">&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; Hey all,
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; Time for the sort-of-annual reminder that L=
ojban falls far short
<br clear=3D"none">&gt;&gt;&gt; of its goals. I'll spell out an explicit re=
cipe for achieving
<br clear=3D"none">&gt;&gt;&gt; those goals.
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; Suppose that Lojban were logical; that is, =
suppose that it has a
<br clear=3D"none">&gt;&gt;&gt; logic [0]. A logic has three components:
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; * A collection of letters which form a coll=
ection of words
<br clear=3D"none">&gt;&gt;&gt; * A grammar which indicates whether a seque=
nce of words is a
<br clear=3D"none">&gt;&gt;&gt; well-formed sentence
<br clear=3D"none">&gt;&gt;&gt; * A collection of rewrite rules which each =
match sequences of
<br clear=3D"none">&gt;&gt;&gt; words within well-formed sentences and repl=
ace them with new
<br clear=3D"none">&gt;&gt;&gt; sequences of words which are still well-for=
med
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; We have two of three, for what it's worth. =
The failure is in this
<br clear=3D"none">&gt;&gt;&gt; third component. If we had all three, then =
we might call Lojban a
<br clear=3D"none">&gt;&gt;&gt; *type theory* [1]. In a type theory, we sta=
rt with a sentence, and
<br clear=3D"none">&gt;&gt;&gt; then apply rewrite rules to create new sent=
ences. A sequence of
<br clear=3D"none">&gt;&gt;&gt; rewrite rules, along with a starting senten=
ce, is called a *proof*
<br clear=3D"none">&gt;&gt;&gt; when the rules can be applied in sequence t=
o the starting sentence
<br clear=3D"none">&gt;&gt;&gt; in order to produce a new final sentence.
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; The defining feature of type theory is type=
s. A type is a
<br clear=3D"none">&gt;&gt;&gt; collection of proofs, called *elements* of =
the type, which might
<br clear=3D"none">&gt;&gt;&gt; be equivalent to each other. To show equiva=
lence for two objects,
<br clear=3D"none">&gt;&gt;&gt; we would need a pair of proofs which transf=
orm one object into
<br clear=3D"none">&gt;&gt;&gt; another. We can also do this for two differ=
ent proofs which lead
<br clear=3D"none">&gt;&gt;&gt; to the same element in the same type, by tr=
ansforming one proof
<br clear=3D"none">&gt;&gt;&gt; into another, and so on. (This leads to [2]=
.)
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; Contrary to popular belief, types are emerg=
ent features of type
<br clear=3D"none">&gt;&gt;&gt; theory; they do not have to be predefined. =
If we had a collection
<br clear=3D"none">&gt;&gt;&gt; of rewrite rules for Lojban, then we could =
discover types within
<br clear=3D"none">&gt;&gt;&gt; Lojban's existing corpus. A ready stream of=
 examples comes from
<br clear=3D"none">&gt;&gt;&gt; the fact that sets are like partial (*trunc=
ated*) types; they have
<br clear=3D"none">&gt;&gt;&gt; elements and equivalence, but no proofs.
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; In fact, this would give the native type th=
eory [3][4][5] of
<br clear=3D"none">&gt;&gt;&gt; Lojban. A native type theory is one which i=
s generated directly
<br clear=3D"none">&gt;&gt;&gt; from the three components I mentioned earli=
er, but ignoring any
<br clear=3D"none">&gt;&gt;&gt; "types" which might be defined internally a=
lready. For example,
<br clear=3D"none">&gt;&gt;&gt; {ctaipe} does not actually refer to Lojban'=
s types. The native
<br clear=3D"none">&gt;&gt;&gt; type theory could be directly put to use co=
mputationally:
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; * To prove formal facts about Lojban uttera=
nces [6]
<br clear=3D"none">&gt;&gt;&gt; * To optimize Lojban utterances, shortening=
 or clarifying them [7]
<br clear=3D"none">&gt;&gt;&gt; * To synthesize Lojban utterances which des=
cribe a
<br clear=3D"none">&gt;&gt;&gt; partially-specified world [8]
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; * To compile Lojban utterances into executa=
ble programs [9]
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; Iterating on CLL has not produced the rewri=
te rules that we might
<br clear=3D"none">&gt;&gt;&gt; desire. It sketches several rules and even =
gives some examples for
<br clear=3D"none">&gt;&gt;&gt; the "logical" connectives, but it is far fr=
om complete. Similarly,
<br clear=3D"none">&gt;&gt;&gt; la brismu suggests a handful of rewrite rul=
es borrowed from CLL
<br clear=3D"none">&gt;&gt;&gt; and other logics, but is missing the tense =
system, BAI,
<br clear=3D"none">&gt;&gt;&gt; Lojban-in-Lojban grammar, mekso, and much m=
ore.
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; Lojban only cosplays as a logical language.=
 We could fix that, if
<br clear=3D"none">&gt;&gt;&gt; we cared to learn the relevant maths.
<br clear=3D"none">&gt;&gt;=20
<br clear=3D"none">&gt;&gt; Do we have a plan? No deadlines but some plan m=
ight be needed. Where
<br clear=3D"none">&gt;&gt; to start from? Can we solve problems iterativel=
y?
<br clear=3D"none">&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; Peace,
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; ~ C.
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; [0] <a rel=3D"nofollow noopener noreferrer"=
 shape=3D"rect" target=3D"_blank" href=3D"https://ncatlab.org/nlab/show/log=
ic">https://ncatlab.org/nlab/show/logic</a>
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; [1] <a rel=3D"nofollow noopener noreferrer"=
 shape=3D"rect" target=3D"_blank" href=3D"https://ncatlab.org/nlab/show/typ=
e+theory">https://ncatlab.org/nlab/show/type+theory</a>
<br clear=3D"none">&gt;&gt;&gt; [2] <a rel=3D"nofollow noopener noreferrer"=
 shape=3D"rect" target=3D"_blank" href=3D"https://ncatlab.org/nlab/show/hom=
otopy%20type%20theory">https://ncatlab.org/nlab/show/homotopy%20type%20theo=
ry</a>
<br clear=3D"none">&gt;&gt;&gt; [3]
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt; <a rel=3D"nofollow noopener noreferrer" shape=
=3D"rect" target=3D"_blank" href=3D"https://golem.ph.utexas.edu/category/20=
21/02/native_type_theory.html">https://golem.ph.utexas.edu/category/2021/02=
/native_type_theory.html</a>
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; [4]
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;=20
<br clear=3D"none">&gt; <a rel=3D"nofollow noopener noreferrer" shape=3D"re=
ct" target=3D"_blank" href=3D"https://golem.ph.utexas.edu/category/2021/03/=
native_type_theory_part_2.html">https://golem.ph.utexas.edu/category/2021/0=
3/native_type_theory_part_2.html</a>
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;&gt; [5]
<br clear=3D"none">&gt;&gt;&gt;=20
<br clear=3D"none">&gt;&gt;=20
<br clear=3D"none">&gt; <a rel=3D"nofollow noopener noreferrer" shape=3D"re=
ct" target=3D"_blank" href=3D"https://golem.ph.utexas.edu/category/2021/03/=
native_type_theory_part_3_1.html">https://golem.ph.utexas.edu/category/2021=
/03/native_type_theory_part_3_1.html</a>
<br clear=3D"none">&gt;&gt;&gt; [6] <a rel=3D"nofollow noopener noreferrer"=
 shape=3D"rect" target=3D"_blank" href=3D"http://us.metamath.org/">http://u=
s.metamath.org/</a>
<br clear=3D"none">&gt;&gt;&gt; [7] <a rel=3D"nofollow noopener noreferrer"=
 shape=3D"rect" target=3D"_blank" href=3D"https://egraphs-good.github.io/">=
https://egraphs-good.github.io/</a>
<br clear=3D"none">&gt;&gt;&gt; [8] <a rel=3D"nofollow noopener noreferrer"=
 shape=3D"rect" target=3D"_blank" href=3D"https://github.com/webyrd/Barlima=
n">https://github.com/webyrd/Barliman</a>
<br clear=3D"none">&gt;&gt;&gt; [9] <a rel=3D"nofollow noopener noreferrer"=
 shape=3D"rect" target=3D"_blank" href=3D"http://docs.idris-lang.org/en/lat=
est/">http://docs.idris-lang.org/en/latest/</a>
<br clear=3D"none">&gt;=20
<br clear=3D"none">&gt;  --
<br clear=3D"none">&gt; You received this message because you are subscribe=
d to the Google
<br clear=3D"none">&gt; Groups "lojban" group.
<br clear=3D"none">&gt; To unsubscribe from this group and stop receiving e=
mails from it, send
<br clear=3D"none">&gt; an email to <a rel=3D"nofollow noopener noreferrer"=
 shape=3D"rect">lojban+un...@googlegroups.com</a>.
<div class=3D"yiv5265063655yqt4769281188" id=3D"yiv5265063655yqtfd31666"><b=
r clear=3D"none">&gt; To view this discussion on the web visit
<br clear=3D"none">&gt; <a rel=3D"nofollow noopener noreferrer" shape=3D"re=
ct" target=3D"_blank" href=3D"https://groups.google.com/d/msgid/lojban/16cc=
d800-23f0-4c9f-9ee7-8c7f4f08223en%40googlegroups.com">https://groups.google=
.com/d/msgid/lojban/16ccd800-23f0-4c9f-9ee7-8c7f4f08223en%40googlegroups.co=
m</a>
<br clear=3D"none">&gt; [1].
<br clear=3D"none">&gt;=20
<br clear=3D"none">&gt;=20
<br clear=3D"none">&gt; Links:
<br clear=3D"none">&gt; ------
<br clear=3D"none">&gt; [1]
<br clear=3D"none">&gt; <a rel=3D"nofollow noopener noreferrer" shape=3D"re=
ct" target=3D"_blank" href=3D"https://groups.google.com/d/msgid/lojban/16cc=
d800-23f0-4c9f-9ee7-8c7f4f08223en%40googlegroups.com?utm_medium=3Demail&amp=
;utm_source=3Dfooter">https://groups.google.com/d/msgid/lojban/16ccd800-23f=
0-4c9f-9ee7-8c7f4f08223en%40googlegroups.com?utm_medium=3Demail&amp;utm_sou=
rce=3Dfooter</a>
<br clear=3D"none"></div></blockquote></div><div class=3D"yiv5265063655yqt4=
769281188" id=3D"yiv5265063655yqtfd09188">

<p></p>

-- <br clear=3D"none">
You received this message because you are subscribed to the Google Groups "=
lojban" group.<br clear=3D"none">
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a rel=3D"nofollow noopener noreferrer" shape=3D"rect" ymailto=3D"m=
ailto:lojban+unsubscribe@googlegroups.com" target=3D"_blank" href=3D"mailto=
:lojban+unsubscribe@googlegroups.com">lojban+unsubscribe@googlegroups.com</=
a>.<br clear=3D"none">
To view this discussion on the web visit </div><a rel=3D"nofollow noopener =
noreferrer" shape=3D"rect" target=3D"_blank" href=3D"https://groups.google.=
com/d/msgid/lojban/872ff21c-712d-4a4b-8f4f-351d6ff549dan%40googlegroups.com=
?utm_medium=3Demail&amp;utm_source=3Dfooter">https://groups.google.com/d/ms=
gid/lojban/872ff21c-712d-4a4b-8f4f-351d6ff549dan%40googlegroups.com</a><div=
 class=3D"yiv5265063655yqt4769281188" id=3D"yiv5265063655yqtfd76496">.<br c=
lear=3D"none">
</div></div></div></div>
            </div>
        </div></body></html>

<p></p>

-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;lojban&quot; group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:lojban+unsubscribe@googlegroups.com">lojban+unsub=
scribe@googlegroups.com</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/d/msgid/lojban/797745934.37318.1617322884561%40mail.yahoo.com?utm_medium=
=3Demail&utm_source=3Dfooter">https://groups.google.com/d/msgid/lojban/7977=
45934.37318.1617322884561%40mail.yahoo.com</a>.<br />

------=_Part_37317_243919069.1617322884557--