From 657ad3327ff7f199aedb308337df8745060ad7d6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 May 2015 21:35:59 -0700 Subject: [PATCH] chore(hott): remove unnecessary '[trans]' attributes --- hott/init/equiv.hlean | 2 -- hott/init/logic.hlean | 3 --- 2 files changed, 5 deletions(-) diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index bb428f74e..6ed67a359 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -273,7 +273,5 @@ namespace equiv attribute equiv.trans [trans] attribute equiv.refl [refl] attribute equiv.symm [symm] - attribute equiv_of_equiv_of_eq [trans] - attribute equiv_of_eq_of_equiv [trans] end equiv diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean index 984b503ff..f04050a50 100644 --- a/hott/init/logic.hlean +++ b/hott/init/logic.hlean @@ -125,9 +125,6 @@ section assume H₁ H₂, H₂ ▸ H₁ end -attribute ne.of_eq_of_ne [trans] -attribute ne.of_ne_of_eq [trans] - /- iff -/ definition iff (a b : Type) := prod (a → b) (b → a)