Mercurial > hg > Members > kono > Proof > category
changeset 667:60e881060534
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 27 Oct 2017 10:01:35 +0900 |
| parents | ba84fbc64c7d |
| children | 07c84c8d9e4f |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 3 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Mon Oct 23 15:21:20 2017 +0900 +++ b/SetsCompleteness.agda Fri Oct 27 10:01:35 2017 +0900 @@ -267,12 +267,11 @@ eq3' : (x : a ) (i j : Obj C) (k : I) → ( ΓMap s Γ k (TMap t i x) ≡ TMap t j x ) ≡ ( ΓMap s Γ k (snmap (f x) i) ≡ snmap (f x) j ) eq3' x i j k = ≡cong ( λ h → ( ΓMap s Γ k (h i) ≡ h j )) ( extensionality Sets ( λ i → eq1 x i ) ) - irr≅ : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≅ eq' - irr≅ refl refl = refl + irr≅ : { c₂ : Level} {d e : Set c₂ } { x : d } { y : e } ( ee : d ≡ e ) ( eq eq' : x ≅ y ) → eq ≅ eq' + irr≅ refl refl refl = refl eq4 : ( x : a) ( i j : Obj C ) ( g : I ) - → TMap t i x ≡ snmap (f x) i → ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g } ) ≅ sncommute (f x) i j g - eq4 x i j g eq = {!!} -- irr≅ ? ? + eq4 x i j g = ? -- irr≅ ? ? ? postulate eq6 : {a : Level } {A : Set a} {B : A → Set a} {f g : (y : A) → B y} → (∀ y → f y ≡ g y) → ( ( λ y → f y ) ≅ ( λ y → g y )) -- eq5 : ( x : a) → sncommute (limit1 a t x) ≅ sncommute (f x) eq5 : ( x : a) → ( ( λ i → TMap t i x ) ≡ snmap (f x) )