From 3523a70b4c8bd414991fdfcc5c763adb96ed045b Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 21 Nov 2014 23:11:57 -0500 Subject: [PATCH] fix(hott/path): make recursion-like definitions reducible --- library/hott/path.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/hott/path.lean b/library/hott/path.lean index e7186b0f3..33abbaaf0 100644 --- a/library/hott/path.lean +++ b/library/hott/path.lean @@ -24,11 +24,11 @@ notation x ≈ y `:>`:50 A:49 := @path A x y definition idp {A : Type} {a : A} := idpath a -- unbased path induction -definition rec' {A : Type} {P : Π (a b : A), (a ≈ b) -> Type} +definition rec' [reducible] {A : Type} {P : Π (a b : A), (a ≈ b) -> Type} (H : Π (a : A), P a a idp) {a b : A} (p : a ≈ b) : P a b p := path.rec (H a) p -definition rec_on' {A : Type} {P : Π (a b : A), (a ≈ b) -> Type} {a b : A} (p : a ≈ b) +definition rec_on' [reducible] {A : Type} {P : Π (a b : A), (a ≈ b) -> Type} {a b : A} (p : a ≈ b) (H : Π (a : A), P a a idp) : P a b p := path.rec (H a) p @@ -182,7 +182,7 @@ rec_on p (take q h, h ⬝ (concat_1p _)) q -- Transport -- --------- -definition transport {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) : P y := +definition transport [reducible] {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) : P y := path.rec_on p u -- This idiom makes the operation right associative.