Extension types up to homotopy

[TashiWalde]

In a conversation with @emilyriehl, we discussed the comparison between the (inbuilt, strict) extension types along \phi \subset \psi and the weak extension types, i.e. the fibers of the restriction map (\psi -> A) -> (\phi -> A).

1) Via fiber induction, implement an easy proof that these are equivalent, functorially.

2) Deduce that a type having unique extensions along \phi -> \psi is equivalent to being local for the inclusion \phi –> \psi.

[TashiWalde]

A side question for @fizruk : For some reason, rzk does not seem able to infer the type of (τ, refl) in the expression Σ (τ : extension-type σ), (( τ, refl) =_{homotopy-extension-type σ} th) (src/simplicial-hott/04-extension-types.rzk.md, line 55), if I do not explicitly specify which equality type I am talking about (i.e. if I omit the _{homotopy-extension-type σ}). Does this make sense to you, or something it should be able to do?

[fizruk]

A side question for @fizruk : For some reason, rzk does not seem able to infer the type of (τ, refl) in the expression Σ (τ : extension-type σ), (( τ, refl) =_{homotopy-extension-type σ} th) (src/simplicial-hott/04-extension-types.rzk.md, line 55), if I do not explicitly specify which equality type I am talking about (i.e. if I omit the _{homotopy-extension-type σ}. Does this make sense to you, or something it should be able to do?

Here's the definition in question:

https://github.com/rzk-lang/sHoTT/blob/1b1ff2d71ae374be1d05f74cff0db45906d49c59/src/simplicial-hott/04-extension-types.rzk.md?plain=1#L52-L61

The problem is that the typechecker currently only considers inferring type from the left argument of the identity type, but here we need infer it from the right one. It should be possible to have a simple fix here, will try to fit in the next release :)

[jonweinb]

See also weak vs strict extension types.

[emilyriehl]

@TashiWalde I was actually working on the same thing but I'm glad you beat me to it ;) I won't have time to look at this until this evening. Would you mind leaving this open until then? (In any case, we're going to have to deal with the conflicts resulting from the renumbering.)

[TashiWalde]

See also weak vs strict extension types.

@TashiWalde I was actually working on the same thing but I'm glad you beat me to it ;) I won't have time to look at this until this evening. Would you mind leaving this open until then? (In any case, we're going to have to deal with the conflicts resulting from the renumbering.)

I apologize. I didn't realize you were also working on this. If you have a different implementation of extension-type-weakening you prefer to use, I don't mind replacing it.

EDIT: Looks like I spoofed not just one, but two people.

[emilyriehl]

No need to apologize on my behalf! This looks great. I got distracted by filling in various HoTT lemmas which I'll separate out and push separately.