From f2dfca25f9629725bf1a3b7b33e9e965e5cb8ec6 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 20 Sep 2018 16:03:32 +0200
Subject: [PATCH] refactor: use notation for trunc_index

---
 hott/types/fiber.hlean | 6 +++---
 hott/types/pi.hlean    | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean
index 84a500a0f..f8936d03e 100644
--- a/hott/types/fiber.hlean
+++ b/hott/types/fiber.hlean
@@ -130,7 +130,7 @@ namespace fiber
   end
 
   definition is_trunc_fiber (n : ℕ₋₂) {A B : Type} (f : A → B) (b : B)
-    [is_trunc n A] [is_trunc (n.+1) B] : is_trunc n (fiber f b) :=
+    (HA : is_trunc n A) (HB : is_trunc (n.+1) B) : is_trunc n (fiber f b) :=
   is_trunc_equiv_closed_rev n !fiber.sigma_char _
 
   definition is_contr_fiber_id (A : Type) (a : A) : is_contr (fiber (@id A) a) :=
@@ -404,8 +404,8 @@ namespace fiber
   end
 
   definition is_trunc_pfiber (n : ℕ₋₂) {A B : Type*} (f : A →* B)
-    [is_trunc n A] [is_trunc (n.+1) B] : is_trunc n (pfiber f) :=
-  is_trunc_fiber n f pt
+    (HA : is_trunc n A) (HB : is_trunc (n.+1) B) : is_trunc n (pfiber f) :=
+  is_trunc_fiber n f pt HA HB
 
   definition pfiber_pequiv_of_is_contr [constructor] {A B : Type*} (f : A →* B) (H : is_contr B) :
     pfiber f ≃* A :=
diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean
index 2211711b5..32dec003e 100644
--- a/hott/types/pi.hlean
+++ b/hott/types/pi.hlean
@@ -274,7 +274,7 @@ namespace pi
 
   /- Truncatedness: any dependent product of n-types is an n-type -/
 
-  theorem is_trunc_pi (B : A → Type) (n : trunc_index)
+  theorem is_trunc_pi (B : A → Type) (n : ℕ₋₂)
       [H : ∀a, is_trunc n (B a)] : is_trunc n (Πa, B a) :=
   begin
     revert B H,
@@ -291,11 +291,11 @@ namespace pi
       is_trunc_eq n (f a) (g a) }
   end
   local attribute is_trunc_pi [instance]
-  theorem is_trunc_pi_eq (n : trunc_index) (f g : Πa, B a)
+  theorem is_trunc_pi_eq (n : ℕ₋₂) (f g : Πa, B a)
       [H : ∀a, is_trunc n (f a = g a)] : is_trunc n (f = g) :=
   is_trunc_equiv_closed_rev n !eq_equiv_homotopy _
 
-  theorem is_trunc_not [instance] (n : trunc_index) (A : Type) : is_trunc (n.+1) ¬A :=
+  theorem is_trunc_not [instance] (n : ℕ₋₂) (A : Type) : is_trunc (n.+1) ¬A :=
   by unfold not;exact _
 
   theorem is_prop_pi_eq [instance] [priority 490] (a : A) : is_prop (Π(a' : A), a = a') :=