michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/hott/fibrant): set arguments for type class resolution

Browse source
This commit is contained in:
Jeremy Avigad 2014-11-04 12:37:20 -05:00 committed by Leonardo de Moura
parent 92b0a538c5
commit 05ec76185d
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/hott/fibrant.lean
View file

@ -15,11 +15,11 @@ namespace fibrant
axiom unit_fibrant : fibrant unit
axiom nat_fibrant : fibrant nat
axiom bool_fibrant : fibrant bool
axiom sum_fibrant {A B : Type} (C1 : fibrant A) (C2 : fibrant B) : fibrant (A ⊎ B)
axiom prod_fibrant {A B : Type} (C1 : fibrant A) (C2 : fibrant B) : fibrant (A × B)
axiom sigma_fibrant {A : Type} {B : A → Type} (C1 : fibrant A) (C2 : Πx : A, fibrant (B x)) :
axiom sum_fibrant {A B : Type} [C1 : fibrant A] [C2 : fibrant B] : fibrant (A ⊎ B)
axiom prod_fibrant {A B : Type} [C1 : fibrant A] [C2 : fibrant B] : fibrant (A × B)
axiom sigma_fibrant {A : Type} {B : A → Type} [C1 : fibrant A] [C2 : Πx : A, fibrant (B x)] :
fibrant (Σx : A, B x)
axiom pi_fibrant {A : Type} {B : A → Type} (C1 : fibrant A) (C2 : Πx : A, fibrant (B x)) :
axiom pi_fibrant {A : Type} {B : A → Type} [C1 : fibrant A] [C2 : Πx : A, fibrant (B x)] :
fibrant (Πx : A, B x)
instance [persistent] unit_fibrant