Mercurial > hg > Members > kono > Proof > category

comparison SetsCompleteness.agda @ 505:1f47d14533d0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 17 Mar 2017 10:43:32 +0900
parents b489f27317fb
children 817093714fd5
comparison
equal deleted inserted replaced
504:b489f27317fb 505:1f47d14533d0
52 } 52 }
53 53
54 open Functor 54 open Functor
55 open NTrans 55 open NTrans
56 56
57 record Slimit { c₂ } ( Γobj : {I A : Set c₂ } → I → A ) ( Γmap : {I A : Set c₂ } → ( (f : I → I ) → A → A )) : Set c₂ where 57 record Slimit { c₂ } ( ΓObj : Obj (Sets { c₂ }) → Obj (Sets { c₂ }) ) ( ΓMap : {A B : Obj Sets} → Hom Sets A B → Hom Sets (ΓObj A) ( ΓObj B ))
58 field 58 : Set c₂ where
59 s-u0 : {!!} 59 -- field
60 -- tlimit : Obj Sets
61 -- tmap : (A : Obj Sets) → Hom Sets ? (ΓObj A)
62 -- tcommute : {a b : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ ΓMap f o tmap a ] ≈ Sets [ tmap b o id1 Sets tlimit ] ]
60 63
61 open Slimit 64 open Slimit
62 65
63 SetsLimit : { c₂ : Level} 66 SetsLimit : { c₂ : Level}
64 ( ΓObj : {I A : Set c₂ } → I → A ) ( ΓMap : {I A : Set c₂ } → ( (f : I → I ) → A → A )) 67 ( ΓObj : Obj Sets → Obj Sets ) ( ΓMap : {A B : Obj Sets} → Hom Sets A B → Hom Sets (ΓObj A) ( ΓObj B ))
65 ( ΓObj' : Obj Sets → Obj Sets ) ( ΓMap' : {A B : Obj Sets} → Hom Sets A B → Hom Sets (ΓObj' A) ( ΓObj' B )) 68 ( Γ : IsFunctor (Sets { c₂}) (Sets { c₂}) ΓObj ΓMap )
66 ( Γ : IsFunctor (Sets { c₂}) (Sets { c₂}) ΓObj' ΓMap' ) 69 → Limit Sets Sets ( record { FObj = ΓObj ; FMap = ΓMap ; isFunctor = Γ } )
67 → Limit Sets Sets ( record { FObj = ΓObj' ; FMap = ΓMap' ; isFunctor = Γ } ) 70 SetsLimit { c₂} ΓObj ΓMap Γ = record {
68 SetsLimit { c₂} ΓObj ΓMap ΓObj' ΓMap' Γ = record { 71 a0 = Slimit ΓObj ΓMap
69 a0 = Slimit ΓObj ΓMap 72 ; t0 = record { TMap = tmap ; isNTrans = record { commute = tcommute } }
70 ; t0 = s-u0 {!!}
71 ; isLimit = record { 73 ; isLimit = record {
72 limit = {!!} 74 limit = {!!}
73 ; t0f=t = {!!} 75 ; t0f=t = {!!}
74 ; limit-uniqueness = {!!} 76 ; limit-uniqueness = {!!}
75 } 77 }
76 } 78 } where
79 tmap : (a : Obj Sets) → Hom Sets (Slimit ΓObj ΓMap) (ΓObj a)
80 tmap a _ = {!!}
81 tcommute : {a b : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ ΓMap f o tmap a ] ≈ Sets [ tmap b o id1 Sets (Slimit ΓObj ΓMap) ] ]
82 tcommute {a} {b} {f} = {!!}
77 83
78 84
85
86