Presheaves and Yoneda Lemma

src/Category/Coreflection.ard

@@ -68,7 +68,7 @@
   \func coreflection-map (x : comma-precat L B) : Hom {comma-precat L B} x to-comma
     | (x, s, d) => (Equiv.ret {isCoreflection} d, id {TrivialCat} s, rewrite id-left $ Equiv.f_ret {isCoreflection} d)
 
-  \func to-comma-terminal  : terminal-obj (comma-precat L B) => terminal-ind {comma-precat L B} to-comma
+  \func to-comma-terminal  : terminal-obj (comma-precat L B) => isTerminal {comma-precat L B} to-comma
       (\lam (p, s, q) => Contr.make (coreflection-map (p, s, q))
           (\lam a => exts (inv $ Equiv.adjoint $ a.3 *> id-left, cases a.2 \with {
             | Graph.empty p1 => idp

src/Category/Limit.ard

@@ -83,10 +83,13 @@
     | f_hinv => limUnique \lam j => inv o-assoc *> pmap (`∘ _) (L.limBeta L' j) *> L'.limBeta L j *> inv id-right
 
   \func transFuncMap {D : Precat} (L L' : Limit { | D => D }) (H : Functor L.J L'.J) (a : NatTrans (Comp L'.G H) L.G) : Hom L' L =>
-    limMap (\new Cone {
+    limMap cone
+  \where {
+    \func cone : Cone G L' => \new Cone {
       | coneMap j => a j ∘ L'.coneMap (H j)
       | coneCoh f => inv o-assoc *> pmap (`∘ _) (inv (a.natural f)) *> o-assoc *> pmap (_ ∘) (L'.coneCoh (H.Func f))
-    })
+    }
+  }
 }
 
 \meta Colimit G => Limit (Functor.op {G})
@@ -448,6 +451,24 @@
           (rewriteI o-assoc $ rewrite (p-beta1 P P', p-beta1 P' P) (inv id-right))
           (rewriteI o-assoc $ rewrite (p-beta2 P P', p-beta2 P' P) (inv id-right))
     }
+
+  \func pullback-of-mono {D : Precat} {x y z : D} {f : Mono {D} {x} {z}} {g : Hom y z} (P : Pullback f.f g) : Mono {D} {P.apex} {y} (Pullback.pbProj2 {P})
+    \cowith
+      | isMono {_} {q} {h} eq2 =>
+        \let s : g ∘ (P.pbProj2 ∘  q) = g ∘ (P.pbProj2 ∘ h) => pmap (g ∘ __) eq2
+        | f-s : f.f ∘ P.pbProj1 ∘ q = f.f ∘ P.pbProj1 ∘ h => rewrite (P.pbCoh, o-assoc, o-assoc) s
+        | eq1 : P.pbProj1 ∘ q = P.pbProj1 ∘ h => f.isMono $ rewriteI (o-assoc, o-assoc) f-s
+      \in
+        Pullback.pbEta eq1 eq2
+
+  \func pullback-of-mono' {D : Precat} {x y z : D} {f : Hom x z} {g : Mono {D} {y} {z}} (P : Pullback f g.f) : Mono {D} {P.apex} {x} (Pullback.pbProj1 {P})
+  \cowith
+    | isMono {_} {q} {h} eq2 =>
+      \let s : f ∘ (P.pbProj1 ∘  q) = f ∘ (P.pbProj1 ∘ h) => pmap (f ∘ __) eq2
+           | f-s : g.f ∘ P.pbProj2 ∘ q = g.f ∘ P.pbProj2 ∘ h => rewrite (inv P.pbCoh, o-assoc, o-assoc) s
+           | eq1 : P.pbProj2 ∘ q = P.pbProj2 ∘ h => g.isMono $ rewriteI (o-assoc, o-assoc) f-s
+      \in
+        Pullback.pbEta eq2 eq1
 }
 
 \func limits<=pr+eq {D : Precat}
@@ -498,10 +519,9 @@
 
 \func terminalMap' {C : Precat} {t : terminal-obj C} {x : C} : Hom x t => tupleMap (\case __)
 
-\func terminal-ind {C : Precat} (a : C) (e : \Pi (b : C) -> Contr (Hom b a))
-  : terminal-obj C
+\func isTerminal {C : Precat} (a : C) (e : \Pi (b : C) -> Contr (Hom b a))
+  : terminal-obj C a
   \cowith
-    | apex => a
     | proj j => absurd j
     | tupleMap {Z} _ => Contr.center {e Z}
     | tupleBeta {_} {_} {j} => absurd j
@@ -518,6 +538,11 @@
   \func terminalMap {x : Ob} : Hom x terminal => tupleMap (\case __)
 
   \lemma terminal-unique {x : Ob} {f g : Hom x terminal} : f = g => tupleEq (\case __)
+
+  \func global-section {c : Ob} (x : Hom terminal c) : SplitMono x
+    \cowith
+      | hinv => terminalMap
+      | hinv_f => terminal-unique
 }
 
 \class PrecatWithBprod \extends Precat {

src/Category/Slice.ard

@@ -22,4 +22,4 @@
   | Precat => SlicePrecat x
   | univalence => Cat.makeUnivalence \lam (e : Iso) =>
       \have e' => Functor.Func-iso {SlicePrecat.forget x} e
-      \in (ext (Cat.isotoid e', Cat.transport_Hom_iso-left e' _ (inv e.f.2)), simp_coe (Cat.transport_Hom_iso-right e' _ id-right))
+      \in (ext (Cat.isotoid e', Cat.transport_Hom_iso-left e' _ (inv e.f.2)), simp_coe (Cat.transport_Hom_iso-right e' _ id-right))

src/Category/SubobjectPoset.ard

@@ -0,0 +1,113 @@
+\import Category
+\import Category.Limit
+\import Category.Subobj
+\import Data.Or
+\import Function.Meta
+\import Logic
+\import Meta
+\import Order.Lattice
+\import Order.PartialOrder
+\import Paths
+\import Paths.Meta
+\import Relation.Equivalence
+
+\func SubobjectPoset {C : Precat} (c : C) => Preorder.PosetC {SubobjPreorder {C} c}
+
+\record widePullback {D : Precat} {J : \Set} {z : D} {objs : J -> D} (maps : \Pi (j : J) -> Hom (objs j) z) {
+  | wpbLim : LimitDiagram { | Diagram => diagram maps }
+}
+  \where {
+    \instance Shape (J : \Set) : Graph\cowith
+      | V => Or (\Sigma) J
+      | E => \case __, __ \with {
+        | inr i, inl _ => \Sigma
+        | _, _ => Empty
+      }
+
+    \func diagram {D : Precat} {J : \Set} {z : D} {objs : J -> D} (maps : \Pi (j : J) -> Hom (objs j) z)
+      : Diagram (Shape J) D
+    \cowith
+      | F x => \case x \with {
+        | inl _ => z
+        | inr i => objs i
+      }
+      | Func {a} {b} e => \case\elim a, \elim b, \elim e \with {
+        | inr i, inl _, e => maps i
+      }
+
+    \func widepullback-of-mono {D : Precat} {J : \Set} {z : D} {objs : J -> D}
+                               (monomaps : \Pi (j : J) -> Mono {D} {objs j} {z}) (wpb : widePullback {D} {J} {z} (\lam (j : J) => Mono.f {monomaps j})) : Mono (coneMap {wpb.wpbLim} (inl ())) =>
+      \new Mono {
+        | isMono {_} {g} {h} p => unfold at p $ limUnique (\lam j => unfold at j $ \case\elim j \with {
+          | inl () => p
+          | inr i =>
+            \let | eq : (Mono.f {monomaps i} ∘ coneMap {wpb.wpbLim} (inr i)) ∘ g = (Mono.f {monomaps i} ∘ coneMap {wpb.wpbLim} (inr i)) ∘ h => unfold $ rewrite (diagramCoh {wpb.wpbLim} {inr i} {inl ()} ()) p
+            \in
+              Mono.isMono {monomaps i} $ rewriteI (o-assoc, o-assoc) eq
+        })
+      }
+  }
+
+\open Pullback
+
+\instance SubobjectMeetsemilatice (C : PrecatWithPullbacks) (c : C) : Bounded.MeetSemilattice
+  | Poset => SubobjectPoset c
+  | meet => meet'
+  | meet-left {x} {y} => \case\elim x, \elim y \with {
+    | in~ sx, in~ sy => \case\elim sx, \elim sy \with {
+      | subobj _ mx, subobj _ my => inP (pbProj1, pbCoh)
+    }
+  }
+  | meet-right {x} {y} => \case\elim x, \elim y \with {
+    | in~ sx, in~ sy => \case\elim sx, \elim sy \with {
+      | subobj _ mx, subobj _ my => inP (pbProj2, idp)
+    }
+  }
+  | meet-univ {x} {y} {z} z<=x z<=y => \case\elim x, \elim y, \elim z, \elim z<=x, z<=y \with {
+    | in~ sx, in~ sy, in~ sz, z<=x', z<=y' => \case\elim sx, \elim sy, \elim sz, \elim z<=x', \elim z<=y' \with {
+      | subobj _ mx, subobj _ my, subobj _ mz, inP (f, eqf), inP (q, eqq)
+      => inP (pbMap f q (unfold $ rewrite (eqf, eqq) idp),
+              unfold $ unfold $ rewrite (o-assoc, pbBeta2 {pullback (Mono.f {mx}) (Mono.f {my})}) eqq)
+    }
+  }
+  | top => in~ (subobj _ idIso)
+  | top-univ {x} => \case\elim x \with {
+    | in~ a => \case\elim a \with {
+      | subobj sub m => inP (Mono.f {m}, rewrite id-left idp)
+    }
+  }
+  \where {
+    \func mono-from-pullback {a b d : C} (f : Mono {C} {a} {d}) (g : Mono {C} {b} {d})
+      : Mono {C} {pullback f.f g.f} {d} => Mono.comp g (pullback-of-mono (pullback f.f g.f))
+
+    \func subobj-product \alias\infix 7 xx {a b d : C} (f : Mono {C} {a} {d}) (g : Mono {C} {b} {d}) : Subobj d =>
+      subobj _ (mono-from-pullback f g)
+
+    \func product-comm {x y z : C} (f : Mono {C} {x} {z}) (g : Mono {C} {y} {z}) : f xx g <= g xx f =>
+      unfold (xx) $ inP (pbMap pbProj2 pbProj1 (inv pbCoh), rewrite (o-assoc, pbBeta2 {pullback g.f f.f}) pbCoh)
+
+    \func product-monotone {x y z w : C} (f : Mono {C} {x} {z}) (g : Mono {C} {y} {z})
+                           (h : Mono {C} {w} {z}) (f<=g : subobj _ f <= subobj _ g) : f xx h <= g xx h
+    \elim f<=g
+      | inP (q, eq) =>
+        \let pmap' : Hom (pullback f.f h.f) (pullback g.f h.f) => pbMap (q ∘ pbProj1) pbProj2
+            (unfold $ rewriteI o-assoc $ rewrite (eq, pbCoh {pullback f.f h.f}) idp) \in
+          inP (pmap', unfold $ unfold $ rewrite (o-assoc, pbBeta2 {pullback g.f h.f}) idp)
+
+    \func product-monotone' {x y z w : C} (f : Mono {C} {x} {z}) (g : Mono {C} {y} {z}) (h : Mono {C} {w} {z})
+                            (f<=g : subobj _ f <= subobj _ g) : h xx f <= h xx g =>
+      product-comm h f <=∘ {SubobjPreorder z} {h xx f} {f xx h} {h xx g}
+          (product-monotone f g h f<=g <=∘ {SubobjPreorder z} {f xx h} {g xx h} {h xx g} product-comm g h)
+
+    \func meet' (a b : SubobjectPoset c) : SubobjectPoset c
+    \elim a, b
+      | in~ (subobj _ m), in~ (subobj _ n) => in~ $ m xx n
+      | in~ (subobj _ m), ~-equiv (subobj _ mx) (subobj _ my) (r1, r2) i =>
+        ~-equiv (m xx mx) (m xx my) (product-monotone' mx my m r1, product-monotone' my mx m r2) i
+      | ~-equiv (subobj _ mx) (subobj _ my) (r1, r2) i, in~ (subobj _ m) =>
+        ~-equiv (mx xx m) (my xx m) (product-monotone mx my m r1, product-monotone my mx m r2) i
+  }
+
+ \instance SubobjectJoinSemilattice {C : Precat} (has-pushouts : PrecatWithPullbacks C.op) (c : C)
+ : JoinSemilattice (SubobjectPoset c)
+ => MeetSemilattice.op {SubobjectMeetsemilatice has-pushouts c}

src/Category/Topos.ard

@@ -1,16 +1,22 @@
 \import Algebra.Meta
 \import Category
+--\import Category.Adjoint
 \import Category.CartesianClosed
 \import Category.Coreflection
 \import Category.Limit
+--\import Category.Subobj
+--\import Category.SubobjectPoset
 \import Equiv
 \import Function (isInj)
 \import Function.Meta
 \import Logic
 \import Meta
+--\import Order.PartialOrder
 \import Paths
 \import Paths.Meta
+--\import Relation.Equivalence
 \import Set.Category
+--\import Topology.Locale
 \open PrecatWithBprod
 
 \class ToposPrecat \extends FinCompletePrecat, CartesianClosedPrecat {
@@ -53,6 +59,57 @@
   \func transpose-inj {A B : Ob} {f g : Hom (Bprod A B) omega} (e : p-transpose f = p-transpose g)
     : f = g => p-transpose-univ f *> pmap (belongs ∘ prodMap __ (id B)) e *> (inv $ p-transpose-univ g)
 
+--  \func subobject-equiv (C : Ob) : Equiv {SubobjectPoset C} {Hom C omega} => \new QEquiv {
+--    | f => from-subobj
+--    | ret m => in~ (from-char-map m)
+--    | ret_f sub =>
+--      \let equiv => ~-equiv {SubobjPreorder C} {Preorder.EquivRel.~} \in
+--      \case\elim sub \with {
+--      | in~ a => \case\elim a \with {
+--        | subobj sub m => equiv (from-char-map (from-subobj (in~ (subobj sub m)))) (subobj sub m)
+--            $ (inP (Iso.hinv {pb-of-char-iso m}, unfold $ unfold Pullback.unique.p-map $
+--                                                          \let s => pbBeta1 {char-pullback m} {sub} {Mono.f {m}} {terminalMap} \in
+--                                                          unfold at s $ {?}), {?}) -- this is the same as to say that pullbacks are equal
+--      }
+--  }
+--    | f_sec c => inv $ char-unique $ unfold {?}
+--  }
+--    \where {
+--      \func from-subobj (x : SubobjectPoset C) : Hom C omega
+--      \elim x
+--        | in~ a => \case\elim a \with {
+--          | subobj _ m => char-map m
+--        }
+--        | ~-equiv x y (r1, r2) => \case\elim x, \elim y, \elim r1, \elim r2 \with {
+--          | subobj a m1, subobj b m2, eq1, eq2 =>
+--            \let | (h1, eq1') => SubobjPreorder.extractMap {_} {C} m2 eq1
+--                 | (h2, eq2') => SubobjPreorder.extractMap {_} {C} m1 eq2
+--                 | iso => SubobjPreorder.antisymmetric m2 m1 (inP $ (h2, eq2')) (inP $ (h1, eq1'))
+--                 | iso-mono => Iso.isMono {iso}
+--            \in
+--              char-unique (\new Pullback {
+--                | pbCoh => rewriteI (eq2', o-assoc) $ rewrite (pbCoh {char-pullback m1}, o-assoc, terminate) idp
+--                | pbMap {w} p1 n coh => h1 ∘ pbMap {char-pullback m1} {w} p1 n coh
+--                | pbBeta1 => rewriteI o-assoc $ rewrite (eq1', pbBeta1 {char-pullback m1}) idp
+--                | pbBeta2 => terminal-unique
+--                | pbEta {w} {g} {h} coh _ =>
+--                  \let | c => pbEta {char-pullback m1} {w} {h2 ∘ g} {h2 ∘ h} (rewrite (inv o-assoc, eq2', inv o-assoc, eq2') coh) terminal-unique
+--                  \in
+--                    iso-mono {w} {g} {h} c
+--              })
+--        }
+
+--      \func pb-of-char-iso {B C : Ob} (m : Mono {\this} {B} {C})
+--        => Pullback.unique (char-map m) true-map (char-pullback m) (pullback (char-map m) true-map)
+--
+--      \func from-char-map (m : Hom C omega) : SubobjPreorder C =>
+--        \let
+--          | true-mono => global-section true-map
+--          | pb-of-mono => Pullback.pullback-of-mono' {_} {_} {_} {_} {_} {true-mono} (pullback m true-map)
+--        \in
+--          subobj (Pullback.apex {pullback m true-map}) pb-of-mono
+--    }
+
   \func internal-equality \alias eq (B : Ob) : Hom (Bprod B B) omega =>
     char-map (diagonal.isSplitMono B)
 
@@ -181,7 +238,7 @@
 
   {-
   The idea: a relation S between B and C is functional iff all elements of B have a single image under S.
-  'all-with-single-img' returns the subset consisinf of elements of B with singleton images.
+  'all-with-single-img' returns the subset consising of elements of B with singleton images.
   -}
 
   \func all-with-single-img {B C : Ob} : Hom (P $ Bprod B C) (P B) => p-transpose is-image-single
@@ -374,4 +431,16 @@
                          {eq : (\lam x => IsElement m (p1 x)) = (\lam _ => \Sigma)} (x : w) : IsElement m (p1 x) =>
       \let s : IsElement m (p1 x) = (\Sigma) => path (\lam i => (eq @ i) x) \in
         sigma-prop-ext-inv s
-  }
+  }
+
+
+--\instance SubobjectLocale-Topos {C : BicompleteCat} {C-topos : ToposPrecat C} (obj : C) : Locale
+--  | Poset => SubobjectPoset obj
+--  | Join {J} G => {?}
+--  | Join-cond => {?}
+--  | Join-univ => {?}
+--  | Join-ldistr>= => {?}
+--  \where {
+--    \func map-to-homs {J : \Set} (G : J -> SubobjectPoset obj) : \Pi (j : J) -> Hom {C-topos} obj omega
+--      => \lam j => ToposPrecat.subobject-equiv obj (G j)
+--  }