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 < > hermogene...@student.uni-tuebingen.de <javascript:>> escreveu: > >> Fernando Yamauti <fgya...@gmail.com <javascript:>> 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 logica-l+u...@dimap.ufrn.br <javascript:>. >> Para postar neste grupo, envie um e-mail para logi...@dimap.ufrn.br >> <javascript:>. >> 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/87wpb1tpz7.fsf%40camelot.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 logica-l+unsubscr...@dimap.ufrn.br. Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br. 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/28e4c785-a336-4b64-989f-42e3de6a9f6f%40dimap.ufrn.br.
