<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><br><div><div>On 4 Oct 2010, at 22:26, Andreas Abel wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div>Thorsten, I mostly agree with your exposition.<br><br>But we also need to distinguish:<br><br>1) Internal representation. (sum, products, (co)induction)<br>2) External syntax. (data and record)<br><br>In particular, I do not think that Agda's record syntax is a very good idea and think that Haskell's syntax is better. In my practical experience, it is not an uncommon refactoring to turn a "record" into a data type by adding a field:<br><br> data D = C1 { f1 :: A1, ..., fn :: An } -- "record"<br><br>later add:<br><br> | C2 ...<br><br>In Agda you have to rewrite record syntax into data syntax if you want to do this change.<br><br>Also, being a record is not necessary tied to having exactly one constructor, and you put forward the Vec example, which is an indexed record.<br><br>In my opinion, a record is more extensionally given as a data types whose complete set of projections is definable. Lists are not records because their constructors are overlapping (both produce a List A), </div></blockquote><div><br></div><div>Just to state the obvious, Lists can be represented as records namely:</div><div><br></div><div><div>record List (A : Set) : Set where</div><div> constructor list</div><div> field</div><div> isCons : Bool</div><div> hd : T isCons → A</div><div> tl : T isCons → List A</div><div><br></div><div>Btw, when trying to define append</div><div><br></div><div><div>append : ∀ {A} → List A → List A → List A</div><div>append (list true h t) bs = list true h (λ _ → append (t _) bs)</div><div>append (list false _ _) bs = bs</div><div><br></div><div>the termination checker complains. I am not sure why, since (t _) is smaller than (list true h t), isn't it? </div></div></div><div><br></div><blockquote type="cite"><div>but Vec's constructor's are not overlapping (one produces a Vec A zero, the other a Vec A (suc n), which cannot be confused).<br><br>In MiniAgda you can define the Vec record by<br><br> data Vec (A : Set) : Nat -> Set<br> { vnil : Vec A zero<br> ; vcons : [n : Nat] -> (vhead : A) -> (vtail : Vec A n) -> Vec A (suc n)<br> } fields vhead, vtail<br><br>which creates the two destructors vhead and vtail.<br><br>The big question is: which indexed records give rise to modules?<br><br>Encoding indexed records in the way you describe below works of course, but is it a practical solution?<font class="Apple-style-span" color="#000000"><font class="Apple-style-span" color="#144FAE"><br></font></font></div></blockquote><div><br></div>No, I guess we want the destructor syntax. But it least it is clear what it means.</div><div><br></div><div>Cheers,</div><div>Thorste</div><div><br><blockquote type="cite"><div>Cheers,<br>Andreas<br><br><br><br><br>On Oct 4, 2010, at 7:49 PM, Thorsten Altenkirch wrote:<br><br><blockquote type="cite">I think it is a good idea if we distinguish two issues:<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">1) The definitions of datatypes by constructors or destructors<br></blockquote><blockquote type="cite"> corresponding to labelled sums (data) and labelled products (codata)<br></blockquote><blockquote type="cite">2) The definition of recursive datatypes as either inductive or coinductive<br></blockquote><blockquote type="cite"> corresponding to initial algebras or terminal coalgebras.<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">E.g. sometimes it is more natural to represent coinductive datatypes in their constructor representations, eg. for colists. Also decoupling the two allows a flexible syntax for mixed inductive / coinductive datatypes (see Nisse's and main recent papers on this).<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">In any case, I think it is a good idea to dualize our current way to define indexed datatypes by indexed constructors to indexed records defined by destructors as Dan and Andreas suggest. To add another example, we can define Vec using destructors:<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">record Vec (A : Set) : ℕ → Set where<br></blockquote><blockquote type="cite"> destructor<br></blockquote><blockquote type="cite"> hd : ∀ {n} → Vec A (suc n) → A<br></blockquote><blockquote type="cite"> tl : ∀ {n} → Vec A (suc n) → Vec A n<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">Dually to the fact that we can encode indexed datatypes using equality and sigma-types, we can can encode these indexed records using eqaulity and pi-types, namely<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">record Vec (A : Set)(n : ℕ) : Set where<br></blockquote><blockquote type="cite"> field<br></blockquote><blockquote type="cite"> hd : ∀ {m} → n ≡ suc m → A<br></blockquote><blockquote type="cite"> tl : ∀ {m} → n ≡ suc m → Vec A m<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">And we can recover the constructors:<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">nil : ∀ {A} → Vec A 0<br></blockquote><blockquote type="cite">nil = record {hd = λ () ; tl = λ ()}<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">cons : ∀ {A n} → A → Vec A n → Vec A (suc n)<br></blockquote><blockquote type="cite">cons {A}{n} a as = record {hd = λ _ → a;<br></blockquote><blockquote type="cite"> tl = λ eq → tl' eq}<br></blockquote><blockquote type="cite"> where<br></blockquote><blockquote type="cite"> tl' : ∀ {m} → suc n ≡ suc m → Vec A m<br></blockquote><blockquote type="cite"> tl' refl = as<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">Cheers,<br></blockquote><blockquote type="cite">Thorsten<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">On 4 Oct 2010, at 09:04, Andreas Abel wrote:<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite"><blockquote type="cite">Hi Dan,<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">thanks for your post. It's a pity you were not at the last Agda meeting in Nottingham where Anton Setzer gave a talk on this. We have been discussing coinduction for two years on the Agda meetings now, an the conclusions we reached were quite similar to what you present here.<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">This is my own digest of the discussion. Basically, when you write (in fantasy Agda)<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">codata Stream (A : Set) : Set where<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> cons : (head : A) -> (tail : Stream A) -> Stream A<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">this means that you are defining a corecursive record<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">record Stream (A : Set) : Set where<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> destructor<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> head : Stream A -> A<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> tail : Stream A -> Stream A<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">I am using a keyword "destructor" here instead of "field", because field does not allow you to mention the record you are destructing in the type. But this is important for coinductive families, as you also point out, or, we could also call them "indexed records".<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">It comes natural then to extend pattern matching to destructor patterns, so the constructor is creating an object defined by its observations.<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">cons : .{A : Set} -> A -> Stream A -> Stream A<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">head (cons a as) = a<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">tail (cons a as) = as<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">Of course, cons and the destructors could be created automatically from the above "codata" definition. If you go on and define map you get<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">map : .{A B : Set} -> (A -> B) -> Stream A -> Stream B<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">head (map f s) = f (head s)<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">tail (map f s) = map f (tail s)<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">map does not reduce by itself, only if its head or tail is demanded. Thus, there is no special care needed to prevent looping of the type checker in the presence of corecursion anymore. Also, the subject reduction problem discussed on the Coq and Agda lists (posted by Nicolas Oury) is gone.<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">The above definition of map could be generated from the constructor-based one automatically, I suppose, and should be the internal representation (part of the deal has been realized by Nisse and me already as "record pattern translation").<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">An interesting special case is the Unit type (empty record)<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">codata Unit : Set<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> destructors<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">We get<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">unit : Unit<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">() -- no destructors<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">and this makes, as you observed below, Unit the terminal type<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">terminal : .{A : Set} -> A -> Unit<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">()<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">(We probably need a better syntax for "no destructors", maybe<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">terminal a = ()<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">to indicate that "terminal a" is of a type which has no destructors.)<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">Then we can go on and have indexed records, as you also observe.<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">data Fin : ℕ → Set where<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> mk : ∀{n} → Maybe (Fin n) → Fin (suc n)<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> empty : ⊥ → Fin 0<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">This could be represented as<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">record Fin : Nat -> Set where<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> destructors<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> fromSuc : .{n : Nat} -> Fin (suc n) -> Maybe (Fin n)<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> fromZero : Fin 0 -> Bot<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">and then we get the constructors<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">mk : .{n : Nat} -> Maybe (Fin n) -> Fin (suc n)<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">fromFin (mk m) = m<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">-- fromZero does not match<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">empty : Bot -> Fin 0<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">empty ()<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">or<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">fromZero (empty a) = a<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">Cheers,<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">Andreas<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">On Oct 4, 2010, at 4:47 AM, Dan Doel wrote:<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">On Sunday 03 October 2010 6:10:34 pm Nils Anders Danielsson wrote:<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">On 2010-10-01 15:09, Iain Lane wrote:<br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">record Tailspin : Set where<br></blockquote></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">field<br></blockquote></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> Kaboom : Tailspin<br></blockquote></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">test : Tailspin<br></blockquote></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">test = ?<br></blockquote></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">I think the problem here is that you are using a recursive record type.<br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">Such types are not really supported, but for some reason they are not<br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">disallowed, maybe to allow experiments with coinductive records:<br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">record Stream (A : Set) : Set where<br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> constructor _∷_<br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> field<br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> head : A<br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> tail : ∞ (Stream A)<br></blockquote></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">I posted this in response to an issue on the bug tracker* (so sorry if you're<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">seeing this twice), but there may be some eyes here that it wouldn't reach<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">otherwise, and it's related to the above.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">I was thinking not long ago about notations for defining codata. One nice<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">special case is when the functor in question is a product. Since the<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">observation is then T -> FT*GT*..., you can write it like:<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">codata Stream A = Head :: A & Tail :: Stream A<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">But, I was thinking about a more GADT/inductive family-like syntax, and the<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">obvious choice is:<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">codata Stream (A : Set) : Set where<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> head :: Stream A -> A<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> tail :: Stream A -> Stream A<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">where the list specifies the destructors, and the type being defined is a<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">product thereof, instead of a sum as in the inductive case (and this is<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">probably not surprising; inductives and sums are colimits, and coinductives<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">and products are limits). Charity handles type definitions in this way.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">But, in the ordinary coinductive case, the first argument is always the same,<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">so we could think about eliding it, which of course produces the suggestive:<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">codata Stream (A : Set) : Set where<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> head :: A<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> tail :: Stream A<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">and this looks exactly like records. And, in fact, it doesn't just look like<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">records, it *behaves* a lot like (Agda) records in several ways.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">1) Both records and codata are defined by the observations that can be<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">performed on them, rather than how they're constructed, as inductives are.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">2) The eta rule for records is very much like proper extensional equality for<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">coinductive types: two values are equal if all observations/projections of the<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">two are equal. For instance, for the empty record:<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">record ⊤ : Set where<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">with no projections, as a codata, we'd expect to, for any type not needing to<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">support any observations, there to be a canonical injection into the empty<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">record:<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">ana : ∀{A : Set} → A → ⊤<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">ana _ = _<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">term : ∀{A} → (f : A → ⊤) → f ≡ ana<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">term f = refl<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">And lo and behold, there is. Not that this isn't equally justified by<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">induction for non-recursive records (inductive and coinductive records should<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">coincide when non-recursive), but the focus on equality of<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">projections/observations seems like a coinductive take.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">3) In the bug in question, there was a problem with the termination checker<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">not accepting code involving something like:<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">foo ... (x , y) = ... (foo ... x) ... (foo ... y) ...<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">because the match on (x , y) is translated to projections from the record.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">However, Nils also pointed out that the following code should not check:<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">record R : Set where<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> constructor c<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> field<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> p : R<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">foo : R -> R<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">foo (c r) = foo r<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">because it translates into:<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">foo : R -> R<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">foo r = foo (p r)<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">which will not normalize (foo r => foo (p r) => foo (p (p r)) => ...). The<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">solution found was to make 'p r <= r', so that the checker is aware that the<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">argument isn't getting *bigger*, but it isn't necessarily getting smaller,<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">either (the latter part invalidates foo). However, is this situation not<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">rather strange?<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">If R were indeed inductive, we'd expect it to be empty. For instance:<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">data R : Set where<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> c : R -> R<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">¬R : R → ⊥<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">¬R (c r) = ¬R r<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">but this is exactly the function we've just ruled out, because it won't<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">normalize with records. And in the inductive case, p r must be smaller than r,<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">but we are treating it as if it isn't.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">However, if records are coinductive, the above makes perfect sense:<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">a) p r <= r, because coinductive types admit circular definitions, and so<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> projecting out of one may yield something of equal size, but not greater.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">b) foo is obviously not a productive corecursive definition, so it's natural<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> to rule it out. There's no longer a strange situation where we must rule<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> out an ostensibly inductively justified definition because it would fail<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> to normalize.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">c) It's okay that we can't prove that R is uninhabited, because it *is*<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> inhabited by c (c (c (c ...))).<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">4) I haven't bothered to think this through much yet, but: coinductives had<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">problems (and still do in Coq, I think) with subject reduction when they were<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">initially conceived of as being built out of constructors. Taking the view<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">that values of coinductive type are opaque things with observation functions<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">seems important to a well-working theory.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">When constructors and matching thereon were added for records, I believe there<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">were similar issues with subject reduction, which is why the matches are now<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">translated to projections.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">I suspect these two situations are related.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">So, how about it? Is it possible that Agda has had non-recursive coinductive<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">types all along, and that codata would have been better added by fixing the<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">way that recursive records work?<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">On the topic specified in the subject line, I've been thinking about what<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">coinductive families might look like. Inductive families are initial algebras<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">in a slice category (which makes them a way of specifying how an entire family<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">T i is constructed at once), so a coinductive family should be a final<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">coalgebra in the same. I'm not sure I have the chops to specify what that is,<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">exactly, *but*, I can speculate wildly.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">We allow the specification of inductive families by allowing constructors to<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">target arbitrary values of the index:<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">data Fin : ℕ → Set where<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> zero : ∀{n} → Fin (suc n)<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> suc : ∀{n} → Fin n → Fin (suc n)<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">So, it stands to reason that we should be able to specify coinductive families<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">by allowing projections to specify arbitrary starting indices:<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">codata CoFin : ℕ → Set where<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> pred : Fin (suc n) → Maybe (Fin n)<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> empty : Fin 0 → ⊥<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">Of course, where the 'n' comes from in the pred destructor is something I<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">haven't figured out yet. :) Perhaps the presence of the n at all is an<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">illusion in both cases. Edwin Brady et al. tell us that inductive families<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">need not store their indices**. Perhaps this is not merely an optimization,<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">but a recognition that quantification over indices is part of a schema for<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">defining many constructors, not actually a field of the constructor, and:<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">pred : ∀{n} → Fin (suc n) → Maybe (Fin n)<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">is a similarly sensible schema (apologies if the paper actually makes this<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">observation; it's been a while since I read it).<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">If this definition is a little surprising, note that we could also write Fin<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">as:<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">data Fin : ℕ → Set where<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> mk : ∀{n} → Maybe (Fin n) → Fin (suc n)<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> empty : ⊥ → Fin 0<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">which makes it a little clearer that we're dealing with the same functors<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">here.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">Thoughts?<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">-- Dan<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">[*] <a href="http://code.google.com/p/agda/issues/detail?id=334">http://code.google.com/p/agda/issues/detail?id=334</a><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">[**] <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.62.3849">http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.62.3849</a><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">Also, here's a fancier proof than the top one: the anamorphism into the<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">product record is unique. Of course, I don't expect eta rules to extend nicely<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">into providing extensional equality of recursive records-as-codata.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">module Prod where<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">record _×_ (A B : Set) : Set where<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> field<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> fst : A<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> snd : B<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">open _×_<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">ana : ∀{A B C : Set} → (C → A) → (C → B) → C → A × B<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">ana f g x = record { fst = f x ; snd = g x }<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">comm₁ : ∀{A B C} → (f : C → A) (g : C → B) → (fst ∘ ana f g) ≡ f<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">comm₁ f g = refl<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">comm₂ : ∀{A B C} → (f : C → A) (g : C → B) → (snd ∘ ana f g) ≡ g<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">comm₂ f g = refl<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">open ≡-Reasoning<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">univ : ∀{A B C : Set} → (f : C → A) (g : C → B)<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> → (h : C → A × B)<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> → (fst ∘ h) ≡ f<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> → (snd ∘ h) ≡ g<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> → h ≡ ana f g<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">univ f g h eq₁ eq₂ = begin<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> (λ x → h x)<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> ≡⟨ refl ⟩<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> (λ x → record { fst = (fst ∘ h) x<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> ; snd = (snd ∘ h) x })<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> ≡⟨ cong (λ k →<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> λ x → record { fst = k x<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> ; snd = (snd ∘ h) x })<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> eq₁ ⟩<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> (λ x → record { fst = f x<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> ; snd = (snd ∘ h) x })<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> ≡⟨ cong (λ k → λ x → record { fst = f x<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> ; snd = k x })<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> eq₂ ⟩<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> (λ x → record { fst = f x ; snd = g x })<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> ≡⟨ refl ⟩<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> (λ x → ana f g x)<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"> ∎<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">_______________________________________________<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">Agda mailing list<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">Andreas Abel <>< Du bist der geliebte Mensch.<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">Theoretical Computer Science, University of Munich<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">Oettingenstr. 67, D-80538 Munich, GERMANY<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><a href="http://www2.tcs.ifi.lmu.de/~abel/">http://www2.tcs.ifi.lmu.de/~abel/</a><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">_______________________________________________<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">Agda mailing list<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br></blockquote></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite"><br></blockquote><br>Andreas Abel <>< Du bist der geliebte Mensch.<br><br>Theoretical Computer Science, University of Munich<br>Oettingenstr. 67, D-80538 Munich, GERMANY<br><br><a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a><br>http://www2.tcs.ifi.lmu.de/~abel/<br><br></div></blockquote></div><br></body></html>