From 85fc133fa0d64c61c380fcecada8f8358ad4b773 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 1 Mar 2019 15:45:10 +0100 Subject: transport and homotopy --- Prod.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Prod.thy') diff --git a/Prod.thy b/Prod.thy index 0bd037d..2cb62e4 100644 --- a/Prod.thy +++ b/Prod.thy @@ -24,8 +24,8 @@ syntax "_lam" :: "[idt, t, t] \ t" ("(2\'(_: _')./ _)" 30) "_lam'" :: "[idt, t, t] \ t" ("(2\_: _./ _)" 30) translations - "\(x: A). B" \ "(CONST Prod) A (\x. B)" "\x: A. B" \ "(CONST Prod) A (\x. B)" + "\(x: A). B" \ "(CONST Prod) A (\x. B)" "\(x: A). b" \ "(CONST lam) A (\x. b)" "\x: A. b" \ "(CONST lam) A (\x. b)" -- cgit v1.2.3