#######
#
# 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: