implementation · deprecated: Dialectica

Here is an Agda proof that Dial(Set)(2) is a category.
(assuming Agda Set + functions as Set)

There are 2 holes that are Cubical Agda related. I'm still filling those in. (showing that the hom set has the homotopy level set and a hole in equality of morphisms in dial)

Valeria de Paiva (May 18 2022 at 19:56):

I have now read your file, thanks! I don't quite follow the proof that Dial(Set)(2) is a category.

I was expecting proofs of associativity of composition, and of the identity triangles.
Are these subsumed into the sequence of assertions between lines 137and 139?

I'm guessing that line 135 is the definition of identity map in DialSet, but it looks a bit strange.

and I don't understand line 136, because I don't know what are compositions C and D in this case.
is this the hole you've mentioned?

I expect this is just me not knowing how the import of modules works in agda, but more pointers would be appreciated.

Eric Bond (May 18 2022 at 20:48):

(λ u → u) ∧ (λ u x → x) st (λ u x → ≤-refl)

(U , X ,  α) -> (U, X ,  α)

The first map (λ u → u) is the identity map for U.
The second map (λ u x → x) is a "projection" from U \x X to X (but in curried/uncurried form).
The last term (λ u x → ≤-refl) is of type (u : U)(x :X) → α u x ≤² α u x so the condition holds by reflexivity of ≤²

The type of the right identity is m ∘ᶜ id = m.
But to prove this we need to consider what it means for two morphisms to be equal.

Morphism consist of three components (f , F, and the condition). It suffices to show that if you have 2 morphisms, then they are equal if they are equal in the first 2 components (f and F). This is where cong-dial : f ≡ f' → F ≡ F' → m₁ ≡ m₂ comes from. So then we just need to look component wise at what the composition in the identity law is doing.

so in m∘ᶜ id = m The first component is f ∘ id = f where ∘ and id are from Set. This holds by definitional equality so it is dispatched with refl
The second component is a bit more involved.

f₁ := (λ u → u)
F₁ := (λ u x → x)
from the definition of the identity morphism

and we have some
F₂  :  U → X → X

Now we consider what composition does on F
F' : U → X → X
F' u x = let
                 u = f₁ u
                 x' = F₂ u x
                 x' = F₁ u x'
                 in x'

so F₂  is equivalent to F' and so this holds by definitional equality

Eric Bond (May 18 2022 at 20:49):

The same reasoning applies for left identity and associativity. They hold by definitional equality once you define the right notion of equality of morphisms (homotopy type theory is paying dividends here)

Eric Bond (May 18 2022 at 21:02):

and I don't understand line 136, because I don't know what are compositions C and D in this case.

_∘ᶜ_ is the name for composition in the type of PreCategories.
_∘ᴰ_ is the name of the operation defined on line 76 which is composition of morphisms in Dial(Set)(2).
So in total, line 136 is saying for the PreCategory DialSetCat , composition _∘ᶜ_ is _∘ᴰ_

Valeria de Paiva (May 18 2022 at 21:06):

great! but then where is the hole?
also when I said line 135 looked a bit strange as identity, I could see the two functions and I know this is how the identity works.
But I was expecting it to be an instance of the code in lines 49--58, not to be part of the proof, by what I expect is the import of some PreCat module. but things are much clearer now, thanks a bunch!

Valeria de Paiva (May 18 2022 at 21:10):

even if in this case the equality on f and F is on the nose, but the condition is a kind of lax equality (in Chu spaces it would be a real equality too!)

Eric Bond (May 18 2022 at 21:18):

Oh yes! That is a good point. It would be useful to not 'inline' the definition of Identity morphism since It could be used in other contexts. I'll fix that.

There are 2 holes. Holes look like this {! !}
See lines 126 and 134.
The hole on 126 is in the definition of cong-dial : f ≡ f' → F ≡ F' → m₁ ≡ m₂ where I just need to use the proof eq-maps-cond and some clever path definitions to complete the definition.

The hole on 134 is Is saying that the HomSets in DialSetCat are Sets w.r.t homotopy level.
It is missing a proof of this condition (x y : Ob) → is-set (x ⇒ y).
For folks who haven't seen this before it is basically saying that if you have two morphisms f and g and two proofs of equivalence of those morphisms p : f ≡ g and q : f ≡ g, then it is the case that p ≡ q.

This condition could be left out. It's an artifact of the HoTT book and some folks think it is easier to leave that condition elsewhere.
https://github.com/agda/cubical/issues/625

Valeria de Paiva (May 18 2022 at 21:24):

oh, ok. many thanks for the explanation of the hole then! (the other one is not a hole anymore, right?

Eric Bond (May 18 2022 at 21:30):

I'm going to remove the is-set condition for now so hole 134 will go away.
The hole in cong-dial is still a TODO.

Valeria de Paiva (May 18 2022 at 21:33):

newbie question: can we have a promissory note to fill the hole and carry on working on the monoidal structures of DialSet or without filling the holes things do not compile?

Eric Bond (May 18 2022 at 21:37):

That is a good question. The way Agda is implemented, you can usually continue working normally while there are holes and the file will still type check. for example.
Screen-Shot-2022-05-18-at-2.36.57-PM.png

Eric Bond (May 18 2022 at 21:38):

I can even normalize/evaluate the term b in this case. It reduces to ?0 tt where ?0 is supposed to be a function from Bool -> Bool defined in not, but it has not been defined.

Eric Bond (May 18 2022 at 21:41):

However if we had a file that depended on this file and I left holes on it, there would be errors in the new file.
You have some control over the behavior of this. For instance if you add the flag {-# OPTIONS --allow-unsolved-metas #-} then you could bypass this check and continue working.

Eric Bond (May 18 2022 at 21:43):

Caveats are if you leave holes "at the type level" or if you leave a hole in a term Agda needs to deduce a type. Then it complains. Generally you can leave holes at the "term level" and sometimes at the "type level".

Eric Bond (May 18 2022 at 21:48):

For the specific case you mentioned.. yes the hole for cong-dial will not prevent the file from type checking and can be left as a TODO while the monodial structure is developed.

Valeria de Paiva (May 18 2022 at 21:53):

Yay! thanks! for @Charlotte Aten we will need to do the file lineale.agda properly: starting with the definition of One, Two, Three (Kleene-style)--sets of truth-values, Nat, closed interval [0,1], etc. and it's fairly independent from Dialset, because it's just a parameter in the more complicated version of DialSet.

Eric Bond (May 18 2022 at 21:57):

While I'm rambling away, and in case any lurkers are interested, holes are not just a TODO in a proof.. they are interactive.
Screen-Shot-2022-05-18-at-2.58.02-PM.png

for instance if my cursor is in this hole there are a few different commands I can run
ctrl+c, ctrl+t - this will tell me my current "goal" or what Type of term I need to fill the hole with

ctrl+c, ctrl+a - this will begin a "proof search" where Agda will try to fill the hole with a term from the local context

ctrl+c, ctrl+n - this evaluates the current term in the hole and shows the result

ctrl+c, ctrl+e - this tells you the terms and their types in the local proof context
and many more

Eric Bond (May 18 2022 at 22:06):

Valeria de Paiva (May 18 2022 at 22:10):

yes, I know. we need the definition(s) and then the examples from "Dialectica Petri Nets" https://arxiv.org/abs/2105.12801
none of these have been automated

Eric Bond (May 18 2022 at 22:20):

sounds good :)
I'm context switching back to my 9 to 5 which is currently hardware verification using Isabelle HOL :upside_down:

Valeria de Paiva (May 20 2022 at 01:25):

@Eric Bond I still have two questions about the proof that DialSet is a category.

I was expecting cong-dial to be more like: f ≡ f' → F ≡ F' → cond ≡ cond' → m₁ ≡ m₂

I also don't understand what the extensionality of functions has to do with swapping the arguments in

Eric Bond (May 20 2022 at 16:53):

The explanation for the derivation of function extensionality turned into a wall of text.
I've decided to just make it available here.

Eric Bond (May 20 2022 at 17:11):

cong-dial : f ≡ g → F ≡ G → m₁ ≡ m₂
cong-dial p q i = (p i)  ∧ (q i)  st (eq-cond p q i)

Observe when
i := i0, (p i) ∧ (q i) st (eq-cond p q i) := f ∧ F st cond
and
i := i1, (p i) ∧ (q i) st (eq-cond p q i) := g ∧ G st cond'

eq-cond has an ugly type because it requires Dependent Path Types PathP.
The gist is

eq-cond : (p : f ≡ g) → (q : F ≡ G) →  PathP <ugly mess>  cond cond'

eq-cond : (p : f ≡ g) → (q : F ≡ G) →
        PathP (λ i → (u : U)(y : Y) → α u ((q i) u y) ≤² β ((p i) u) y) cond cond'

Eric Bond (May 20 2022 at 22:34):

Valeria de Paiva (May 21 2022 at 02:55):

Valeria de Paiva (May 21 2022 at 02:57):

Eric Bond (May 22 2022 at 04:08):

Valeria de Paiva (May 22 2022 at 04:16):

Great! this way they can go in parallel, as the next step in DialSets is the monoidal closed structure. Need to add the parallel tensor and its internal-hom.

Eric Bond (May 22 2022 at 05:10):

Valeria de Paiva (May 22 2022 at 05:36):

cool! as I wrote about the tensor in lineales one, I think we need to show functoriality in both coordinates, as we shouldn't rely on symmetry.
so I expect you to need another compat-like function

of shape perhaps something like compat : {c : Two} → ({a b: Two} → a ≤² b → (c ⊗² a) ≤² (c ⊗² b))

Eric Bond (May 22 2022 at 16:37):

Finished the tensor bifunctor.
Next up, monoidal structure. So far CatLib.agda is a spartan version of the agda-categories library but It might make sense to just use agda-categories. Thoughts? I can also merge the new developments into your repo.

Valeria de Paiva (May 23 2022 at 04:35):

Not many thoughts here (very tired after 2 days of intense workshopping at CSLI). do whatever you think works for us as a group. thanks!
but yes, please do merge the developments to https://github.com/vcvpaiva/Dialectica/.

Eric Bond (May 24 2022 at 17:37):

Valeria de Paiva (May 24 2022 at 18:35):

@Eric Bond the github repo is not working for me, because we need to have the "proof-irrelevant" structures (the several lineales) separated from the dual-sided structures DialSet, DialPos, DialTop, DialHask, etc. maybe we need another 15 min chat?

Eric Bond (May 24 2022 at 21:02):

Valeria de Paiva (May 24 2022 at 21:07):

Eric Bond (May 26 2022 at 00:07):

Valeria de Paiva (May 26 2022 at 00:09):

Eric Bond (May 26 2022 at 00:12):

Sure! Should be a Settings button near the top right under watch and fork. within settings, on the left there is a Collaborators tab. In that you should see a Manage Access page with Add people. My username is bond15 but if that doesn't show up then bond.eric.23@gmail.com should work.

Valeria de Paiva (May 26 2022 at 00:28):

Eric Bond (May 26 2022 at 05:33):

got it! Thanks!
Is there a source that lays out the definitions of the lineales that are desired?

Valeria de Paiva (May 26 2022 at 13:48):

yes, the Dialectica Petri Net paper describes some. But it would be good to "find" also existing libraries for Boolean algebra, Heyting algebra

Eric Bond (May 26 2022 at 17:56):

I was going to ask about this via email but I figured the current topic of this chat is related so...

I see you are jointly organizing a trimester at HIM on the topic of Prospects of Formal Mathematics.
I was wondering if you could share more details about that :).
(Who should join, costs, what to expect, online or in person...etc)

Valeria de Paiva (May 29 2022 at 23:22):

@Eric Bond I don't know much more than what is in the HIM page, which was our proposal. I have organized a Dugstuhl meeting before, but have not been to a HIM meeting ever, so again this is all new to me too.
Repeating the information from the HIM page here, we have 3 thematic workshops planned. But the rest is still fluid, to be decided.

Planned Activities: The trimester will organize work into:
Regular get-togethers: e.g. weekly seminars, informal workshops, and open problem sessions
Formalization Schools (both F2F and online) to get participants into the practice of formalizing mathematical knowledge

Thematic Workshops:
Formalizations in Modern Mathematics (June 2024)
Bridging Between Informal and Formal Mathematics (July 2024)
Libraries of Digitized Mathematics (August 2024)

Charlotte Aten (Jun 01 2022 at 20:48):

Hey @Valeria de Paiva , I've finally gotten the internet back and wanted to check in about the status of our project. What's been going on has been documented in the summaries and photos in the Dialectica Google drive to some extent but I will add some comments here as well. I'd like to invite you to the Overleaf document that @Eric Bond and I have for this project. Can you supply me with an appropriate email to use?

Valeria de Paiva (Jun 01 2022 at 20:51):

Sure, Charlotte. Either valeria.depaiva@gmail.com or valeria@topos.institute work. I can see in the Google Drive the summaries Day 1 and Day 2 that Jeremie posted, but I cannot see pictures at all. where are they?

Charlotte Aten (Jun 01 2022 at 21:05):

Great, you should have an invitation at the gmail address! I just uploaded the photos from today to the folder called "2022 June 1 notes - Calculations". There is a similar folder for May 30 containing photos from that day.

Charlotte Aten (Jun 01 2022 at 21:11):

On Monday I discussed the relationship between extrinsic game semantics and Negulescu's processes with the games group, which turned out to be pretty strong. There were two pretty natural ways (using the notions of strategies and coherence spaces, respectively) to view games as being included in the process space lattice Neglescu described. Moreover, we found that Negulescu's lattice embeds into the poset G(2^E) where G is the Girard variant of the Dialectica construction and 2^E is the poset of subsets of the collection of all executions in question.

Charlotte Aten (Jun 01 2022 at 21:17):

Oh and I should mention @Valeria de Paiva that the comments on that Overleaf document give a slightly more detailed outline of what @Eric Bond and I have been planning/working on for the past two days. We have a way of playing the token game for Dialectica Petri nets which generalizes what seems to be natural when the lineale in question is 2 or Z. Part of the motivation for this is based on a general algebraic consideration about lineales which is kind of a separate conversation that I will make a new conversation for.

Charlotte Aten (Jun 01 2022 at 22:01):

Jeremy asked me something about Dialectica Petri nets which I am still planning to try to understand myself but would like to ask here just in case there's a quick answer. Is there a natural way to view the category M_L(Set) used in the definition of the Petri net category Net_L as an example of the Girard variant GC for some appropriate choice of C? It seems like either there is a fundamental reason why it shouldn't be possible or there is some relatively trivial pairing that can be done and it was just written this way in the original paper in order to make the exposition cleaner. This is also of interest since reformulating M_L(Set) as GC for some C paves the way for a «modal» version of the constructions at play here, which is something I haven't really thought about myself much yet but know that @Eric Bond and @Nelson Niu have expressed interest in.

Valeria de Paiva (Jun 01 2022 at 22:04):

Sure, M_2(Set) is just GSet,exactly. It was just written as M_L(Set) to show that we can vary the L's, as it's done in the Petri nets paper.

Valeria de Paiva (Jun 01 2022 at 22:08):

So the preprint about "multi"-relations is a tiny generalization of Chapter 3, where we change 2= {true, false} into a lineale L, a linear version of a Boolean-algebra or of a Heyting algebra.

Charlotte Aten (Jun 01 2022 at 22:17):

Awesome, I will have to check that out now. Thanks so much for explaining! I'm glad I finally had a chance to get back online and ask some questions.

Valeria de Paiva (Jun 01 2022 at 22:18):

I'm really glad too!! I wasn't expecting issues with the internet, I must say. I am now home so able to talk, if you guys want to.

Charlotte Aten (Jun 01 2022 at 22:21):

That sounds great! People are going to be collecting for dinner soon so I'll head over there now and maybe we can put together a meeting afterwards and use the videoconferencing device that we were given if you'd like.

Charlotte Aten (Jun 02 2022 at 15:01):

Good morning @Valeria de Paiva ! We were wondering whether you have a particular reason for not trying to define the token game in the original Dialectica Petri nets paper. Eric and I gave a quite natural definition but found that it clashes with the notion that a 0 element of the base lineale L represents "no arc" as opposed to "an arc with cost 0". More amusingly, the dependent Dialectica construction actually fixes this problem by creating a distinction between arcs of value 0 and the absence of an arc, so we're thinking we should redo the basic setup from your paper with dependent M_L(Set) in order to be able to use tokens how we want in our construction.

Valeria de Paiva (Jun 02 2022 at 15:15):

hi @Charlotte Aten this might be a good idea. I don't do the token game simply bc I was following Winskel, who was my PN expert then. But the dependent Dialectica is problematic, I don't know how to provide structure for it--maybe Tamara's function-space works as desired, maybe it doesn't. I don't know, I'm trying to read, but going slowly.

Eric Bond (Jun 02 2022 at 22:25):

For dependent Dialectica in Set with L.. perhaps these could be shown to be adjoint?

    _⊗_ : DDial → DDial → DDial
    (pos₁ ▹ dir₁ c α₁) ⊗ (pos₂ ▹ dir₂ c α₂) = (pos₁ × pos₂) ▹ (λ { (p₁ , p₂) → dir₁ p₁ × dir₂ p₂}) c λ{ (p₁ , p₂) (d₁ , d₂) → α₁ p₁ d₁ ⊙ α₂ p₂ d₂}
        where
            open MonProset mon

    [_,_] : DDial → DDial → DDial
    [ pos₁ ▹ dir₁ c α₁ , pos₂ ▹ dir₂ c α₂ ] =
        Σ (pos₁ → pos₂) (λ f → (p₁ : pos₁)→ dir₂ (f p₁) → dir₁ p₁) ▹ (λ{ (f , F) → Σ pos₁ (λ p₁ → dir₂ (f p₁))}) c
            λ{ (f , F) (u , y) → α₁ u (F u y) ⊸ α₂ (f u) y}
        where
            open Lineale.Lineale lin

Nelson Niu (Jun 02 2022 at 23:10):

Valeria de Paiva (Jun 02 2022 at 23:25):

@Eric Bond this would be nice, but come to think of it, an exercise in Bart Jacob's book.
I had totally forgotten about that! I am sorry! Jacobs, "Categorical Logic and Type Theory", page 117, exercise 1.10.11.
but I didn't know how to do the exercise, now I have a function, thanks!!

However, what we want is a cartesian closed category and this is what took Bodil Biering, Tamara von Glehn and Sean Moss theses to produce, I expect. at least in the non-dependent case tensor product is not a cartesian product. and I think the same is true in the dependent case.

Nelson Niu (Jun 11 2022 at 21:08):

I meant to reply to this much earlier when I first saw it, but—what Eric is calling DDial is his Agda code above (dependent Dialectica in Set with L, indeed with any locally small category C) is also Cartesian closed, no? The formula for the Cartesian closure is just quite a bit messier…

Valeria de Paiva (Jun 11 2022 at 21:40):

I find this hard to believe @Nelson Niu . I think the structure we do have on DDial is symmetric monoidal closed, but not cartesian closed. but a proof would be good. my proof is for non-dependent objects only.

Nelson Niu (Jun 11 2022 at 21:42):

Just checking—what do you mean by “structure”? I’m taking “monoidal closed” to mean a specific monoidal product has a closure operation—then “Cartesian closed” just means the Cartesian product is closed, so these would be for different monoidal “structures” on DDial

Nelson Niu (Jun 11 2022 at 22:22):

There’s a proof in Sean Moss’s talk; there’s also a way to compute it directly that I have handwritten somewhere, I can write it up soon

Valeria de Paiva (Jun 12 2022 at 06:12):

but we know that the cartesian product in DDial is (I\times J, A_i+ B_j, the right relation), right?

so saying the category is cartesian closed would mean finding an internal-hom (or exponent) for this monoidal structure. this is what I do find difficult, the monoidal structure we have an internal-hom for is the parallel product, not the cartesian product.

Nelson Niu (Jun 12 2022 at 06:16):

Okay, then we’re talking about the same thing! There is in fact an internal-hom for the Cartesian product in DDial. Unlike the parallel product’s internal-hom, the full subcategory of nondependent objects is not closed under this operation, which is why the Cartesian closure doesn’t exist in the nondependent Dial setting. But it does exist in DDial. The formula is not very pretty, but (with the benefit of hindsight…) there’s a fairly natural way to derive it just by shifting around some sums and products

Valeria de Paiva (Jun 12 2022 at 06:17):

Valeria de Paiva (Jun 12 2022 at 06:19):

Nelson Niu (Jun 12 2022 at 06:19):

(Incidentally, in my mind this is a heuristic benefit of thinking about all this literally in terms of “polynomials”—computations then become as easy as expanding sums and products the way you’d expect them to work)

Nelson Niu (Jun 12 2022 at 06:22):

This very likely won’t make sense without more context, but here’s the derivation of the formula from my notes in any SigmaPiC:

Nelson Niu (Jun 12 2022 at 06:26):

Valeria de Paiva (Jun 12 2022 at 12:38):

Thanks @Nelson Niu !. I was not doubting the cartesian closure of SigmaPiC, but of DDial, in the terminology we just established. SigmaPiC is defined from the completions, from above as it were, I totally believe that it's cartesian closed. DDial is defined from objects and maps, from the ground up, so I was expecting a formula in terms of A_i's and B_j's that we then would prove equivalent to SigmaPiC.

so we were talking about the same problem, but about different potential solutions all along.

Nelson Niu (Jun 12 2022 at 16:20):

When we’ve been working with SigmaPiC, we’ve also been using the explicit ground-up, objects-and-maps construction for it (which has been shown to be the completion already). So we know everything is equivalent already, and the formulas are the same

Nelson Niu (Jun 12 2022 at 16:31):

Here’s the formula for the Cartesian closure in more familiar (I, A_i, P) notation:

Nelson Niu (Jun 12 2022 at 16:32):

Valeria de Paiva (Jun 12 2022 at 18:42):

thanks! but here you've lost me! what's s_i? what's the bar? why the product of b's in B_ji minus(??) s_i?

Nelson Niu (Jun 12 2022 at 18:49):

Nelson Niu (Jun 12 2022 at 18:51):

Nelson Niu (Jun 12 2022 at 18:57):

In fact, a “reason” for the lack of prettiness is that writing objects in DDial in this way, as two sets and a predicate on them, forces you to write them in “normal” form, as Jeremie and the games co. call it. We know every object can be written in this compact, normal form, involving two sets—one you sum over, one you take a product over—because distributively lets you shift sums and products around, but that doesn’t mean that’s always the most natural way to think about them or write them down, especially if they originated from an “extensive” form consisting of a product of sums or something more complicated

Jonathan Weinberger (Jun 21 2022 at 16:04):

Charlotte Aten (Jun 21 2022 at 16:17):

Eric Bond (Jul 01 2022 at 15:29):

One note: The graphic in the paper is drawing f on transitions instead of places. This is inconsistent with what the paper describes where f is a map on places and F is a map on transitions. (I chose to implement the latter)

Valeria de Paiva (Jul 02 2022 at 12:43):

Valeria de Paiva (Jul 04 2022 at 13:12):

Nelson Niu (Aug 13 2022 at 18:55):

So I've been learning (Cubical) Agda from the HoTT summer school and figured I'd try proving Poly (and eventually Dial etc.) is a category myself. I finally learned enough by yesterday to do it, and finished it up today here!

Of course Eric has done most of this already, but the key difference (please correct me if I'm wrong, @Eric Bond!) is that what we'd think of as a category is what the HoTT folks call a precategory. Agda with HoTT makes a distinction between more general types (think ∞-groupoid) and more specific sets (think an ∞-groupoid that is provably a 0-groupoid). So what they call a category has a further requirement that hom-types really are hom-sets that needs to be proven. Eric's already shown that Poly forms a precategory, with hom-types; what I've done here (with a great deal of help from lemmas from the Cubical Agda library) is further show that the category of polynomials where every position-type is a position-set and every direction-type is a direction-set forms a category, with hom-sets. (I don't think this should be too hard to generalize to Dialectica.)

(There's something to be said about these constructions not really being Poly(Sets) or Dial(Sets) if we're coding them up this way—really, these are Dial([whatever category gives Agda its HoTT semantics]). This is a little too much type theory for me to think about in one sitting, though, so I'll just leave this vague parenthetical remark in case anyone finds musing on that interesting...)

Eric Bond (Aug 14 2022 at 13:37):

We’ve been discussing if we want to use a precategory for simplicity or not. In Dial this boils down to: for (a b : L), does the type a <= b contain multiple inhabitants/witnesses? For natural numbers and the usual definition of >= ordering, this can be shown to be a Set (in the HoTT sense)

Eric Bond (Aug 14 2022 at 13:39):

Eric Bond (Aug 14 2022 at 13:51):

And yes, using Set on the nose is a temporary simplification. You can implement this using a displayed category or parameterizing the module with a category C with the appropriate structure. I might have a version of this somewhere.

This opens up a can of worms where you need a lot more infrastructure to reason about definitions. See MorphismsReasoning in Agda-categories.

Eric Bond (Aug 14 2022 at 14:42):

The record to sigma reflection tactic is so nice :open_mouth:. Not aware that existed

Valeria de Paiva (Sep 03 2022 at 18:09):

Eric Bond (Sep 28 2022 at 15:51):

Hello! I’d like to get back on track with formalizing things. I’ve had the good fortune of being distracted with fellowship things and getting set for PhD applications. However, I miss yelling at my computer screen because Agda won’t typecheck something.

Eric Bond (Sep 28 2022 at 15:54):

I plan on refreshing my memory later today by going over the repo and overleaf. I haven’t had a debrief for the Cupertino activities yet.

Valeria de Paiva (Sep 28 2022 at 21:14):

hi, I'm glad you miss yelling at your computer screen! I was going to write asking whether you saw Jacques Caretter talk in the Topos Colloquium last week when he discussed some of the things that make him yell at Agda.

Valeria de Paiva (Sep 28 2022 at 21:15):

I need to finish one thing before I try to open my roll of big paper stickers to try to get a debrief for myself, but working on it.

Eric Bond (Sep 29 2022 at 04:03):

Yes! I caught the first half before a meeting. I also picked up some tricks from the Homotopy Type Theory Summer School.

Stream: deprecated: Dialectica

Topic: implementation

Eric Bond (May 18 2022 at 16:10):