From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/8609 Path: news.gmane.org!not-for-mail From: Zhen Lin Low Newsgroups: gmane.science.mathematics.categories Subject: Are Joyal--Tierney fibrations exponentiable? Date: Fri, 1 May 2015 14:04:36 +0100 Message-ID: Reply-To: Zhen Lin Low NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 X-Trace: ger.gmane.org 1430525417 25769 80.91.229.3 (2 May 2015 00:10:17 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sat, 2 May 2015 00:10:17 +0000 (UTC) To: categories list Original-X-From: majordomo@mlist.mta.ca Sat May 02 02:10:08 2015 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.1.127]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1YoL0Q-0003IZ-IB for gsmc-categories@m.gmane.org; Sat, 02 May 2015 02:10:06 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:38141) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1YoKzJ-0006sj-GT; Fri, 01 May 2015 21:08:57 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1YoKzK-0001L1-0u for categories-list@mlist.mta.ca; Fri, 01 May 2015 21:08:58 -0300 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:8609 Archived-At: Dear categorists, Consider the category M of internal groupoids in a Grothendieck topos, equipped with the Joyal--Tierney model structure where the cofibrations are the injective-on-objects functors and the weak equivalences are the fully faithful functors that are essentially surjective on objects (the latter in the sense of internal logic). Are the fibrations in this model structure exponentiable in the sense that pulling back fibrations along a fibration has a right adjoint? Notice that M is a right proper model category in which the class of cofibrations is closed under pullback, so if the answer to the above question is yes, then the Lumsdaine--Warren construction can be applied to obtain a model of dependent type theory with identity types, dependent products, dependent sums, coproducts, etc. Best wishes, -- Zhen Lin [For admin and other information see: http://www.mta.ca/~cat-dist/ ]