[logic-ml] homotopy type theory

[logic at math.tsukuba.ac.jp]

$B>/$7JdB-$7$F$*$-$^$9!#(B

$B-!!!(BHilbert$B$NBh#2LdBj$H$$$&$N$O#13,=R8lO at M}$GDj<02=(B
$B$5$l$?<+A3?tO@$r4^$`$h$&$J8xM}7O!J$H$/$K(BZFC$B!K$O(Bdecidable$B$+$H(B
$B$$$&LdBj$G!"$3$l$K$D$$$F$O(BGodel$B$NIT40A4 at -DjM}$GH]DjE*$K2r7h$5$l$F(B
$B$$$^$9!#$7$+$7$3$N(BHilbert$B$NBh#2LdBj$r0ULu$7$F(B

$B?t3X$N4pAC$E$1$H$7$F;H$($k7A<0E*BN7O$G(Bdecidable$B$J$b$N$O(B
$BB8:_$9$k$+!)(B

$B$H$9$k$H!"$=$l$OB8:_$7$F$^$5$K(BHomotopy Type Theory (HTT)$B$,(B
$B$=$&$G$"$k$H$$$&$N$,!"2f!9$NN)>l$J$N$G!"K|0l$3$l$,(Bdecidable$B$G$J$$(B
$B$H$$$&$3$H$K$J$k$H!"7c?L$,Av$k$H8@$C$?$N$O!"$=$&$$$&0UL#$G$9!#(B
$B$A$J$_$K(B

dependent type theory with extensional identities

$B$O(Bundecidable$B$G$9!#(B

$B-"!!(BHigher categories$B$OJ*M}3X$G$b$9$4$/4pK\E*$G!"(B
$B$3$l$K$D$$$F$O0J2<$N(BSurvey$B$r$4Mw$/$@$5$$!#(B

https://zbmath.org/?q=an:1236.81006

$B$K$7$`$i(B
$BC^GHBg3X(B
$B?t3X(B

$BDI?-!'%*%^%1$G$9!#<j;}$AL5:;BA$J@^$K$G$b$I$&$>!#(B

https://www.youtube.com/watch?v=iugcK5rZueE


> $B$^$@Bh#42sL\$N9V5AO?$r(Bup$B$7$F$$$^$;$s$,!"(B
> $B$3$3$^$G$G(B
>
> depdendent type theory with intensional identities
>
> $B$,$I$s$J$b$N$+$O46?($O$D$+$a$?$H;W$&$N$G!"(B
> $BBh#52s$+$i$O$=$l$N(BModel$B$,$I$N$h$&$J$b$N$+$N(B
> $B46?($r$D$+$s$G$b$i$&$3$H$rL\;X$7$^$9!#(B
> $B8EE5E*$J(BCategory theory$B$r$6$C$HI|=,$7$?8e!"(B
> higher categories$B$H$O2?$J$N$+!"$I$s$J$b$N$G$J$1$l$P(B
> $B$$$1$J$$$+!"$H$$$C$?E@$rM}2r$7$F$b$i$&$D$b$j$G$9!#(B
> Higher categories$B$b0l at NA0$O(B
>
> $B$=$3$XF'$_9~$s$G$O$$$1$J$$!"E%>B$K(B
> $BB-$r$H$i$l$k$+$i!"(B
>
> $B$H8@$o$l$?$b$N$G$9$,!":#$O5U$K(Bhigher categories$B$J$7$G$O(B
> $B#2#1@$5*$N?t3X$r8l$k$3$H$,$G$-$J$$$H8@$($k>u67$@$H(B
> $B;W$$$^$9!#$?$H$($P(B
>
> http://www.math.harvard.edu/~lurie/papers/highertopoi.pdf
>
> $B$d(B
>
> https://webusers.imj-prg.fr/~frederic.paugam/documents/enseignement/master-mathematical-physics.pdf
>
> $B$r$4Mw$/$@$5$$!#8e<T$K$D$$$F$O;d$N(Breview$B$r(B
>
> https://www.ems-ph.org/journals/journal.php?jrn=news
>
> $B$r:#G/$N#37n9f$G$4Mw$$$?$@$1$^$9!#(BSpace$B$N4X78$G(B
> $BA4J8$r:\$;$i$l$J$+$C$?$N$G!"(B
> $B$=$l$OC^GHBg3X$N(BRepository$B$K$*$$$F$$$^$9!#(B
>
> https://tsukuba.repo.nii.ac.jp/?action=pages_view_main&active_action=repository_view_main_item_detail&item_id=35978&item_no=1&page_id=13&block_id=83
>
> $B$=$N8e!"!g!<(Bgroupoids$B$N?%$j at .$9@$3&$,>e5-$N(B
>
> depdendent type theory with intensional identities
>
> $B$N(BModel$B$K$[$\$J$C$F$$$k$H$$$&OC$r$7$^$9!#!I$[$\!I$H(B
> $B$$$C$?$N$O!"$H$j$"$($:(Bcoherence$B$NLdBj$O<N>]$7$F(B
> $B$H$$$&0UL#$G$9!#(B
>
> $B$3$l$O6/D4$5$l$F$$$k$3$H$G$9$,!">e5-$N(B
>
> depdendent type theory with intensional identities
>
> $B$O(Bdecidable$B$G$9!#$3$l$O(BTait$B$NJ}K!$G4JC1$K(B
> $B<($9$3$H$,$G$-$^$9!#$7$+$7(B
>
> Homotopy type theory
>
> $B$H8@$C$?>l9g$O!"$=$3$K(Bunivalence axiom$B$,F~$C$F$-$^$9$+$i!"(B
> $B$3$l$,(Bdecidability$B$rGK2u$7$F$7$^$o$J$$$+$O!"$^$@L$2r7hLdBj$G$9!#(B
> $B$b$7$b$3$l$,GK2u$7$F$7$^$&$H$$$&OC$K$J$k$H(B
> homotopy type theorists$B$N4V$K7c?L$,Av$k$G$7$g$&!#(B
> $B$=$N>W7b$O(BGödel$B$,IT40A4DjM}$G(BHilbert$B$NBh#2LdBj$K(B
> $BBP$7$FM?$($?>W7b$KI$E($9$k$H;W$$$^$9!#(B
> $B3'$5$s!"$=$s$J$3$H$O$"$j$($J$$$H$+$J$j3ZE7E*$K(B
> $B9=$($F$$$^$9!#(B
>
> $B$K$7$`$i(B
>
> $BDI?-!'%*%^%1$G$9!#<j;}L5:;BA$J@^$K$G$b$I$&$>!#(B
>
> https://www.youtube.com/watch?v=ibjTE5LsN1U
>
>> $B8=:_C^GHBg3X$G>e5-$K$D$$$F9V5A$r(B
>> $B9T$C$F$$$^$9$,!"$=$l$N9V5A(BNotes$B$r(B
>> $BC^GHBg3X$N(BRepository$B$KCV$$$F$$$-$^$9$N$G!"(B
>> $B$40FFb$7$F$*$-$^$9!#(B
>>
>> https://tsukuba.repo.nii.ac.jp/?action=pages_view_main&active_action=repository_view_main_item_detail&item_id=37910&item_no=1&page_id=13&block_id=83
>>
>> $B$K$7$`$i(B
>> $BC^GHBg3X(B
>> $B?t3X(B
>>
>> $BDI?-!'%*%^%1$G$9!#<j;}L5:;BA$J@^$K$I$&$>!#(B
>>
>> https://www.youtube.com/watch?v=RpppLxnESaU
>>
>>
>> _______________________________________________
>> Logic-ml mailing list
>> Logic-ml at fos.kuis.kyoto-u.ac.jp
>> http://www.fos.kuis.kyoto-u.ac.jp/cgi-bin/mailman/listinfo/logic-ml
>>
>
>
>
> _______________________________________________
> Logic-ml mailing list
> Logic-ml at fos.kuis.kyoto-u.ac.jp
> http://www.fos.kuis.kyoto-u.ac.jp/cgi-bin/mailman/listinfo/logic-ml
>