Mixing
In Homotopy Type Theory, where does the lambda expression reside?
Clash Royale CLAN TAG#URR8PPP
up vote
3
down vote
favorite
Background
I am trying to develop a visual language for doing higher level mathematics. The language is essentially the language of categories with some allowances since this thing runs on a computer.
However, doing things naively, you run into the issue of having to hand / hard code every feature. What is needed is the ability to specify the app framework using the app itself. I've decided on HoTT because it's an active area of research and different from what Coq / Isabelle use out-of-the box.
However, I don't want to re-invent the wheel and have the users enter in proofs in a Coq/Isabelle-like textual language. I'd like them to make use of a visual editor wherever this works out nicely, and go to the text editor whereever else.
So the visual editor diagrams will get converted into the same internal data structure that the textual samples get converted to. Ideally the data structure, the textual spec and the visual spec are all synced. This will mean that a lot of visual elements will become locked, as coding change propagation in the network of the data structure can get really difficult, and at times not really make sense. Therefore you lock certain items from editing.
Question
Anyway, where would the lambda expression reside in the above diagram? In HoTT in particular everything lies in a space (a type).
I would like a node with the expression shown and arrow to a tree definition of the expression (yes, a visual tree). Since that is how I will operate on the expressions (as trees).
category-theory math-software lambda-calculus homotopy-type-theory
asked Jul 18 at 19:43
EnjoysMath
8,63642154
add a comment |Â
up vote
3
down vote
favorite
Background
I am trying to develop a visual language for doing higher level mathematics. The language is essentially the language of categories with some allowances since this thing runs on a computer.
However, doing things naively, you run into the issue of having to hand / hard code every feature. What is needed is the ability to specify the app framework using the app itself. I've decided on HoTT because it's an active area of research and different from what Coq / Isabelle use out-of-the box.
However, I don't want to re-invent the wheel and have the users enter in proofs in a Coq/Isabelle-like textual language. I'd like them to make use of a visual editor wherever this works out nicely, and go to the text editor whereever else.
So the visual editor diagrams will get converted into the same internal data structure that the textual samples get converted to. Ideally the data structure, the textual spec and the visual spec are all synced. This will mean that a lot of visual elements will become locked, as coding change propagation in the network of the data structure can get really difficult, and at times not really make sense. Therefore you lock certain items from editing.
Question
Anyway, where would the lambda expression reside in the above diagram? In HoTT in particular everything lies in a space (a type).
I would like a node with the expression shown and arrow to a tree definition of the expression (yes, a visual tree). Since that is how I will operate on the expressions (as trees).
category-theory math-software lambda-calculus homotopy-type-theory
asked Jul 18 at 19:43
EnjoysMath
8,63642154
add a comment |Â
up vote
3
down vote
favorite
up vote
3
down vote
favorite
Background
I am trying to develop a visual language for doing higher level mathematics. The language is essentially the language of categories with some allowances since this thing runs on a computer.
However, doing things naively, you run into the issue of having to hand / hard code every feature. What is needed is the ability to specify the app framework using the app itself. I've decided on HoTT because it's an active area of research and different from what Coq / Isabelle use out-of-the box.
However, I don't want to re-invent the wheel and have the users enter in proofs in a Coq/Isabelle-like textual language. I'd like them to make use of a visual editor wherever this works out nicely, and go to the text editor whereever else.
So the visual editor diagrams will get converted into the same internal data structure that the textual samples get converted to. Ideally the data structure, the textual spec and the visual spec are all synced. This will mean that a lot of visual elements will become locked, as coding change propagation in the network of the data structure can get really difficult, and at times not really make sense. Therefore you lock certain items from editing.
Question
Anyway, where would the lambda expression reside in the above diagram? In HoTT in particular everything lies in a space (a type).
I would like a node with the expression shown and arrow to a tree definition of the expression (yes, a visual tree). Since that is how I will operate on the expressions (as trees).
category-theory math-software lambda-calculus homotopy-type-theory
asked Jul 18 at 19:43
EnjoysMath
8,63642154
Background
I am trying to develop a visual language for doing higher level mathematics. The language is essentially the language of categories with some allowances since this thing runs on a computer.
However, doing things naively, you run into the issue of having to hand / hard code every feature. What is needed is the ability to specify the app framework using the app itself. I've decided on HoTT because it's an active area of research and different from what Coq / Isabelle use out-of-the box.
However, I don't want to re-invent the wheel and have the users enter in proofs in a Coq/Isabelle-like textual language. I'd like them to make use of a visual editor wherever this works out nicely, and go to the text editor whereever else.
So the visual editor diagrams will get converted into the same internal data structure that the textual samples get converted to. Ideally the data structure, the textual spec and the visual spec are all synced. This will mean that a lot of visual elements will become locked, as coding change propagation in the network of the data structure can get really difficult, and at times not really make sense. Therefore you lock certain items from editing.
Question
Anyway, where would the lambda expression reside in the above diagram? In HoTT in particular everything lies in a space (a type).
I would like a node with the expression shown and arrow to a tree definition of the expression (yes, a visual tree). Since that is how I will operate on the expressions (as trees).
category-theory math-software lambda-calculus homotopy-type-theory
asked Jul 18 at 19:43
EnjoysMath
8,63642154
edited Jul 18 at 19:55
asked Jul 18 at 19:43
EnjoysMath
8,63642154
asked Jul 18 at 19:43
EnjoysMath
8,63642154
asked Jul 18 at 19:43
EnjoysMath
8,63642154
8,63642154
add a comment |Â
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
2
down vote
accepted
If we name the two boxes up there 'type $A$' and 'type $B$', so that $f:Ato B$, then the third box, where the corresponding lambda expression lives, is $hom(A, B)$ (meaning internal hom), which in type theory is simply denoted by $Ato B$.
Note that $f$ is of type $Ato B$(rejustifying the notation $fbf:Ato B$) and that it can be rewritten as $lambda a.f(a)$.
The yellow arrow, marked '=', from $B$ to $Ato B$ should rather (be of other color and) go from the arrow $f$.
answered Jul 18 at 21:12
Berci
56.4k23570
Thank you for the detailed analysis and involving the gui. What's wrong with $A$ instead of type A?
– EnjoysMath
Jul 18 at 22:38
Is internal hom different from $textHom(A,B)$ in the category of small types?
– EnjoysMath
Jul 18 at 22:40
:) 'home' was just autocorrection. I didn't intend to write 'type' on the boxes, just wanted to name them.
– Berci
Jul 18 at 22:41
I'm not sure what you exactly mean by 'category of small types'. In the category of sets and functions, it is the same.
– Berci
Jul 18 at 22:52
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
2
down vote
accepted
If we name the two boxes up there 'type $A$' and 'type $B$', so that $f:Ato B$, then the third box, where the corresponding lambda expression lives, is $hom(A, B)$ (meaning internal hom), which in type theory is simply denoted by $Ato B$.
Note that $f$ is of type $Ato B$(rejustifying the notation $fbf:Ato B$) and that it can be rewritten as $lambda a.f(a)$.
The yellow arrow, marked '=', from $B$ to $Ato B$ should rather (be of other color and) go from the arrow $f$.
answered Jul 18 at 21:12
Berci
56.4k23570
Thank you for the detailed analysis and involving the gui. What's wrong with $A$ instead of type A?
– EnjoysMath
Jul 18 at 22:38
Is internal hom different from $textHom(A,B)$ in the category of small types?
– EnjoysMath
Jul 18 at 22:40
:) 'home' was just autocorrection. I didn't intend to write 'type' on the boxes, just wanted to name them.
– Berci
Jul 18 at 22:41
I'm not sure what you exactly mean by 'category of small types'. In the category of sets and functions, it is the same.
– Berci
Jul 18 at 22:52
add a comment |Â
up vote
2
down vote
accepted
If we name the two boxes up there 'type $A$' and 'type $B$', so that $f:Ato B$, then the third box, where the corresponding lambda expression lives, is $hom(A, B)$ (meaning internal hom), which in type theory is simply denoted by $Ato B$.
Note that $f$ is of type $Ato B$(rejustifying the notation $fbf:Ato B$) and that it can be rewritten as $lambda a.f(a)$.
The yellow arrow, marked '=', from $B$ to $Ato B$ should rather (be of other color and) go from the arrow $f$.
answered Jul 18 at 21:12
Berci
56.4k23570
Thank you for the detailed analysis and involving the gui. What's wrong with $A$ instead of type A?
– EnjoysMath
Jul 18 at 22:38
Is internal hom different from $textHom(A,B)$ in the category of small types?
– EnjoysMath
Jul 18 at 22:40
:) 'home' was just autocorrection. I didn't intend to write 'type' on the boxes, just wanted to name them.
– Berci
Jul 18 at 22:41
I'm not sure what you exactly mean by 'category of small types'. In the category of sets and functions, it is the same.
– Berci
Jul 18 at 22:52
add a comment |Â
up vote
2
down vote
accepted
up vote
2
down vote
accepted
If we name the two boxes up there 'type $A$' and 'type $B$', so that $f:Ato B$, then the third box, where the corresponding lambda expression lives, is $hom(A, B)$ (meaning internal hom), which in type theory is simply denoted by $Ato B$.
Note that $f$ is of type $Ato B$(rejustifying the notation $fbf:Ato B$) and that it can be rewritten as $lambda a.f(a)$.
The yellow arrow, marked '=', from $B$ to $Ato B$ should rather (be of other color and) go from the arrow $f$.
answered Jul 18 at 21:12
Berci
56.4k23570
If we name the two boxes up there 'type $A$' and 'type $B$', so that $f:Ato B$, then the third box, where the corresponding lambda expression lives, is $hom(A, B)$ (meaning internal hom), which in type theory is simply denoted by $Ato B$.
Note that $f$ is of type $Ato B$(rejustifying the notation $fbf:Ato B$) and that it can be rewritten as $lambda a.f(a)$.
The yellow arrow, marked '=', from $B$ to $Ato B$ should rather (be of other color and) go from the arrow $f$.
answered Jul 18 at 21:12
Berci
56.4k23570
edited Jul 18 at 22:40
answered Jul 18 at 21:12
Berci
56.4k23570
answered Jul 18 at 21:12
Berci
56.4k23570
answered Jul 18 at 21:12
Berci
56.4k23570
56.4k23570
Thank you for the detailed analysis and involving the gui. What's wrong with $A$ instead of type A?
– EnjoysMath
Jul 18 at 22:38
Is internal hom different from $textHom(A,B)$ in the category of small types?
– EnjoysMath
Jul 18 at 22:40
:) 'home' was just autocorrection. I didn't intend to write 'type' on the boxes, just wanted to name them.
– Berci
Jul 18 at 22:41
I'm not sure what you exactly mean by 'category of small types'. In the category of sets and functions, it is the same.
– Berci
Jul 18 at 22:52
add a comment |Â
Thank you for the detailed analysis and involving the gui. What's wrong with $A$ instead of type A?
– EnjoysMath
Jul 18 at 22:38
Is internal hom different from $textHom(A,B)$ in the category of small types?
– EnjoysMath
Jul 18 at 22:40
:) 'home' was just autocorrection. I didn't intend to write 'type' on the boxes, just wanted to name them.
– Berci
Jul 18 at 22:41
I'm not sure what you exactly mean by 'category of small types'. In the category of sets and functions, it is the same.
– Berci
Jul 18 at 22:52
Thank you for the detailed analysis and involving the gui. What's wrong with $A$ instead of type A?
– EnjoysMath
Jul 18 at 22:38
Thank you for the detailed analysis and involving the gui. What's wrong with $A$ instead of type A?
– EnjoysMath
Jul 18 at 22:38
Is internal hom different from $textHom(A,B)$ in the category of small types?
– EnjoysMath
Jul 18 at 22:40
Is internal hom different from $textHom(A,B)$ in the category of small types?
– EnjoysMath
Jul 18 at 22:40
:) 'home' was just autocorrection. I didn't intend to write 'type' on the boxes, just wanted to name them.
– Berci
Jul 18 at 22:41
:) 'home' was just autocorrection. I didn't intend to write 'type' on the boxes, just wanted to name them.
– Berci
Jul 18 at 22:41
I'm not sure what you exactly mean by 'category of small types'. In the category of sets and functions, it is the same.
– Berci
Jul 18 at 22:52
I'm not sure what you exactly mean by 'category of small types'. In the category of sets and functions, it is the same.
– Berci
Jul 18 at 22:52
add a comment |Â
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2855932%2fin-homotopy-type-theory-where-does-the-lambda-expression-reside%23new-answer', 'question_page');
);
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password