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

style(library): rename set_category to discrete_category

Browse source
This commit is contained in:
Floris van Doorn 2014-11-06 22:18:11 -05:00 committed by Leonardo de Moura
parent 930cc11684
commit 8c7fdd3708
3 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/algebra/category/constructions.lean
View file

@ -70,20 +70,20 @@ namespace category
(λh f, empty.rec _ f) f) (λh f, empty.rec _ f) f)
(λh (g : empty), empty.rec _ g) g (λh (g : empty), empty.rec _ g) g
omit H omit H
definition set_category (A : Type) [H : decidable_eq A] : category A := definition discrete_category (A : Type) [H : decidable_eq A] : category A :=
mk (λa b, set_hom a b) mk (λa b, set_hom a b)
(λ a b c g f, set_compose g f) (λ a b c g f, set_compose g f)
(λ a, decidable.rec_on_true rfl ⋆) (λ a, decidable.rec_on_true rfl ⋆)
(λ a b c d h g f, @subsingleton.elim (set_hom a d) _ _ _) (λ a b c d h g f, @subsingleton.elim (set_hom a d) _ _ _)
(λ a b f, @subsingleton.elim (set_hom a b) _ _ _) (λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
(λ a b f, @subsingleton.elim (set_hom a b) _ _ _) (λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
definition Set_category (A : Type) [H : decidable_eq A] := Mk (set_category A) definition Discrete_category (A : Type) [H : decidable_eq A] := Mk (discrete_category A)
end end
section section
open unit bool open unit bool
definition category_one := set_category unit definition category_one := discrete_category unit
definition Category_one := Mk category_one definition Category_one := Mk category_one
definition category_two := set_category bool definition category_two := discrete_category bool
definition Category_two := Mk category_two definition Category_two := Mk category_two
end end

2
library/algebra/category/default.lean
View file

@ -2,4 +2,4 @@
-- Released under Apache 2.0 license as described in the file LICENSE. -- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Floris van Doorn -- Author: Floris van Doorn
import .basic .morphism .functor .constructions import .morphism .constructions

2
library/logic/eq.lean
View file

@ -90,7 +90,7 @@ namespace eq
drec_on H rfl drec_on H rfl
theorem rec_on_constant2 (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : rec_on H₁ b = rec_on H₂ b := theorem rec_on_constant2 (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : rec_on H₁ b = rec_on H₂ b :=
rec_on_constant H₁ b ⬝ (rec_on_constant H₂ b)⁻¹ rec_on_constant H₁ b ⬝ rec_on_constant H₂ b⁻¹
theorem rec_on_irrel_arg {f : A → B} {D : B → Type} (H : a = a') (H' : f a = f a') (b : D (f a)) : theorem rec_on_irrel_arg {f : A → B} {D : B → Type} (H : a = a') (H' : f a = f a') (b : D (f a)) :
rec_on H b = rec_on H' b := rec_on H b = rec_on H' b :=