--- Day changed Fri Feb 02 2018
stoopkidhi, is there any way to prove that Fin 0 is empty? https://pastebin.com/tBDbdhS502/02 05:02
tomjackstoopkid: the absurd pattern works. notFin0 : Fin 0 -> False ; notFin0 ()02/02 05:20
stoopkidhrm, what's the absurd pattern do, got a link on that?02/02 05:20
stoopkidi see that being used in the definition of the explosion principle for False02/02 05:21
stoopkidnvm found it02/02 05:23
tomjackwith the induction principle https://www.irccloud.com/pastebin/IxTZjTl5/02/02 05:25
stoopkidit's easier to prove it in this one version: https://pastebin.com/LDyTrVSs02/02 05:28
tomjackyes, that one is sometimes nice02/02 05:28
tomjackI usually just let Fin (suc zero) be True OR False02/02 05:29
tomjackI mean, Fin (suc n) be True OR Fin n02/02 05:29
stoopkidoh good point02/02 05:29
tomjackor sometimes this :) https://www.irccloud.com/pastebin/Z4zjY2lD/02/02 05:30
stoopkidinteresting02/02 05:31
stoopkidwhat do you use this one for02/02 05:31
tomjackbit of best of both worlds02/02 05:31
stoopkidi see, what's the benefit of the original version that would be lacking in the (correction to) the one i posted?02/02 05:32
tomjackthe syntax is (inl tt) (inr (inr (inl tt))) or whatever instead of zero and suc02/02 05:32
stoopkidah02/02 05:33
tomjackcould use pattern synonyms for that, but sometimes I like reduction to produce things I want to read02/02 05:33
tomjackbut anyway I guess when working with Fin I always end up back at True OR -, and then associativity, commutativity, unit for OR02/02 05:35
tomjacke.g. for constructing an isomorphism between Fin (n + m) and Fin n OR Fin m02/02 05:35
tomjackoh, also, you can't pattern match on Fin n defined by recursion02/02 05:36
tomjackyou need to pattern match on n first. but the inductive Fin hides that for you02/02 05:36
stoopkidah hrm02/02 05:36
stoopkidbut this version of Fin seemed so clean to me XD02/02 05:38
* stoopkid just noticed its relation to polynomial functors02/02 05:38
stoopkidinteresting i didn't realize til just now that you could define types recursively like this02/02 05:43
stoopkiddidn't think that you couldn't, just never occurred to me to define recursive data-types outside of data declarations02/02 05:44
stoopkidso hypothetically i could use corecursion to construct infinitely large data-types like Nat and List instead of just Fin and Vec like i can do with regular recursion?02/02 05:45
tomjackI don't think so02/02 05:51
tomjackI could be wrong02/02 05:51
tomjackwith corecursion you can construct the infinite stream of sets True, True, True... which you would like to OR together to make Nat, but how to do that?02/02 05:52
stoopkidhttps://pastebin.com/CB7x41T802/02 05:59
stoopkidtypechecks but doesnt pass termination check02/02 05:59
tomjackhmm https://www.irccloud.com/pastebin/uvJibPhV/02/02 06:06
tomjackI wonder if you get something actually equivalent to the nats this way defining a certain M-type as a coinductive record in cubical agda02/02 06:10
stoopkidM-type?02/02 06:12
tomjackoh, no, that is not the nats02/02 06:12
tomjackit is maybe the conats02/02 06:12
tomjackyou can just keep saying "right" forever and never stop02/02 06:12
stoopkidthat's kinda like the nats though02/02 06:12
stoopkidas long as you always can stop02/02 06:13
tomjackI mean there is an element so that suc n = n02/02 06:13
stoopkidoh02/02 06:13
stoopkidnvm :)02/02 06:13
tomjackwell, agda can't prove suc n = n but it should be true :)02/02 06:14
tomjackuhoh : ∀ {ℓ} { : Stream (Set ℓ)} → Any  ; uhoh = inr (♯ uhoh)02/02 06:14
stoopkidright02/02 06:14
tomjackM-types are like this https://www.irccloud.com/pastebin/IAa8kCTr/02/02 06:14
tomjack(huh, so if you take M Set (\ X -> X), up to bisimulation with isomorphisms, is that some kind of set theory with infinite chains x₀ ∈ x₁ ∈ ... ?)02/02 06:22
tomjackor rather infinite chains ... ∈ x₁ ∈ x₀02/02 06:22
stoopkidhrm, not sure i follow, but, i don't really know how sized types work02/02 06:33

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!