Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Andreas Abel <andreas.abel@ifi.lmu.de>
To: Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk>,
	Michael Shulman <shulman@sandiego.edu>,
	Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Cc: agda list <Agda@lists.chalmers.se>
Subject: Re: [Agda] [HoTT] Re: Why do we need judgmental equality?
Date: Sun, 17 Feb 2019 15:22:23 +0100	[thread overview]
Message-ID: <bb38d3d6-d169-2a6c-aea3-c76ab9d56d85@ifi.lmu.de> (raw)
In-Reply-To: <8BC255D3-D1CB-4BC3-9EDE-342233AC177C@nottingham.ac.uk>

 > CCed to the agda list. Maybe somebody can comment on the decidabilty 
status?

Ulrich Berger and Anton Setzer: Undecidability of Equality for Codata Types

     Talk given at CMCS'18 Thessaloniki, Greece, 15 April 2018

 
http://www.cs.swan.ac.uk/~csetzer/articles/CMCS2018/bergerSetzerProceedingsCMCS18.pdf


On 2019-02-17 08:56, Thorsten Altenkirch wrote:
> On 17/02/2019, 01:25, "homotopytypetheory@googlegroups.com on behalf of Michael Shulman" <homotopytypetheory@googlegroups.com on behalf of shulman@sandiego.edu> wrote:
> 
>      However, I don't find it
>      arbitrary at all: *negative* types have strict eta, while positive
>      types don't.
> 
> This is a very good point. However Streams are negative types but for example agda doesn't use eta conversion on them, I think for a good reason. Actually I am not completely sure whether this is undecidable.
> 
> E.g. the following equation cannot be proven using refl (it can be proven in cubical agda btw). The corresponding equation for Sigma types holds definitionally.
> 
> infix 5 _∷_
> 
> record Stream (A : Set) : Set where
>    constructor _∷_
>    coinductive
>    field
>      hd : A
>      tl : Stream A
> 
> open Stream
> etaStream : {A : Set}{s : Stream A} → hd s ∷ tl s ≡ s
> etaStream = {!refl!}
> 
> CCed to the agda list. Maybe somebody can comment on the decidabilty status?
> 
> 
> 
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
> 
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda@lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

  parent reply	other threads:[~2019-02-17 14:22 UTC|newest]

Thread overview: 71+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-01-30 11:54 [HoTT] " Felix Rech
2019-02-05 23:00 ` [HoTT] " Matt Oliveri
2019-02-06  4:13   ` Anders Mörtberg
2019-02-09 11:55     ` Felix Rech
2019-02-16 15:59     ` Thorsten Altenkirch
2019-02-17  1:25       ` Michael Shulman
2019-02-17  7:56         ` Thorsten Altenkirch
2019-02-17  9:14           ` Matt Oliveri
2019-02-17  9:18           ` Michael Shulman
2019-02-17 10:52             ` Thorsten Altenkirch
2019-02-17 11:35               ` streicher
2019-02-17 11:44                 ` Thorsten Altenkirch
2019-02-17 14:24                   ` Bas Spitters
2019-02-17 19:36                   ` Thomas Streicher
2019-02-17 21:41                     ` Thorsten Altenkirch
2019-02-17 12:08             ` Matt Oliveri
2019-02-17 12:13               ` Matt Oliveri
2019-02-20  0:22               ` Michael Shulman
2019-02-17 14:22           ` Andreas Abel [this message]
2019-02-17  9:05         ` Matt Oliveri
2019-02-17 13:29         ` Nicolai Kraus
2019-02-08 21:19 ` Martín Hötzel Escardó
2019-02-08 23:31   ` Valery Isaev
2019-02-09  1:41     ` Nicolai Kraus
2019-02-09  8:04       ` Valery Isaev
2019-02-09  1:58     ` Jon Sterling
2019-02-09  8:16       ` Valery Isaev
2019-02-09  1:30   ` Nicolai Kraus
2019-02-09 11:38   ` Thomas Streicher
2019-02-09 13:29     ` Thorsten Altenkirch
2019-02-09 13:40       ` Théo Winterhalter
2019-02-09 11:57   ` Felix Rech
2019-02-09 12:39     ` Martín Hötzel Escardó
2019-02-11  6:58     ` Matt Oliveri
2019-02-18 17:37   ` Martín Hötzel Escardó
2019-02-18 19:22     ` Licata, Dan
2019-02-18 20:23       ` Martín Hötzel Escardó
2019-02-09 11:53 ` Felix Rech
2019-02-09 14:04   ` Nicolai Kraus
2019-02-09 14:26     ` Gabriel Scherer
2019-02-09 14:44     ` Jon Sterling
2019-02-09 20:34       ` Michael Shulman
2019-02-11 12:17         ` Matt Oliveri
2019-02-11 13:04           ` Michael Shulman
2019-02-11 15:09             ` Matt Oliveri
2019-02-11 17:20               ` Michael Shulman
2019-02-11 18:17                 ` Thorsten Altenkirch
2019-02-11 18:45                   ` Alexander Kurz
2019-02-11 22:58                     ` Thorsten Altenkirch
2019-02-12  2:09                       ` Jacques Carette
2019-02-12 11:03                   ` Matt Oliveri
2019-02-12 15:36                     ` Thorsten Altenkirch
2019-02-12 15:59                       ` Matt Oliveri
2019-02-11 19:27                 ` Matt Oliveri
2019-02-11 21:49                   ` Michael Shulman
2019-02-12  9:01                     ` Matt Oliveri
2019-02-12 17:54                       ` Michael Shulman
2019-02-13  6:37                         ` Matt Oliveri
2019-02-13 10:01                           ` Ansten Mørch Klev
2019-02-11 20:11                 ` Matt Oliveri
2019-02-11  8:23       ` Matt Oliveri
2019-02-11 13:03         ` Jon Sterling
2019-02-11 13:22           ` Matt Oliveri
2019-02-11 13:37             ` Jon Sterling
2019-02-11  6:51   ` Matt Oliveri
2019-02-09 12:30 ` [HoTT] " Thorsten Altenkirch
2019-02-11  7:01   ` Matt Oliveri
2019-02-11  8:04     ` Valery Isaev
2019-02-11  8:28       ` Matt Oliveri
2019-02-11  8:37         ` Matt Oliveri
2019-02-11  9:32           ` Rafaël Bocquet

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=bb38d3d6-d169-2a6c-aea3-c76ab9d56d85@ifi.lmu.de \
    --to=andreas.abel@ifi.lmu.de \
    --cc=Agda@lists.chalmers.se \
    --cc=Thorsten.Altenkirch@nottingham.ac.uk \
    --cc=homotopytypetheory@googlegroups.com \
    --cc=shulman@sandiego.edu \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).