Minh Today at 10:58 AM In the definition of raa->tnd, could someone explain why the {P : prop} and {Q : prop} are necessary? (edited) image.png image.png

6 replies

Roger Bosman 1 hour ago I think this is how you introduce a forall quantifier in Agda

Roger Bosman 1 hour ago This way you know RAA holds for any P, which means you can feed it nntnd

Jacco Krijnen 1 hour ago It might be insightful to rename these P and Q to R and S for example (the other P and Qs are all quantified on the top-level, whereas these are higher-order)

Minh 1 hour ago ah okay, is this the same as RankNTypes or existential types in Haskell? (edited) New

Eddie Jones 10 minutes ago Yeah it is somewhat like (forall p. RRA p) -> (forall q. TND q)

Eddie Jones 9 minutes ago Which is equivalent to the type (forall p. RRA p) -> TND q but not the default RRA p -> TND q :heart: 1

Minh I’m a bit confused about the actual meaning of strictly positive and positive: Strictly positive means that a recursive type can only occur on the RHS of an arrow in a type of the constructor. Why does this prevent non-termination? Why does this apply only for arrow types of the constructor, and not the arrows which form the actual constructor itself? e.g. data Good : Set where good : Good -> Good -> Good – Good still appears on the LHS if we consider the whole type signature an arrow type Positive means that a recursive type appears on the LHS of an “even number of arrows” - what does this mean? The “even number of arrows” bit is a bit mysterious to me. Thanks a lot!

Florian Chudigiewitsch 7 minutes ago I find that it is well explained in https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/course.pdf chapter 8.4.4

Minh 4 minutes ago thanks, i’ll take a look! :slightly_smiling_face: Eddie Jones 1 minute ago If you permit a constructor lam : (D -> D) -> D for the datatype D then you can define the untyped lambda calculus and in particular (\x. xx)(\x . xx) which doesn’t terminate. It only applies to arrows type for constructor arguments which is why you can have a constructor of type Good -> Good -> Good this is because you can think of this as curried short hand for (Good x Good) -> Good but I cannot apply the same trick to lam constructor

Minh 12:09 PM Couple of questions!

“Let us look at some other examples of categories. We can use the natural numbers to define some categories: The category ! has as objects the natural numbers and morphisms are given as hom !mn = m <= n. This is a category because <= is reflexive and transitive and those properties give rise to identity and composition. The laws hold trivial because there is at most one element of a proposition. This category is an example of a degenerate case of a category: it is a preorder, i.e. a relation that is reflexive and transitive. Question 4 Has this category an initial or a terminal object?”

• “The laws hold trivial because there is at most one element of a proposition” - i’m not really sure what this means?

• The initial object would be 0, but i’m not sure what the terminal object would be?

Eddie Jones 12:12 PM To verify that this forms a category we need associativity of composition and the identity law which means that (f . g) . h = f . (g . h) and f . id = id . f = f. But in this case morphisms f : m -> n merely witness the fact that m <= n so there either is or isn’t an morphism. In which case the laws comes for free because any two morphisms of the same type are equal. For example if I have f : 0 -> 1 and g : 0 -> 1 then f = g because they don’t contain any information other than 0 <= 1 if that makes sense?

12:13 And yeah the initial object is 0 and there isn’t a terminal object unless you extend it to have an infinity natural number

Minh 12:34 PM Does this category make sense to anyone: How can we have one object - what is this object?! “Another category we can be build from natural numbers has only one object and its morphisms are the natural numbers. The identity morphism is 0 and composition is given by addition. The laws follow from the fact that 0 is neutral (n +0= n =0+ n) and (+) associative (l + m) + n = l + (m + n). Here we exploit the algebraic properties of +, namely that it is a monoid; hence categories with one object correspond to monoids. "

12:36 … unless its literally the object representing the domain of Nats

Eddie Jones 12:36 PM The object doesn’t really have to represent anything 12:36 I is just an abstract * 12:37 I guess this is where the intuition that the category of Sets gives you starts to break down - there is no contents to the single object of this category it is not like a set at all 12:41 This category has kinda the opposite structure to the previous one. In that case we have lots of objects labelled by the natural numbers (but we can just think of them as abstract labels) and these objects are related by <= but we don’t need to name morphism because they are all equal whereas in this category we have one object which we don’t need to name because well there is only one but lots of different morphisms labelled by the natural numbers 12:42 The point is that objects and morphisms can be literally anything without any context as long as they have the right laws

Minh 12:42 PM ah i see, thanks! i’ll have to deal with this uncomfortableness for now 12:43 is this object both the terminal and initial object? or are there none at all

Eddie Jones 12:44 PM Yeah it is both 12:44 Which is sometimes called the zero object :+1: 1

12:46 The trick with category theory is to not think about it too much :joy: New 12:48 But in a legit way, like we often work at different levels of granularity. We might be interested in what a specific object is but we also might not care and actually just wonder how it is related by morphisms to other objects. We then might be thinking about a specific functor and wonder how it maps morphisms in one category to morphisms in another or we might just be thinking about the category of categories in which case a functor is just another morphism :heart: 1