I'm still trying to embed the Observational Type Theory into myself and everything in Agda.
I currently have the following universe hierarchy:
Prop : Type 0 : Type 1 : ... (∀ α -> Type α) : Type ω₀ : Type ω₁
To determine the equality of the polymorphic functions of the universe, I needed to add code for Type ω₀ , which made me add Type ω₁ to the metatheory. More on this in the previous question .
Here are the main functions of the target theory, the types of which are transferred to the metatheory using the interpretation operator ⟦_⟧ .
mutual Eq : ⟦ (π₁ lev λ α -> π₁ lev λ β -> univ⁺ α ⇒ univ⁺ β ⇒ prop) ⟧ eq : ⟦ (π₁ lev λ α -> π₁ lev λ β -> π (univ⁺ α) λ A -> π (univ⁺ β) λ B -> A ⇒ B ⇒ prop) ⟧ mutual coerce : ⟦ (π₁ lev λ α -> π₁ lev λ β -> π (univ⁺ α) λ A -> π (univ⁺ β) λ B -> Eq _ _ AB ⇒ A ⇒ B) ⟧ postulate coherence : ⟦ (π₁ lev λ α -> π₁ lev λ β -> π (univ⁺ α) λ A -> π (univ⁺ β) λ B -> π (Eq _ _ AB) λ r -> π A λ x -> eq _ _ AB x (coerce _ _ AB rx)) ⟧
This works this way, but I want to prove coherence , not postulate. There are two problems:
First
How to prove that equal types lie in the same universe? Is this true (in a constructive sense)? Due to Conor McBride , we have the following tagline
Now I think a == b means
once you know that a and b are of the same type, you will know that they have equal values
But types are meanings - doesn't that mean that "as soon as you know that a and b are in the same universe, you will know that they have equal meanings"? I ask because I cannot prove eq xy -> Eq (eq xz) (eq xy) otherwise (the document contains a more general lemma, but this is enough to get sym , trans and others). The problem is that for assigning the type cong (\z' -> eq z' z) p , where p : eq xy , cong must accept the polymorphic function of the universe, because x and y have observable equal, but defining different types. And since the equality of functions is pointwise, cong requires proof of the equality of universes where the types x and y lie. In code, it looks like this:
postulate refl : ⟦ (π₁ lev λ α -> π (univ⁺ α) λ A -> π A λ x -> eq _ _ AA xx) ⟧ cong-levOf : ⟦ (π₀ nat λ α -> π₀ nat λ β -> π (univ α) λ A -> π (univ β) λ B -> Eq _ _ AB ⇒ α ≟ℕ β) ⟧ hsubstitutive : ⟦ (π₀ nat λ α -> π₀ nat λ β -> π₀ nat λ δ -> π (univ α) λ A -> π (univ β) λ B -> π A λ x -> π B λ y -> π (π₀ nat λ γ -> π (univ γ) λ C -> C ⇒ univ δ) λ D -> Eq _ _ AB ⇒ eq _ _ AB xy ⇒ Eq _ _ (D _ A x) (D _ B y)) ⟧ hsubstitutive α β δ AB xy D rq = refl _ (π₀ nat λ γ -> π (univ γ) λ C -> C ⇒ univ δ) D _ _ (cong-levOf _ _ AB r) AB rxyq cong-≅z : ⟦ (π₀ nat λ α -> π₀ nat λ β -> π₀ nat λ γ -> π (univ α) λ A -> π (univ β) λ B -> π (univ γ) λ C -> π A λ x -> π B λ y -> π C λ z -> Eq _ _ AB ⇒ eq _ _ AB xy ⇒ Eq _ _ (eq _ _ AC xz) (eq _ _ BC yz)) ⟧ cong-≅z α β γ ABC xyzrq = hsubstitutive _ _ _ AB xy (λ _ C' z' -> eq _ _ C' C z' z) rq
The proof is provided by cong-levOf _ _ AB r , where cong-levOf postulated.
Second
Type coherence -
coherence : ⟦ (π₁ lev λ α -> π₁ lev λ β -> π (univ⁺ α) λ A -> π (univ⁺ β) λ B -> π (Eq _ _ AB) λ r -> π A λ x -> eq _ _ AB x (coerce _ _ AB rx)) ⟧
but type say sym is
sym : ⟦ (π₀ nat λ α -> π₀ nat λ β -> π (univ α) λ A -> π (univ β) λ B -> π A λ x -> π B λ y -> Eq _ _ AB ⇒ eq _ _ AB xy ⇒ eq _ _ BA yx) ⟧
π₀ instead of π₁ everywhere. The reason for this is because the type passed to refl in the hsubstitutive is (π₀ nat λ γ -> π (univ γ) λ C -> C ⇒ univ δ) and it cannot be (π₁ lev λ γ -> π₁ (univ⁺ γ) λ C -> C ⇒ univ⁺ δ) as necessary because this type is too large and does not have a type in the target theory. Therefore, we cannot use sym when checking coherence because it cannot handle enough great types. The same applies to most other combinators, which makes coherence unprovable.
The only solution I see is to add Type ω₂ to the metatheory and code for Type ω₁ to goal theory. Then the types Eq , Eq , refl and cong (I mean the usual cong f : eq xy -> eq (fx) (fy) - even for the "small" ( ω₁ ) Eq and Eq it should be in Type ω₂ , because f can be large) will lie in Type ω₂ , so we can, for example, say that Type ω₀ (but not higher) is equal to itself. And the types coerce and coherence will lie in Type ω₁ , so although we can say that Type ω₀ is equal to itself, this equation cannot be forced (this does not seem to be a big problem).
I assume that instead of adding Type ω₂ to the hierarchy, it’s easier to do this
Prop : Type 0 : Type 1 : ... (∀ α -> Type α) : Type ω₀ : Type ω₁ : Type ω₂ : Type ω₃ : ...
but before I split up, can you say if this sounds like a good plan? Am I chasing my tail with the latest extension of the Type ω₂ universe?
I will also repeat the questions from the first part here: How to prove that equal types lie in the same universe? Is this true (in a constructive sense)? Is it true that "Eq AB means that as soon as you find out that a and b are in the same universe, you will know that they have equal meanings"?