Nik05 Nik05 --- Day changed Thu Jan 11 2018 I got a question about inductive types, I thought all sub function types need to end with the inductive type. But I got a inductive type that im not sure how it works 11/01 18:17 data P {u} {U : Set u} (A : S U) : S (S U) where P≙ : ∀ {X : S U} → X ⊆ A → X ∈ (P A) 11/01 18:18 Nik05: I guess X \in P A reduces to P A X, solving the mystery 11/01 19:14 in general the “sub function types” must indeed end with the inductive types — or better, the constructors must indeed construct the inductive, but that’s tested after normalization 11/01 19:14 Nik05: you should check where \in is defined to confirm what I’m saying, though my guess is very reasonable 11/01 19:15 sets can be seen as predicates (the characteristic function of the set), and then s \in S (element s belongs to set S) becomes S s (element s satisfies predicate S) 11/01 19:16 x in A is defined as A x 11/01 19:16 Nik05: as expected 11/01 19:17 Nik05: after seeing the definition, can you follow my reasoning? Where do you have questions? 11/01 19:17 Looking at it now, thank you pgiarrusso 11/01 19:18 welcome :-) 11/01 19:18 so X in P A indeed reduces to P A X, but shouldnt the function and in P A and not in P A X? 11/01 19:19 sorry my english 11/01 19:20 Shouldnt the function end in 'P A' and not in 'P A X'? 11/01 19:20 pgiarrusso: sorry but my inductive type is P : A -> S (S U). But the last type is P A X : S U 11/01 21:30 I still don't get it :P 11/01 21:36 Nik05: Nik05 the next question is what is S? And U? 11/01 21:49 I’m sure reducing those will take you further to the answer 11/01 21:50 S : U -> Set l 11/01 21:50 That’s its type... no definition? 11/01 21:51 And U? 11/01 21:51 S {u} U = U → Set u 11/01 21:52 thats the definition 11/01 21:52 U is the predicate variable 11/01 21:52 It looks like S X means “predicate on X” 11/01 21:52 Yes 11/01 21:54 Or is this a strange definition? 11/01 21:54 And since S (S X) means U -> S X, the mismatch indeed disappears 11/01 21:55 It’s not so strange, it’s pretty standard 11/01 21:55 But if you have more questions, it might be easier if you sent a complete example 11/01 21:56 Though maybe we’re (almost) done 11/01 21:56 Oke 11/01 21:56 Nik05: generally, the typechecker must run definitions before comparing types, and you must do the same (as we’ve done) to follow what it does 11/01 21:57 It seems that P A should be something like the powerset of A? 11/01 21:58 Yes indeed 11/01 22:00 I still don't see how it matches. P A has type S (S U) = (U -> Set) -> Set. P A X has type Set 11/01 22:03 Or 11/01 22:04 Wait 11/01 22:04 it is 11/01 22:07 pgiarrusso when i make a hole in the last return type and fill in my definition agda doesnt except the definition... 11/01 22:19 oh maybe this is a constraint problem 11/01 22:20 You’ll need to add back the Set levels to inline the definition by hand 11/01 22:21 Or maybe it’s some other such stupid detail going wrong, but guessing from here is hard 11/01 22:21 '_152 : S U' this is my constraint error 11/01 22:22 no idea how to read that 11/01 22:22 Not a complete error message; but that underscore thing is a metavariable, so it’s somehow failing to infer some implicit parameter 11/01 22:28 Nik05: again, hard to help without actual code + error, you should use a self-contained gist 11/01 22:28 Meanwhile, time to go to bed for me 11/01 22:29 have a good night pgiarrusso 11/01 22:29 thank you a lot 11/01 22:29 Nik05: good night! 11/01 22:29 thank you 11/01 22:29 next time i will, sorry thought i would get this simple problem 11/01 22:30