Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |

####### # # E-scripts on Type Systems. # # Note 1: use the eev command (defined in eev.el) and the # ee alias (in my .zshrc) to execute parts of this file. # Executing this file as a whole makes no sense. # An introduction to eev can be found here: # # (find-eev-quick-intro) # http://angg.twu.net/eev-intros/find-eev-quick-intro.html # # Note 2: be VERY careful and make sure you understand what # you're doing. # # Note 3: If you use a shell other than zsh things like |& # and the for loops may not work. # # Note 4: I always run as root. # # Note 5: some parts are too old and don't work anymore. Some # never worked. # # Note 6: the definitions for the find-xxxfile commands are on my # .emacs. # # Note 7: if you see a strange command check my .zshrc -- it may # be defined there as a function or an alias. # # Note 8: the sections without dates are always older than the # sections with dates. # # This file is at <http://angg.twu.net/e/types.e> # or at <http://angg.twu.net/e/types.e.html>. # See also <http://angg.twu.net/emacs.html>, # <http://angg.twu.net/.emacs[.html]>, # <http://angg.twu.net/.zshrc[.html]>, # <http://angg.twu.net/escripts.html>, # and <http://angg.twu.net/>. # ####### # «.dependent» (to "dependent") # «.dependent-sums» (to "dependent-sums") https://math.stackexchange.com/questions/3466976/online-reference-book-for-implementing-concepts-in-type-theory/3468022#3468022 Simon Thompson: "Type Theory and Functional Programming" (1999) https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf ##### # # Research library of the ##dependent IRC channel. # 2020mar28 # ##### # «dependent» (to ".dependent") # (find-es "irc" "irccloud") # https://github.com/dpndnt/library ##### # # How to express dependent sums as inductive types # 2020mar31 # ##### # «dependent-sums» (to ".dependent-sums") # https://hub.darcs.net/dolio/agda-share/browse/ParamInduction.agda#139 # https://categorytheory.zulipchat.com/#narrow/stream/229111-general/topic/Category.20of.20Types # (find-books "__logic/__logic.el" "girard") # (find-proofsandtypespage (+ 8 81) "11 System F") https://categorytheory.zulipchat.com/#narrow/stream/229111-general/topic/Category.20of.20Types/near/192349559 Anyone has good pointers on why most texts on the Calculus of Constructions written by logicians avoid mentioning dependent sums, like Σa:A.B(a)? When we do Categorical Semantics for DTTs (canonical e.g.: in Bart Jacobs "Categorical Logic and Type Theory") we do the opposite - we explain most concepts on the adjunction Σ⊣π^* first, and leave most properties of π^*⊣Π as exercises... Here is my guess: rules for dependent sums _used to be_ given explicitly - for example they appear in the system in Zhaohui Luo's thesis - but then people like Christine Paulin-Mohring showed that dependent sums can be defined as certain initial algebras using inductive types blah blah blah - see https://hal.inria.fr/hal-01094195/ for an overview... Problem: I'm not being able to neither find on the web, nor define myself, a definition of Σa:A.B(a) given in terms of Π! I know that chapter 11 of Girard's "Proofs and Types" - http://www.paultaylor.eu/stable/prot.pdf - is about System F and about how to define Booleans, naturals, products and inductive types in System F, and I'm rereading it and finding it quite clear, but I'm not being able to adapt its definition of "×" to a definition of a "Σ" - probably because I don't have much practise... Any hints? Any pointers? Thanks in advance!!! What is "coe"? Some kind of coercion operator? Anyway: thanks, great! Cleaning up the notation a bit, this works in the naïve models that I have in mind: Let S = Σx:A.B(x) and S' = ΠR:Type. (Πx:A. B(x) → R) → R. If s':S' then we can define πs' and π's' as: πs' := s' A (λa:A. λb:B(a). a) and π's' := s' (B(πs')) (λa:A. λb:B(a). b). Homework for me for the next months: understand the extra axioms that we need to add to make this work "in general"... Dan Doel: Here is an Agda proof that parametricity allows you to derive induction for encoded Σ: https://hub.darcs.net/dolio/agda-share/browse/ParamInduction.agda#139 Dan Doel: Although I haven't run it in a very long time, so it's possible the file no longer loads. # Local Variables: # coding: utf-8-unix # End: