$B>/$7JdB-$7$F$*$-$^$9!#(B
$B-!!!(BHilbert$B$NBh#2LdBj$H$$$&$N$O#13,=R8lO@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@-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@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-m...
$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=rep...
$B$=$N8e!"!g!<(Bgroupoids$B$N?%$j@.$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=rep...
$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 [email protected] http://www.fos.kuis.kyoto-u.ac.jp/cgi-bin/mailman/listinfo/logic-ml
Logic-ml mailing list [email protected] http://www.fos.kuis.kyoto-u.ac.jp/cgi-bin/mailman/listinfo/logic-ml