Mercurial > hg > Members > kono > Proof > category
changeset 502:01a0dda67a8b
on going ..
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 16 Mar 2017 21:43:10 +0900 |
| parents | 61daa68a70c4 |
| children | bd33096c189b |
| files | freyd2.agda |
| diffstat | 1 files changed, 36 insertions(+), 33 deletions(-) [+] |
line wrap: on
line diff
--- a/freyd2.agda Thu Mar 16 10:26:30 2017 +0900 +++ b/freyd2.agda Thu Mar 16 21:43:10 2017 +0900 @@ -66,42 +66,45 @@ ∎ ) -HpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → (b : Obj A) - { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) - → LimitPreserve A I (Sets {c₂}) ( HomA A b ) -HpreseveLimit {_} { c₂} A b I = record { - preserve = λ Γ limita → record { - limit = λ a t → limitu a Γ t limita - ; t0f=t = λ { a t i } → t0f=tu {a} Γ t limita {i} - ; limit-uniqueness = λ { a t f } t=f → limit-uniquenessu {a} Γ limita t f t=f - } - } where - limitu : ( a : Obj Sets ) → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) → ( limita : Limit A I Γ ) → - Hom Sets a (FObj (HomA A b) (a0 limita)) - limitu = {!!} - t0f=tu : { a : Obj Sets } → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) → ( limita : Limit A I Γ ) → - ∀ { i : Obj I } → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) i o limitu a Γ t limita ] ≈ TMap t i ] - t0f=tu = {!!} - limit-uniquenessu : { a : Obj Sets } → (Γ : Functor I A ) - → ( limita : Limit A I Γ ) → - ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) → ( f : Hom Sets a (FObj (HomA A b) (a0 limita)) ) - → ( ∀ { i : Obj I } → (Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) i o f ] ≡ TMap t i ) ) - → Sets [ limitu a Γ t limita ≈ f ] - limit-uniquenessu = {!!} +-- {*}↓U has preinitial full subcategory iff U is representable + +record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (b : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where + field + -- FObj U x : A → Set + -- FMap U f = Set → Set + -- λ b → Hom (a,b) : A → Set + -- λ f → Hom (a,-) = λ b → Hom a b + + repr→ : NTrans A (Sets {c₂}) U (HomA A b ) + repr← : NTrans A (Sets {c₂}) (HomA A b) U + representable→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A b) x )] + representable← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)] + +-- HpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → (b : Obj A) +-- { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) +-- → LimitPreserve A I (Sets {c₂}) ( HomA A b ) +-- HpreseveLimit {_} { c₂} A b I = record { +-- preserve = λ Γ limita → record { +-- limit = λ a t → limitu a Γ t limita +-- ; t0f=t = λ { a t i } → t0f=tu {a} Γ t limita {i} +-- ; limit-uniqueness = λ { a t f } t=f → limit-uniquenessu {a} Γ limita t f t=f +-- } +-- } where +-- limitu : ( a : Obj Sets ) → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) → ( limita : Limit A I Γ ) → +-- Hom Sets a (FObj (HomA A b) (a0 limita)) +-- limitu = {!!} +-- t0f=tu : { a : Obj Sets } → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) → ( limita : Limit A I Γ ) → +-- ∀ { i : Obj I } → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) i o limitu a Γ t limita ] ≈ TMap t i ] +-- t0f=tu = {!!} +-- limit-uniquenessu : { a : Obj Sets } → (Γ : Functor I A ) +-- → ( limita : Limit A I Γ ) → +-- ( t : NTrans I Sets ( K Sets I a ) ((HomA A b) ○ Γ) ) → ( f : Hom Sets a (FObj (HomA A b) (a0 limita)) ) +-- → ( ∀ { i : Obj I } → (Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) i o f ] ≡ TMap t i ) ) +-- → Sets [ limitu a Γ t limita ≈ f ] +-- limit-uniquenessu = {!!} --- record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (b : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where --- field --- -- FObj U x : A → Set --- -- FMap U f = Set → Set --- -- λ b → Hom (a,b) : A → Set --- -- λ f → Hom (a,-) = λ b → Hom a b --- --- repr→ : NTrans A (Sets {c₂}) U (HomA A b ) --- repr← : NTrans A (Sets {c₂}) (HomA A b) U --- representable→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A b) x )] --- representable← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)] -- -- -- UpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → ( U : Functor A (Sets {c₂}) ) (b : Obj A)