Mercurial > hg > Members > kono > Proof > category

comparison SetsCompleteness.agda @ 781:340708e8d54f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix for 2.5.4.2
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 08 Mar 2019 17:46:59 +0900
parents 984518c56e96
children
comparison
equal deleted inserted replaced
780:b44c1c6ce646 781:340708e8d54f
10 import Relation.Binary.PropositionalEquality 10 import Relation.Binary.PropositionalEquality
11 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → ( λ x → f x ≡ λ x → g x ) 11 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → ( λ x → f x ≡ λ x → g x )
12 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ 12 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
13 13
14 ≡cong = Relation.Binary.PropositionalEquality.cong 14 ≡cong = Relation.Binary.PropositionalEquality.cong
15
16 open import Relation.Binary.PropositionalEquality hiding ( [_] )
15 17
16 lemma1 : { c₂ : Level } {a b : Obj (Sets { c₂})} {f g : Hom Sets a b} → 18 lemma1 : { c₂ : Level } {a b : Obj (Sets { c₂})} {f g : Hom Sets a b} →
17 Sets [ f ≈ g ] → (x : a ) → f x ≡ g x 19 Sets [ f ≈ g ] → (x : a ) → f x ≡ g x
18 lemma1 refl x = refl 20 lemma1 refl x = refl
19 21