comments in infer for coercions

lib/Quox/Typechecker.idr

@@ -479,23 +479,34 @@ mutual
     pure $ InfRes {type = dsub1 ty dim, qout}
 
   infer' ctx sg (Coe ty p q val loc) = do
+    -- if Ψ, 𝑖 | Γ ⊢₀ A ⇐ Type _
     checkType (extendDim ty.name ctx) ty.term Nothing
+    -- if Ψ | Γ ⊢ σ · s ⇐ A‹p/𝑖› ⊳ Σ
     qout <- checkC ctx sg val $ dsub1 ty p
+    -- then Ψ | Γ ⊢ σ · coe (𝑖 ⇒ A) @p @q s ⇒ A‹q/𝑖› ⊳ Σ
     pure $ InfRes {type = dsub1 ty q, qout}
 
   infer' ctx sg (Comp ty p q val r (S [< j0] val0) (S [< j1] val1) loc) = do
+    -- if Ψ | Γ ⊢₀ A ⇐ Type _
     checkType ctx ty Nothing
+    -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
     qout <- checkC ctx sg val ty
+    -- if Ψ, 𝑗, 𝑖=0      | Γ ⊢ σ · t₀ ⇐ A ⊳ Σ₀
+    --    Ψ, 𝑗, 𝑖=0, 𝑗=p | Γ ⊢ t₀ = s ⇐ A
     let ty'  = dweakT 1 ty; val' = dweakT 1 val; p' = weakD 1 p
         ctx0 = extendDim j0 $ eqDim r (K Zero j0.loc) ctx
         val0 = getTerm val0
     qout0 <- check ctx0 sg val0 ty'
     lift $ equal loc (eqDim (B VZ p.loc) p' ctx0) sg ty' val0 val'
+    -- if Ψ, 𝑗, 𝑖=1      | Γ ⊢ σ · t₁ ⇐ A ⊳ Σ₁
+    --    Ψ, 𝑗, 𝑖=1, 𝑗=p | Γ ⊢ t₁ = s ⇐ A
     let ctx1 = extendDim j1 $ eqDim r (K One j1.loc) ctx
         val1  = getTerm val1
     qout1 <- check ctx1 sg val1 ty'
+    -- if Σ = Σ₀ = Σ₁
     lift $ equal loc (eqDim (B VZ p.loc) p' ctx1) sg ty' val1 val'
     let qouts  = qout :: catMaybes [toMaybe qout0, toMaybe qout1]
+    -- then Ψ | Γ ⊢ comp A @p @q s @r {0 𝑗 ⇒ t₀; 1 𝑗 ⇒ t₁} ⇒ A ⊳ Σ
     pure $ InfRes {type = ty, qout = lubs ctx qouts}
 
   infer' ctx sg (TypeCase ty ret arms def loc) = do