SIP details

[JacquesCarette]

I was reading 1Lab.Univalence.SIP and had some questions:

• aren't there even simpler structures, where is-hom is \top or \bot?
• I really don't understand why the structure with the identity type constructor is pointed. (The likely source of my misunderstanding comes from the fact that I've coded a lot of structures by seeing them occur as left adjoints, and this is clouding my understanding. Though now that I think of it, it resembles what happens with the two different formulations of lenses where the identity in one case corresponds to unit introduction/elimintation in the other...)
• surely coproduct of structures works too?
• likely, indexed products (and coproducts) work too. [Reason: both containers and species]
• re: the awkwardness for ∞-Magma: this appears to be a side-effect of currying. It would be interesting to see what happens when
  1. you uncurry
  2. you give yourself a combinator for "native" binary functions.
• I think my misunderstanding about pointed carries over here, as I don't understand at all why pointed appears in relation to ∞-Magma. To me, the empty ∞-Magma exists just fine, so I'm experiencing some dissonance there.
• are there other TypeWith structures that one can associate to Bool which are likewise conjugate? (I'm thinking nand here)

There's way more to be 'mined' from here, but I would like to properly understand the above before venturing too far.

[plt-amy]

• aren't there even simpler structures, where is-hom is \top or \bot?

That's a good point! That paragraph was referring specifically to univalent structures — I'll change it to make this clearer.

I believe the "⊤ structure" is univalent whenever its "shape" is a constant proposition. This is in essence a specialisation of the constantStr: if A is a proposition, then Path A x y is contractible. On the other hand, I'm not sure the "⊥ structure" is ever univalent. Are there any conditions we can impose on a type family F : Type → Type which let us inhabit

⊥ ≃ PathP (λ i → F (ua f i)) (X .snd) (Y .snd)

• I really don't understand why the structure with the identity type constructor is pointed ([...])
• I think my misunderstanding about pointed carries over here, as I don't understand at all why pointed appears in relation to ∞-Magma. To me, the empty ∞-Magma exists just fine, so I'm experiencing some dissonance there.

It's called the "pointed structure" because TypeWith pointedStr ends up becoming the pointed types: Σ[ X ∈ Type ] X. Similarly, the SIP specialised for pointedStr characterises equality in pointed types: (A ≡ B) ≃ Σ[ f ∈ (A .fst ≃ B .fst) ] (f (A .snd) ≡ B .snd).

Unfortunately, as you observed, naming breaks down when pointedStr is used in a contravariant position, since functionStr pointedStr pointedStr has "shape" λ X → (X → X), and there are certainly empty types with a unary function associated!

• surely coproduct of structures works too?
• likely, indexed products (and coproducts) work too. [Reason: both containers and species]

Haven't thought too hard about these, but I also see no reason to think they wouldn't work 🙂

• are there other TypeWith structures that one can associate to Bool which are likewise conjugate? (I'm thinking nand here)

Definitely! Any pair of operations which satisfies a "De Morgan's law" is going to lead to ∞-magmas which are equal over not. This is the case for NAND and NOR:

  not-iso' : Nand ≃[ ∞-Magma ] Nor
  not-iso' .fst = not , isEquiv-not
  not-iso' .snd = fixup {A = Nand} {B = Nor} λ where
    false false → refl
    false true → refl
    true false → refl
    true true → refl

[plt-amy]

I'm still thinking about your point re. the awkwardness of the generated definition of ∞-magma homomorphism. I think we can also get rid of it by specialising to "operation structures":

opStr : Structure ℓ₂ T → Structure _ (λ X → X → T X)
opStr τ .is-hom (A , f) (B , g) h =
  {s : A} → τ .is-hom (A , f s) (B , g (h s)) h