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

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

Didn't deny that it's possible in principle for this very simple case.
But something trivial gets unnaturally complicated when changing foundations.
That's already showing that the new foundation is not superior in all
aspects but actually much worse in particular cases.

This is not unexpected anway that different formalisms have different
advantages and drawbacks. The interesting thing would be to find out
what is easier and what is more cumbersome in which framework.

As I said in a previous mail. Traditional approaches didn't have
universes and fibrations were partly invented to overcome this
shortcoming at the price of having to externalize reasoning.

But there is also extensional type theory with universes. Maybe that's
better than the other 2 approaches.

But one cannot say beforehand which setting is better for what.

What experience tells us is that different setting are good/bad for
different purposes.

That's the point I wanted to make. From my side no need for further
discussion...

Thomas

> Right, the *forward* direction requires either equality of objects or
> using "essential fibers" instead of fibers.  That's what I meant by
> saying a displayed category is a "refinement" of a functor: you can
> make a functor from a displayed category, but the opposite direction
> is harder.  That doesn't mean that you can't express composition of
> functors in terms of displayed categories: it just means you can't (or
> shouldn't) do it in the naive way by first making your displayed
> categories into functors, composing them, and then going back to a
> displayed category.  Instead you just have to "lift" functor
> composition to displayed categories in the same way that we lift
> function composition to Sigma-types.
> 
> Suppose D is a displayed category over C, with types of objects obD(x)
> : Type and types of morphisms D(f) : D(x) -> D(y) -> Type for x:ob(C)
> and f:hom_C(x,y).  Then we can form a total category Sigma(C)D whose
> type of objects is Sigma(x:ob(C)) obD(x) and whose types of morphisms
> are similar Sigma-types.  Now suppose we have a further displayed
> category E over Sigma(C)D.  Then applying associativity of
> Sigma-types, we can construct a displayed category Sigma(D)E over C,
> with type of objects ob(Sigma(D)E)(x) = Sigma(y:obD(x))obE(x,y) and so
> on, whose total category is equivalent (indeed, definitionally
> isomorphic, if Sigma-types have definitional beta and eta) to
> Sigma(Sigma(C)D)E such that its projection functor corresponds to the
> composite of the two functors.
> On Fri, Nov 9, 2018 at 3:56 AM Thomas Streicher
> <streicher@mathematik.tu-darmstadt.de> wrote:

-- 
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.