fix: Model.Natural

Author: Vtec234

HoTTLean/Model/Natural/Interpretation.lean

@@ -832,7 +832,7 @@ theorem tp_sound {Γ i A l} (H : Lookup Γ i A l) {sΓ} (hΓ : sΓ ∈ I.ofCtx 
   | zero => exact I.mem_ofType_wk _ hB
   | succ _ _ _ ih =>
     have ⟨_, _, _, _⟩ := ih hΓ'
-    exact ⟨‹_›, _, ⟨_, ‹_›, rfl⟩, I.mem_ofType_wk _ ‹_›⟩
+    exact ⟨‹_›, _, ‹_›, I.mem_ofType_wk _ ‹_›⟩
 
 theorem var_sound {Γ i A l} (H : Lookup Γ i A l) {sΓ} (hΓ : sΓ ∈ I.ofCtx Γ) :
     ∃ llen, ∃ st ∈ sΓ.var llen i, st ≫ s[l].tp ∈ I.ofType sΓ l A llen := by

HoTTLean/Model/Natural/NaturalModel.lean

@@ -482,6 +482,7 @@ theorem comp_mk
       (by simp [e2]; rw [← Functor.map_comp_assoc, comp_sec]; simp; congr!) := by
   apply ext (A := σA) (by simp [← comp_fst, e1, e3]) <;> simp [← comp_fst, ← comp_snd]
   rw [← comp_dependent, dependent_mk]
+  . simp [e1]
 
 theorem eta (ab : y(Γ) ⟶ M.uvPolyTp.compDom N.uvPolyTp)
     {A} (eq : fst ab ≫ M.tp = A) :
@@ -1176,7 +1177,8 @@ lemma reflSubst_j : ym(ii.reflSubst a) ≫ j i a C r r_tp = r := by
     · simp
   simp only [← heq_eq_eq, comp_eqToHom_heq_iff]
   rw! [equivFst_lift_eq]
-  simp [this]
+  . simp [this]
+  . simp [IsPullback.of_id_fst]
 
 variable (b : y(Γ) ⟶ M.Tm) (b_tp : b ≫ M.tp = a ≫ M.tp)
   (h : y(Γ) ⟶ M.Tm) (h_tp : h ≫ M.tp = ii.isKernelPair.lift b a (by aesop) ≫ ii.Id)