feat: UHomSeq el, code, Pi, lam, Sigma

[Jlh18]

• I changed the definition of UHom so that top map in the pullback square defining the universe is not merely propositional. @Vtec234 and I discussed this a while back I remember - and we agreed that it should be data.

• I defined el and code, and proved their basic properties, including the fact that el (code A) = A and code (el a) = a

• @u5943321 defined the universe max operations needed for Pi, Sigma, lamda

[Jlh18]

@digama0 is it okay that mkPair is written in tactic mode? Maybe we don't ever need to unfold that definition so it's okay? And also it should follow from a more general (and maybe less confusing?) statement about polynomial endofunctors.

[digama0]

@digama0 is it okay that mkPair is written in tactic mode? Maybe we don't ever need to unfold that definition so it's okay? And also it should follow from a more general (and maybe less confusing?) statement about polynomial endofunctors.

Tactic mode is just another way of writing terms, it makes no difference for definitions. What actually matters is whether you use tactics like rw and simp outside of proof contexts, and in this code the rw is called only after zooming in on ?_ that is a proof goal in:

by
  refine compDomEquiv.mk _ t (ym(eqToHom congr(s[i].ext $t_tp)) ≫ B) u ?_ ≫ s.pair ilen jlen
  rw [u_tp, ← Functor.map_comp_assoc]; subst A; simp

This is just the same as

compDomEquiv.mk _ t (ym(eqToHom congr(s[i].ext $t_tp)) ≫ B) u
  (by rw [u_tp, ← Functor.map_comp_assoc]; subst A; simp)
  ≫ s.pair ilen jlen

but easier to format.

[Vtec234]

Suggested change

	/- It is useful to be able to talk about the underlying sequence of Homs in a UHomSeq.
	For such a sequence, we can loosen the condition i < j to i <= j
	without creating Type in Type.
	This is helpful for defining `s[i] → s[max i j]` for Pi and Sigma below.
	-/
	/-- The composite natural model `Hom` from `s[i]` to `s[j]`, where `i ≤ j`.
	This is helpful for defining `s[i] → s[max i j]` for Pi and Sigma below.
	Note that a `UHom` only exists when `i < j`. -/

I think UHom is probably just a bad concept, it's not a hom at all (because Type : Type). But we can leave changing that for later.

[digama0]

What makes it not a hom? It's just a special kind of hom, the actual category structure is over Hom (which is reflexive). It could be expressed as a property or extra data on a hom, but as it says it is bundled for convenience.

[Jlh18]

I moved NaturalModel.Hom things up because that structure is general and well-behaved and often the definitions we want for UHomSeq can be defined at that generality. We could also consider making it even more general, for cartesian squares between UvPolys.

[Vtec234]

What makes it not a hom?

It's not reflexive.

[Jlh18]

I think is quite a strange thing to consider category-theoretically. So it is probably not worth thinking of it as structure on a hom

[digama0]

I mean a UHom is a Hom just like an abelian group is a group, there is an additional property on top of another thing which has the base name. An example from category theory would be something like an epimorphism or a projective object, just because it's an epimorphism doesn't mean it's not a morphism anymore, and not all categorical properties are closed under id and comp.

[Jlh18]

I agree with all of that. My point is that I don't see a way to phrase this definition in a way that is invariant under equivalence of categories Cart C ~~ E. Maybe there is, I don't know

[digama0]

The notion doesn't really make sense; this is not a pure categorical definition, it comes with additional data. In any case, that is by no means a requirement for something to be a valid notion