From 107550238bcb03dfc84aae3c116fb776c5cc7d67 Mon Sep 17 00:00:00 2001 From: seulbaek Date: Tue, 19 Jan 2016 16:02:17 -0800 Subject: [PATCH] refactor(hott/choice): rename lemmas for 3.8.2 --- hott/choice.hlean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/hott/choice.hlean b/hott/choice.hlean index 92920b3e35..d1c3b96451 100644 --- a/hott/choice.hlean +++ b/hott/choice.hlean @@ -28,13 +28,13 @@ section (to_inv !sigma_pi_equiv_pi_sigma) (H X A P HX HA HP HI)) -- AC_cart can be derived from AC' by setting P := λ _ _ , unit. - definition AC'_to_AC_cart : AC'.{u} -> AC_cart.{u} := + definition AC_cart_of_AC' : AC'.{u} -> AC_cart.{u} := λ H X A HX HA HI, trunc_functor _ (λ H0 x, (H0 x).1) (H X A (λ x a, lift.{0 u} unit) HX HA (λ x a, !is_trunc_lift) (λ x, trunc_functor _ (λ a, ⟨a, lift.up.{0 u} unit.star⟩) (HI x))) -- And the converse, by setting A := λ x, Σ a, P x a. - definition AC_cart_to_AC' : AC_cart.{u} -> AC'.{u} := + definition AC'_of_AC_cart : AC_cart.{u} -> AC'.{u} := by intro H X A P HX HA HP HI; apply H X (λ x, Σ a, P x a) HX (λ x, !is_trunc_sigma) HI