Re: [HoTT] Re: Precategories, Categories and Univalent categories

[Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk>]

Sorry, I was to quick pressing send. We need the category to have homsets
C : |C| -> |C| -> Set which means that the equations of a category are
propositional. Similar we need to say

Fm : C(x,y) -> |F|(x) -> |F|(y) -> Set

and add fibred id and composition and the laws (again propositional).
Thorsten


On 08/11/2018, 16:01, "homotopytypetheory@googlegroups.com on behalf of
Thorsten Altenkirch" <homotopytypetheory@googlegroups.com on behalf of
Thorsten.Altenkirch@nottingham.ac.uk> wrote:

>Hi Thomas,
>
>two answers: the first is that in this particular case one doesn't need
>strict equality because one can present this as an indexed structure in
>type theory, e.g. assume as given a category C then a fibration F is a
>structure with the following components (here I assume that the base cat C
>is given by objects |C|, morphisms C(_,_) and so on.
>
>|F| : |C| -> U
>Fm : C(x,y) -> |F|(x) -> |F|(y) -> U
>id_F : Fm id a a
>comp_F : Fm f b c -> Fm g a b -> Fm (f o g) a c
>coe : C(x,y) -> |F|(y) -> |F|(x)
>coh : (p : C(x,y)) -> Fm(p,coe(p,x,a),a)
>
>The 2nd answer is that this is not always possible and the most well known
>example are semi-simplicial types. In this case we can produce indexed
>structures for all finite approximations but we can't generate the
>approximations in a uniform way (the question is actually an open
>problem). However, you don't want to force your categories to be struct
>but you want to be able to talk about your univalent, non-strict
>categories from a strict metatheoretic perspective. This can be realized
>by a 2-level type theory as for example explained in our paper [1]
>http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf
>
>Cheers,
>
>Thorsten
>
>[1] @InProceedings{altenkirch_et_al:LIPIcs:2016:6561,
>author ={Thorsten Altenkirch and Paolo Capriotti and Nicolai Kraus},
>title ={{Extending Homotopy Type Theory with Strict Equality}},
>booktitle ={25th EACSL Annual Conference on Computer Science Logic (CSL
>2016)},
>pages ={21:1--21:17},
>series ={Leibniz International Proceedings in Informatics (LIPIcs)},
>ISBN ={978-3-95977-022-4},
>ISSN ={1868-8969},
>year ={2016},
>volume ={62},
>editor ={Jean-Marc Talbot and Laurent Regnier},
>publisher ={Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
>address ={Dagstuhl, Germany},
>URL ={http://drops.dagstuhl.de/opus/volltexte/2016/6561},
>URN ={urn:nbn:de:0030-drops-65612},
>doi ={http://dx.doi.org/10.4230/LIPIcs.CSL.2016.21},
>annote ={Keywords: homotopy type theory, coherences, strict equality,
>homotopy type system}
>}
>
>
>
>
>
>On 08/11/2018, 11:58, "Thomas Streicher"
><streicher@mathematik.tu-darmstadt.de> wrote:
>
>>Thorsten asked why I prefer to have strict equality on categories.
>>The answer is that one needs it in category theory typically when
>>speaking about Grothendieck fibrations.
>>And the latter is most useful in many contexts in particular when
>>understanding geometric morphisms. This by the way also extends to
>>Grothendieck fibrations in quasicategories as in Joyal and Lurie's
>>accounts.
>>
>>Thomas
>>
>>
>
>
>
>
>This message and any attachment are intended solely for the addressee
>and may contain confidential information. If you have received this
>message in error, please contact the sender and delete the email and
>attachment. 
>
>Any views or opinions expressed by the author of this email do not
>necessarily reflect the views of the University of Nottingham. Email
>communications with the University of Nottingham may be monitored
>where permitted by law.
>
>
>
>
>-- 
>You received this message because you are subscribed to the Google Groups
>"Homotopy Type Theory" group.
>To unsubscribe from this group and stop receiving emails from it, send an
>email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
>For more options, visit https://groups.google.com/d/optout.




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.