Oi Bruno, Obrigado pelas referencias. Eu já conhecia todas elas menos a do Walsh (que vou ler depois com mais calma, mas aparentemente o que ele faz é pegar a imagem da diagonal pelo elemento final da fibra em A, mas isso leva a um problema semelhante ao do artigo do Ladyman e Presnell, já que uma categoria em geral tem elementos a mais; elementos locais, por exemplo, em um no topos de feixes que tem seções que não são globais). Infelizmente ainda acho as justificativas pré-formais dadas nesses artigos um tanto insuficientes. E, além disso, tenho objeções às justificativas dadas no caso extensional (as duas ultimas abaixo).
A do Tsementzis só substitui um problema por outro, já que a (meta)matemática não trata de espaços e, sim, de juízos sobre proposições. No final o paper só descreve o modelo simplicial de uma maneira mais intuitiva (e meio bagunçada para alguém que já sabe homotopia), mas, para isso ocorrer, é necessário acreditar no modelo simplicial. A do Ladyman e Presnell também me parece um tanto insuficiente. Por exemplo, um tipo A \times B pode ter mais termos que somente os (a, b) com a : A e b: B. O que são esses termos? O que é uma prova de A \times B que não pode ser definicionalmente modificada para se quebrar em provas de A e B, respectivamente? Esse é o exemplo mais banal, enquanto, no artigo, é usado algo mais envolvido de mesma natureza, a contratibilidade da fibra do espaço dos caminhos. Um outro caso que me incomoda muito e o Martin-Löf sempre joga em baixo do tapete: o porquê de " 'A true' infere 'B true' " ser correto, onde A é falso (onde o "falso" é clássico, ou seja, existe uma prova de \neg A) , para um construtivista. Como se constrói uma prova, a partir de uma prova de que o falso é verdadeiro? Ou ainda, outro problema que leva ao regresso infinito e a identificação de um objeto do conhecimento com o conhecimento desse objeto (que o Rodrigo havia comentado a um tempo atras de maneira diferente). Um juízo do tipo 'A true' pode virar uma proposição onde '(A true) true' se torna um juízo. E, mais. No ponto de vista epistemico, essas duas coisas são equivalentes (saber que vc sabe é igual a saber). Acho que o ponto de vista epistemico não bate com a teoria, já que garantir que o tipo "A é habitado" não é equivalente a A (em um dado universo), ou será que é? Ou seja, a justificativa do ML não é adequada e só a teoria funciona. Felizmente, só "trabalho" (brinco) com os modelos (infinito) categorias, então mesmo se todo o construtivismo como enunciado na HoTT estiver "errado" ainda tenho motivos para estudá-lo :) Abs, Fernando Yamauti Em 4 de abril de 2017 10:10, Bruno Bentzen <[email protected]> escreveu: > Oi Fernando, > > Talvez você possa se interessar também por esta animada discussão na FOM > > https://www.cs.nyu.edu/pipermail/fom/2016-March/019575.html > > que chegou a ser uma thread bem animada no mês de março do ano passado > (inclusive este paper é mencionado). > > O Ladyman e o Presnell parecem ter sido os primeiros a sugerir que uma > justificativa para as regras da identidade da HoTT deva ser apresentada de > uma maneira 'pré-matemática'. De lá para cá tem havido outras propostas de > justificação diferentes. Uma delas é a proposta inferencialista do Patrick > Walsh que possui uma abordagem bastante inspirada na teoria das categorias > > https://www.academia.edu/22231067/Categorical_Harmony_and_Path_Induction > > Uma outra é a do Dimitris Tsementzis, que é uma explicação pré-formal para > a HoTT baseada em "noções espaciais": > > http://philsci-archive.pitt.edu/12824/ > > Abraços, > Bruno > > -- > Bruno Bentzen > https://sites.google.com/site/bbentzena/ > > On Tuesday, April 4, 2017 at 12:30:25 AM UTC+8, Fernando Yamauti wrote: >> >> Muito obrigado! >> >> Em 3 de abril de 2017 13:28, Hermógenes Oliveira < >> [email protected]> escreveu: >> >>> Fernando Yamauti <[email protected]> escreveu: >>> >>> > Oi, >>> > >>> > Será que alguém teria acesso ao paper >>> > >>> > 1 Ladyman, J., Presnell, S.: Identity in Homotopy Type Theory, Part I: >>> > The Justification of Path Induction. Philosophia Mathematica (2015) ? >>> >>> Coincidência. Eu li esse artigo recentemente. A versão que eu li está >>> disponível em >>> >>> http://philsci-archive.pitt.edu/11079/1/Identity_in_HTT_public.pdf >>> >>> Sem contar o selinho da Oxford University Press, não sei se há muitas >>> diferenças entre a versão acima e a versão oficial. >>> >>> Além das páginas tradicionais, >>> >>> https://homotopytypetheory.org/links/ >>> https://ncatlab.org/nlab/show/homotopy+type+theory#References >>> >>> mais referências interessantes para quem estiver estudando Teoria >>> Homotópica dos Tipos podem ser encontradas no repositório do grupo de >>> estudos que estamos organizando aqui em Tübingen: >>> >>> https://github.com/BinderDavid/HoTT-StudyGroup >>> >>> -- >>> Hermógenes Oliveira >>> >>> -- >>> Você está recebendo esta mensagem porque se inscreveu no grupo >>> "LOGICA-L" dos Grupos do Google. >>> Para cancelar inscrição nesse grupo e parar de receber e-mails dele, >>> envie um e-mail para [email protected]. >>> Para postar neste grupo, envie um e-mail para [email protected]. >>> Visite este grupo em https://groups.google.com/a/di >>> map.ufrn.br/group/logica-l/. >>> Para ver esta discussão na web, acesse https://groups.google.com/a/di >>> map.ufrn.br/d/msgid/logica-l/87wpb1tpz7.fsf%40camelot.oliveira. >>> >> >> -- > Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos > Grupos do Google. > Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie > um e-mail para [email protected]. > Para postar nesse grupo, envie um e-mail para [email protected]. > Acesse esse grupo em https://groups.google.com/a/ > dimap.ufrn.br/group/logica-l/. > Para ver essa discussão na Web, acesse https://groups.google.com/a/ > dimap.ufrn.br/d/msgid/logica-l/28e4c785-a336-4b64-989f- > 42e3de6a9f6f%40dimap.ufrn.br > <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/28e4c785-a336-4b64-989f-42e3de6a9f6f%40dimap.ufrn.br?utm_medium=email&utm_source=footer> > . > -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para [email protected]. Para postar neste grupo, envie um e-mail para [email protected]. Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAJGvw-3b3y3B3MaM3M4%2Bg6Oko32SJ21exeePr%2B1Bsf9XBOPqQA%40mail.gmail.com.
