{-# OPTIONS --allow-unsolved-metas #-} -- {-# OPTIONS --cubical-compatible --safe #-} open import CCC open import Level open import Category open import Definitions open import HomReasoning module ToposSub {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A c ) (n : ToposNat A (CCC.1 c)) where open Topos open Equalizer open ≈-Reasoning A open CCC.CCC c open Functor open import Category.Sets hiding (_o_) open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym) -- ○ b -- b -----------→ 1 -- | | -- m | | ⊤ -- ↓ char m ↓ -- a -----------→ Ω record SubObject (a : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ) where field sb : Obj A sm : Hom A sb a smono : Mono A sm postulate I : Set c₁ small : Small A I open import yoneda A I small module SubObjectFunctor (S : (a : Set (c₁ ⊔ c₂ ⊔ ℓ)) → Set c₂) (solv← : {x : Obj A} → S (SubObject x) → SubObject x) (solv→ : {x : Obj A} → SubObject x → S (SubObject x)) (soiso← : {a : Obj A} → (x : SubObject a) → solv← (solv→ x) ≡ x) (soiso→ : {a : Obj A} → (x : S (SubObject a) ) → solv→ (solv← x) ≡ x) (≡←≈ : {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y) where open SubObject Smap : {x y : Obj A} → Hom A y x → Hom Sets (S (SubObject x)) (S (SubObject y)) Smap {x} {y} h s = solv→ record { sb = y ; sm = id1 A y ; smono = record { isMono = λ f g eq → sm1 f g eq } } where sm1 : {a : Obj A } → ( f g : Hom A a y ) → A [ A [ id1 A y o f ] ≈ A [ id1 A y o g ] ] → A [ f ≈ g ] sm1 f g eq = begin f ≈↑⟨ idL ⟩ id1 A y o f ≈⟨ eq ⟩ id1 A y o g ≈⟨ idL ⟩ g ∎ SubObjectFuntor : Functor (Category.op A) (Sets {c₂}) SubObjectFuntor = record { FObj = λ x → S (SubObject x) ; FMap = Smap ; isFunctor = record { identity = {!!} ; distr = {!!} ; ≈-cong = {!!} } } open NTrans sub→topos : (Ω : Obj A) → Representable A ≡←≈ SubObjectFuntor Ω → Topos A c sub→topos Ω R = record { Ω = Ω ; ⊤ = TMap (Representable.repr→ R) 1 (solv→ record { sb = {!!} ; sm = {!!} ; smono = {!!} }) ; Ker = λ {a} h → record { equalizer-c = sb {!!} ; equalizer = sm {!!} ; isEqualizer = {!!} } ; char = λ m mono → {!!} ; isTopos = record { char-uniqueness = {!!} ; ker-m = {!!} } } topos→rep : (t : Topos A c ) → Representable A ≡←≈ SubObjectFuntor (Topos.Ω t) topos→rep t = record { repr→ = record { TMap = λ a Sa → Topos.char t (sm (solv← Sa)) (smono (solv← Sa)) ; isNTrans = record { commute = {!!} } } -- Hom A a Ω ; repr← = record { TMap = λ a h → solv→ record {sb = equalizer-c (Ker t h) ; sm = equalizer (Ker t h) ; smono = {!!} } ; isNTrans = {!!} } -- FObj (Sub S) a ; reprId→ = {!!} ; reprId← = {!!} }