coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Reasoning about CIC in Coq + univalence

From: Talia Ringer <tringer AT cs.washington.edu>
To: Coq-Club <coq-club AT inria.fr>
Subject: [Coq-Club] Reasoning about CIC in Coq + univalence
Date: Tue, 13 Oct 2020 14:32:33 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=Pass smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-ua1-f43.google.com
Ironport-phdr: 9a23:eqkLUxUHW8aA9/bdR/j1K6ZLuMvV8LGtZVwlr6E/grcLSJyIuqrYbBaCt8tkgFKBZ4jH8fUM07OQ7/m/HzFRqs/f6jgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrrwjdrMkbjI9tJqosyxbFvGZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhNww4DaboKbOudgcKzBZt4VX3ZNU9xLWiBdHo+xbY0CBPcBM+ZCqIn9okMDowWkCgmoBePg0CJDiGP33a083OQuDxvG1xEnEtISqnTUrdP1NKgMXuCv16TH0S7DY+lY2Djn84jIchEhofeDXbJsdsrRz1MjGB3YgVWNsIHoOS6e2esRvWaB9eVgSf6vhHA9qwF3ujWiydsgh43Hi4waxF7K+yF0zJorKdClVEN1bsOoHZ9Nui+aKod7Td0vTm50tSs0xbALu5C2cSkJxZk62hLSaf2Kfo6V6RzgTOacOSl0iG5hdb6lhBu/8VKsxvPiWsWqylpHoSRIn9/RvX4XzRPT8NKISv5l80ehxzmP0wfT5/lBIU8ulKrbL4ctwqMqmZYOqEjDECD7lUvsgK+ZcUUk/eeo6+D5bbn8upCcMIp0hhn/MqQohMO/Hfw1PhYSU2Wf4+ix173u8VfnTLlUkPE6iKbUvZ7CKcQevKG5AgtV0og56xa4CjeryMgYnWMGLFJDdxKIkZLpNkrSL/DjF/u+jU6jkCxrx/DHOL3hDYnNLn/FkLv7Y7ly9lNcxBIpzd9D/5JUFq0BIPXrV0Dts9zYFwY1PBCww+b6E9pwzZgeWGKKAq+BKqzeq16I5uQ1I+mNfoAZojj9K+J2r8Lp2FQ+gBo2ebSjlc8cb2n9FfB7KW2YZ2Dti5EPCzFZkBA5SbnWgVmDWHZpZnC9Urh0si0hCYSpAJ3rTZvrn7Wa3Ca9EYFRYCZLBk3aQiSgTJmNR/pZMHHaGcRmiDFRDeH9Gb9k7gmnsUrB85QiNvDdo3xKvomly9Fu5+zVmg0183p5A9nPizjcHVExpXsBQnoN5I46pEV8zlmZ1q0h0q5TDppM7uhJUwE1KZnaieF2FoKrA1+TTpKyUF+jB+6eL3QxQ9Y2mYJcZk98H5C/h0mG0XbxRbASkLOPCdo/9aeOh3U=

Hi again!

I'd like to try out a proof about one of my tools, but to do so I need to introspect on the behavior of inductive constructors and eliminators, so I guess I need an embedding of CIC. It's OK for the purpose of this proof to use univalence, since my tool's metatheory is univalent. Is there an embedding of CIC I can play with, maybe in CoqHoTT?

Talia

[Coq-Club] Reasoning about CIC in Coq + univalence, Talia Ringer, 10/13/2020
- Re: [Coq-Club] Reasoning about CIC in Coq + univalence, Yannick Forster, 10/13/2020
  - Re: [Coq-Club] Reasoning about CIC in Coq + univalence, Talia Ringer, 10/13/2020