From e00ccff6deebfb40e8fdc64a238afef3c96c60a0 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 2 Nov 2015 12:28:22 -0500 Subject: [PATCH] fix(hott): make sure the HoTT library compiles with --to_axiom --- hott/algebra/category/functor/examples.hlean | 4 ++-- hott/init/trunc.hlean | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/hott/algebra/category/functor/examples.hlean b/hott/algebra/category/functor/examples.hlean index 7e4848adaa..8824e06116 100644 --- a/hott/algebra/category/functor/examples.hlean +++ b/hott/algebra/category/functor/examples.hlean @@ -110,7 +110,7 @@ namespace functor (functor_uncurry_id G) (functor_uncurry_comp G) - theorem functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F := + definition functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F := functor_eq (λp, ap (to_fun_ob F) !prod.eta) begin intro cd cd' fg, @@ -134,7 +134,7 @@ namespace functor rewrite [▸*, ↑functor_uncurry_hom, respect_id, ▸*, id_right]} end - theorem functor_curry_functor_uncurry : functor_curry (functor_uncurry G) = G := + definition functor_curry_functor_uncurry : functor_curry (functor_uncurry G) = G := begin fapply functor_eq, exact (functor_curry_functor_uncurry_ob G), intro c c' f, diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 4baeb3a973..84637b4d23 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -154,15 +154,15 @@ namespace is_trunc (λn IH Hn, is_trunc_of_imp_is_trunc) Hn H - -- the following cannot be instances in their current form, because they are looping - theorem is_trunc_of_is_contr (A : Type) (n : trunc_index) [H : is_contr A] : is_trunc n A := + -- these must be definitions, because we need them to compute sometimes + definition is_trunc_of_is_contr (A : Type) (n : trunc_index) [H : is_contr A] : is_trunc n A := trunc_index.rec_on n H _ - theorem is_trunc_succ_of_is_hprop (A : Type) (n : trunc_index) [H : is_hprop A] + definition is_trunc_succ_of_is_hprop (A : Type) (n : trunc_index) [H : is_hprop A] : is_trunc (n.+1) A := is_trunc_of_leq A (show -1 ≤ n.+1, from star) - theorem is_trunc_succ_succ_of_is_hset (A : Type) (n : trunc_index) [H : is_hset A] + definition is_trunc_succ_succ_of_is_hset (A : Type) (n : trunc_index) [H : is_hset A] : is_trunc (n.+2) A := is_trunc_of_leq A (show 0 ≤ n.+2, from star)