Show older

what about topoi? what kind of topos do they use to model dependent TT

I think elementary topoi are related to lcccs so I'm filing it under that one

How unusual. I've never seen it like this before
This explains very much the whole category of contexts thing... the empty context is the terminal object because you can always perform an empty substitution of all of the 0 variables in the empty context under any other context (because you have no terms that actually use the other context)
The direction the arrows in are sort of opposite of what I imagine a substitution to be in my head tho so I'll have to geometrically replace my vision of that lol

we interrupt this tangent on cwf to so I can take some notes down from my logic class lol
actual work to do...

after several interludes involving updating my SSN with Workday, having lunch, going to half a lecture for a class I dropped, and having some yogurt, I've finally finished going over the notes, but now I'm too tired for new category theory things to enter my brain

it's an indexed category
but why is it indexed over, like, the opposite category

okay functor from C{op} into the category of families of sets
that's a function from things in C to a family of sets (sounds good to me) and a function from morphisms in C{op} to morphisms between families of sets

so things in C are contexts and families here are types? so it's types that are well typed in those contexts?

and it's a family of terms. you give it a type and it gives you a set of terms of that type. okey doke
now given a morphism in C{op}
that's a substitution but it's op so it's the
if you reverse the
wtf is the reverse of a substitution

the morphisms in C those are substitutions Δ → Γ which means I take the free variables in Γ and I substitute them with terms that are well typed in Δ
γ : Δ → Γ = [xᵢ ↦ aᵢ]ᵢ where xᵢ ∈ Γ and Δ ⊢ aᵢ
turning that backwards I have a morphism from Γ to Δ which is a
which is um

maybe I should take notes while I read
maybe that'll help my understanding instead of only trying to read off of the paper

Finished dinner, back at it again with the categories
I don't get why substitution is from the context you end up with into the context whose variables you're substituting with the empty context as the terminal object instead of being the category from contexts you're replacing into the context you end up with and the empty context as the initial object where you can get to any context by substituting nothing from the empty context

It would certainly get rid of all the contravariant nonsense with the functor into the category of families

wym the syntax of a type theory is the initial model. what's the model of a cwf and initial in what category, the category of categories with families??

I lied I'm looking at the last little definition of morphisms between cwfs
I've forgotten what a natural transformation is and they use this funny looking arrow between functors and idk why

Did u know. Preservation of substitution is a natural transformation

The thing about cwf is that it feels like just yet another language, and as of yet I haven't been convinced that people are translating from the type theory to the category correctly, especially when I still haven't seen a translation function explicitly written out like one would for a syntactic or a set theoretic model or a logical relation

The thing about category is that it feels very nice when you do the thing in category theory land. Like when you suppose a functor and prove it has an initial F-algebra and deduce a catamorphism from initiality it's like wow so nice and easy! But then it's not always clear how results translate back into the original thing you were modeling. Like okay my inductive is shaped like a polynomial functor so I can apply all these results, but I'm not certain once I have a catamorphism how it arises in the original language where my inductive was. In the case of dependent type theories you can't just shuffle things in the initiality equation around because there's no termination argument!

A category with families really does look nice in terms of modelling substitution with low effort in an abstract way that handles all your intrinsically well-typed contexts and terms and types. But once I get a result from the category (I haven't yet), how do I know I can apply it back? In fact the category in question just has a bunch of objects, it doesn't have the shape of types yet

The name is literally a family of sets. Even if the notion of a type fits into these categories with sets in them how do I know that results about sets can be imported back into categories unless I first already have types inside the category

I find myself writing about categories using a type theoretic language, like a morphism in the category of families is a function between the indices and a family of functions where forall x in the original index it goes from blah to blah, but I've literally written it down as \forall x: X. U_x -> V_f(x) and I apply the index like it's a regular argument lmao

I think the problem is I don't actually know how a family of sets is defined in foundational set theory, and it seems like people are just like "this exists", so if something "just exists" I'm like okay this looks like a Pi type so it is a Pi type

a key feature of the notion of cwf is
that it can be presented as a generalized algebraic theory

you're really gonna make me learn One More Thing huh

Is a presheaf just a contravariant functor or are there additional properties I can assume that they haven't mentioned here beyond the functor

Like at this point if you're saying things like "D-valued presheaf over C" you can just say a contravariant functor from C to D
I'm guessing D is typically Set but in a cwf it's Fam instead so clearly it can be other categories that aren't Set-like

presheaves have a universal property whose statement I can't read so I'm going to ignore it until they bring it up

From the definition of ucwf it is immediately clear that an
initial ucwf Tucwf can be generated inductively

no it's not! show me!

A cwf is democratic provided each context Γ is represented by a type Γ in the sense that there is an isomorphism γ_Γ : Γ ≃ 1.Γ̅

what is. what's this 1. notation. pleas

The name is pretty funny though. because it's represented by a type, haha get it

oh my god it's a typo. it's supposed to be a cdot, not a .

First of all where can I file a bug report. Second of all it's going into some detail into the categorical model for unityped calculus and I'm wondering how much of it I need to understand to understand the rest of it because it's talking about Lawvere theories and unless those become important for cwfs too I'd rather not spend the brain power on it

wtf is that. why are there integrals. is this one of those limit things? stop that


as far as I can tell it should really be
∀ (Γ: 𝒞) → Ty(Γ) → Set but it's a contravariant functor from Ty(Γ) to Set
a family of contravariant functors indexed over contexts in 𝒞
(Tm(Γ))_Γ∈𝒞 where Tm(Γ) : Ty(Γ) → Set, as they'd say

oh I see. it's a dependent pair type lmao

It really took me a few good minutes to figure out that what they were doing here was just uncurrying a function with a really weird notation for a dependent pair
Granted it's meant to be a dependent product category of 𝒞 and Ty, I guess, but the notation (Ty(Γ))_Γ∈𝒞 very much does exist already in this document

If ∫ꟲ Ty is a category and its objects are ⟨Γ, A⟩, what are the morphisms between objects
because it seems like it has to be a morphism γ: Δ → Γ and a morphism _[γ]: Ty(Δ) → Ty(Γ) but then that's only between objects ⟨Δ, A⟩ and ⟨Γ, A[γ]⟩??

Why does it have to be an initial cwf anyway

I can't tell what properties arise from being initial

uncaptioned math 

this is gonna be completely impenetrable bc. it is to me. but am I reading this wrong or does this not like. type check
ok some context, we've got some definitions, with Δ, Γ : 𝒞, γ : Δ → Γ, A : Ty(Γ)

_._ : (Γ: 𝒞) → Ty(Γ) → 𝒞
_[γ] : Ty(Γ) → Ty(Δ) (N.B. this is contravariant)
_[γ] : Tm(Γ, A) → Tm(Δ, A[γ])
p : Γ.A → Γ
q : Tm(Γ.A, A[p])
⟨γ, a⟩ : Δ → Γ.A (where a : Tm(Γ, A))
γ↑A : Δ.A[γ] → Γ.A

a bunch of confusing implicit arguments but anyway. so we have

γ : Δ → Γ
φ : Γ.A → Γ.B
γ↑A : Δ.A[γ] → Γ.A
ϕ ∘ γ↑A : Δ.A[γ] → Γ.B
q : Tm(Γ.B, B[p])
q[ϕ ∘ γ↑A] : Tm(Δ.A[γ], B[p][ϕ ∘ γ↑A])
⟨p, q[ϕ ∘ γ↑A]⟩ : Δ.A[γ] → Δ.B[p][ϕ ∘ γ↑A]

so I guess I need to get from B[p][ϕ ∘ γ↑A] to B[γ]???

Sign in to participate in the conversation

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.