var i₁ , q₁ ≅e var i₂ , q₂ = top

Author: effectfully

Core.agda

@@ -206,7 +206,7 @@ var i₁    , x₁      ≅s var i₂    , x₂      = x₁ ≅ x₂
 (D₁ ⊛ E₁) , s₁ , t₁ ≅s (D₂ ⊛ E₂) , s₂ , t₂ = D₁ , s₁ ≅s D₂ , s₂ & E₁ , t₁ ≅s E₂ , t₂
 _                   ≅s _                   = bot
 
-var i₁    , q₁      ≅e var i₂    , q₂      = i₁ ≅ i₂
+var i₁    , q₁      ≅e var i₂    , q₂      = top
 π A₁ D₁   , x₁ , e₁ ≅e π A₂ D₂   , x₂ , e₂ = x₁ ≅ x₂ & D₁ x₁ , e₁ ≅e D₂ x₂ , e₂
 (D₁ ⊛ E₁) , s₁ , e₁ ≅e (D₂ ⊛ E₂) , s₂ , e₂ = D₁ , s₁ ≅s D₂ , s₂ & E₁ , e₁ ≅e E₂ , e₂
 _                   ≅e _                   = bot

Property/Eq.agda

@@ -7,7 +7,6 @@ open import OTT.Function.Pi
 
 infix 4 _≟_
 
--- TODO?
 module _ where
   open import Relation.Binary.PropositionalEquality.TrustMe