Toots for jcreed@mastodon.social account

Written by jcreed on 2025-01-26 at 19:13

like, "humans were not meant to count that high" weird

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-26 at 19:13

I... made a record type at universe level Typeω on purpose. That feels weird.

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-22 at 18:19

For example, the reader applicative

FA = S → A

can implement all of the above with

pure a = λ _ → a

f ⟨*⟩ x = λ s → (f s) (x s)

Γ A = (s : S) → A s

f ⟨*⟩d x = λ s → (f s) (x s)

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-22 at 18:15

Is there a canonical notion of "dependent applicative functor"?

If the universe of types is named U, then I imagine wanting imagine wanting a map F : U → U with, as usual for an applicative,

pure : A → FA

⟨*⟩ : F(A → B) → FA → FB

but I'd also like a notion of "global section"

Γ : FU → U

so that I can do "dependent function application under F"

⟨⟩d : F((x : A) → B x) → (a : F a) → Γ ((pure B) ⟨⟩ a)

Is this a thing? Does it arise out of nicer axioms than these, maybe?

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-17 at 14:02

wait, so: given types A and B, is it possible to construct (allowing, say, HITs but not the univalence axiom) a "microcosm" univalent universe that only need have codes for specifically A and B, i.e. the data

E C : Type

p : E → C

such that

cA cB : C

fiber p cA ≃ A

fiber p cB ≃ B

(c₁ c₂ : C) → (c₁ ≡ c₂) ≃ (fiber p c₁ ≃ fiber p c₂)

? Does this follow from having (or is it similar to the construction of) arbitrary K(G,1)? I can't tell if I need to be worried about higher coherences...

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-16 at 20:28

I trust @ncf will tell me if I messed up somewhere :)

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-16 at 20:21

I think I actually solved the puzzle from this thread! https://mastodon.social/@jcreed/113817949467897065

Here's my claimed solution

https://github.com/jcreedcmu/parametricity/blob/430e33c7a9ea0d381b84118260ca0b64ad4e32f5/StrictEquiv.agda

It's a definition of isEquiv : (f : A → B) → Type such that

• isEquiv is a mere proposition

• if you define A ≅ B = Σ (A → B) isEquiv then you can define a definitionally involutive

invert : (A ≅ B) → (B ≅ A)

which definitionally preserves the identity equivalence, and definitionally exchanges f ↔ f⁻¹ and section ↔ retraction

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-14 at 15:49

... but to see the H version of OTT defining identity types for A by recursion on A and still maybe keep higher homotopy information is intriguing? (the acronym coincidence of HoTT and HOTT is grimly hilarious)

Something about defining a type constructor by recursion like that is still weird to me, but I see the advantages. Things being equal on the nose is nice when you can get away with it.

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-14 at 15:47

Ok, I've gone from "I have heard about the entire world of OTT but know zero about it" to "Shulman's talks/slides on higher OTT seem approachable and I get the appeal". For whatever reason I have a very "No one shall expel us from the paradise which Cantor has created for us" gut feeling that maybe biases me against anything that has a whiff of adopting UIP as a principle...

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-12 at 23:21

Lol this is a bummer

check1 : (eq : A' ≅ A) → funIsEq (eq .snd) ≡ invIsEq (invEquiv eq .snd)

check1 eq = refl

check : (eq : A' ≅ A) → invIsEq (eq .snd) ≡ funIsEq (invEquiv eq .snd)

check eq = refl

check2 : (eq : A' ≅ A) → retIsEq (eq .snd) ≡ secIsEq (invEquiv eq .snd)

check2 eq = refl

check3 : (eq : A' ≅ A) → secIsEq (eq .snd) ≡ retIsEq (invEquiv eq .snd)

check3 eq i a j = {!!} -- not definitionally equal

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-11 at 17:01

is something wrong with me that balatro just feels... random and not fun? don't wanna yuck your yum, but idgi

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-11 at 15:40

@ecavallo @amy @cbaberle (dgmw, I love modalities and substructurality! but what I love even more is whittling down required machinery)

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-11 at 15:40

@ecavallo @amy @cbaberle and by "discrete" I mean the notion "a map from the interval is the same thing as a constant map" that I can state without invoking any flat/crisp/modality/etc. stuff

Fundamentally, I am asking: can I get away without thinking about either modalities or substructurality, or can I learn something interesting about why those are necessary from why this attempt fails?

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-11 at 15:38

https://jcreedcmu.github.io/posts/2025-01-11/ I put up a blogpost with some stuff I've been thinking and agda'ing about lately, which has been only possible thanks to @ecavallo @amy @cbaberle helping me along a bunch lately!

As usual there is a decent chance it's either inconsistent or not novel, but it's fun to think about.

The main question to the experts is: can I get away with doing what I do here, postulating that the parametricity interval commutes with pushouts as long as all the components are discrete?

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-09 at 16:42

maybe I can do it by relating it to the weaker property that all functions T → A are constant...

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-09 at 15:48

Say a type A is T-discrete if the constant combinator A → (T → A) is an equivalence. Is there a nice cubical way to show that if A is T-discrete, and for every (a : A) we have B a is T-discrete, then Σ A B is T-discrete? I think I might succeed if I slog through the path computations, but they get thick fast when I try to do it directly.

(doing it for nondependent products is easy, it's the dependency that kills me)

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-04 at 23:29

Me sowing dependent products: Haha fuck yeah!!! Yes!! Me reaping the consequent path existence obligations: Well this fucking sucks. What the fuck.

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-04 at 23:28

why is it that sigma types are absolutely the bread and butter, the invisible, ubiqitous, healthsome water of informal mathematics, what could be more natural than supposing some objects that have some properties, and yet when I have to reason about them in a proof assistant, it's nothing but tears, wailing, gnashing of teeth, and desperate pleas to the gods of hcomp and hfill

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-02 at 20:03

@cbaberle hmm my current guess is it might be ok for just coproducts but is very sketchy for pushouts; specifically I'm picturing the presheaf category for reflexive graphs, and T being the one edge representable

=> More informations about this toot | View the thread

Written by jcreed on 2025-01-02 at 19:17

so in reading https://hyrax.cbaberle.com/index.html I'm wondering... @cbaberle you mention we can't fully axiomatize "...these amazing right adjoints directly in the internal language of all types..." without modality & crispness etc. I don't have Licata-Orton-Pitts-Spitters fully paged in to know, but: can I state internally without anything exploding that, for an interval-ish, cohesion-ish type T that T → — preserves some colimits? Like, the expected map (T → A) + (T → B) → T → (A + B) is an equivalence?

=> More informations about this toot | View the thread

=> This profile with reblog | Go to jcreed@mastodon.social account