juan_gandhi | Entries tagged with topos

Given a topos ℰ and an internal functor f: C → D in ℰ between two internal categories, we have three adjoint functors, Σ_f⊣f*⊣Π_f.

These two functors, Σ_f and Π_f, can be viewed as giving left and right Kan extensions for diagrams (copresheaves) of ℰ^C along f.

Meaning, for a copresheaf X: C → ℰ,

Σ_f(X) = Lan_f(X)

Π_f(X) = Ran_f(X)

(I mean, I'm still stuffing Kan extensions into my brain, and this picture is what makes the picture clearer)

P.S. Ха! Оказалось, что это теорема, и доказывается через Йонеду.

Theorem 2.6. If the Kan extensions exist for all F, then Lan_K− and Ran_K− are
respectively the left and right adjoints to the functor − ○ K which is precomposition with K.

https://github.com/vpatryshev/wowiki/wiki/Logic-of-Elementary-Topos

https://www.meetup.com/SF-Types-Theorems-and-Programming-Languages/events/270634414/

Copresheaf. Just a diagram, or a presheaf over op-category. Also, a notation I could not recognize at first: Set^→. Just Set^𝟚.

Закончил свою логику. (Ну там тесты еще всю ночь побегут, но это фигня, мираж.)

def checkDistributivity(cat: Category): MatchResult[Any] = {

  val topos = new CategoryOfDiagrams(cat)
  import topos._
  val points = Ω.points

  val desc = s"Testing ${cat.name} distributivity laws"
  println(desc)
  
  for { pt1 ← points } {
    println(s"  at ${pt1.tag}")
    val p = predicateFor(pt1)

    for { pt2 ← points } {
      val q = predicateFor(pt2)
      val pAndQ = p ∧ q
      val pOrQ = p ∨ q

      for { pt3 ← points } {
        val r = predicateFor(pt3)
        // distributivity of conjunction over disjunction
        (p ∧ (q ∨ r)) === (pAndQ ∨ (p ∧ r))
        // distributivity of disjunction over conjunction
        (p ∨ (q ∧ r)) === (pOrQ ∧ (p ∨ r))
      }
    }
  }

  ok
}

for { p <- Ω.points } {
  val pp = predicateFor(p)
  (True ∧ pp) === pp
  (False ∧ pp) === False

  // idempotence
  (pp ∧ pp) === pp

  for { q <- Ω.points } {
    val pq = predicateFor(q)
    val ppq = pp ∧ pq
    
    // commutativity
    (pp ∧ pq) === (pq ∧ pp)
    
    for { r <- Ω.points } {
      val pr = predicateFor(r)
      // associativity
      (ppq ∧ pr) === (pp ∧ (pq ∧ pr))
    }
  }
}

Woke up at 4:20, went to fix my topos logic code. Done by 5:59. Happiness!

Reminds me what we did in Forth, with Leo, present here:

      applyTo | "a" | "b"  | "c" | "d"  | "e" |
      at("a") | "a" | "ab" | ""  | ""   | ""  |
      at("b") | ""  | "b"  | ""  | ""   | ""  |
      at("c") | ""  | "cb" | "c" | "cd" | ""  |
      at("d") | ""  | ""   | ""  | "d"  | ""  |
      at("e") | ""  | ""   | ""  | "ed" | "e"

This is a test case. Rather, 25 test cases.
We scan through at("a") to at("e"), where at(x) is a representable diagram (presheaf, functor, whatever) for object x:

      val at = (obj: topos.site.Obj) => topos.representable(obj)

and then, in each row, apply this representable to objects "a",..., "e", and check that the result is a set (hom(x, y)) consisting of the values in the cells of the table. The values in the table are split by comma and converted to sets - because we deal with Grothendieck toposes.

But toposes are not essential here. I just decided to be lazy, and write code as tables, as Leo suggested eons ago, probably in 1989. It's not even my idea.

Implementation:

      val at = (obj: topos.site.Obj) => topos.representable(obj)
      
      case class table(data: List[String] = Nil) {
        def |(x: String): table = table(x::data)
        def |(d: Diagrams.Diagram) = check(d, data, data)
      }

      case class check(d: Diagram, data: List[String], fullList: List[String]) {
        def |(x: String): check = {
            d(data.head) === x.split(",").toSet
            check(d, data.tail, fullList)
        }
        def |(d: Diagram): check = check(d, fullList, fullList)
      }

      val applyTo = new table

  private def diagonalize[T](f: Int => T): PartialFunction[(Int, Int), T] =
      { case (i, j) if i == j => f(i) }

S	M	T	W	T	F	S
1	2	3	4	5	6	7
8	9	10	11	12	13	14
15	16	17	18	19	20	21
22	23	24	25	26	27	28
29	30

Observations

Views from Souths

Entries tagged with topos

Σ⊣*⊣Π

spent some leisure time writing a useful reference page

come listen to my talk on topos logic implementation

til

сегодня праздник у девчат

еще похвастаться

some progress with logic

hurray, conjunction test passed

the kind of programming

strangely categorical construct I needed

Profile

June 2025

Syndicate

Most Popular Tags

Page Summary

Active Entries

Style Credit

Expand Cut Tags