Thread Links			Date Links
Thread Prev	Thread Next	Thread Index	Date Prev	Date Next	Date Index

ONT Re: Differential Logic

To: Inquiry <inquiry@stderr.org>, Ontology <ontology@ieee.org>, SemioCom <gdsemiocom@univ-perp.fr>
Subject: ONT Re: Differential Logic
From: Jon Awbrey <jawbrey@oakland.edu>
Date: Sat, 07 Jun 2003 23:18:03 -0400
References: <3E982563.F67459A5@oakland.edu> <3EB73352.259E602@oakland.edu> <3EDC0D54.D068D971@oakland.edu> <3EDCC2DA.ED1AF1C9@oakland.edu> <3EDCE234.D1E311FF@oakland.edu> <3EDD60C0.F2108C0@oakland.edu> <3EDE3B22.60A09F83@oakland.edu> <3EDEAE71.46BB1B1@oakland.edu> <3EDF556A.E2D8D8C5@oakland.edu> <3EDF9E7D.1BEB2C08@oakland.edu> <3EE003B8.7476DAFC@oakland.edu> <3EE21FCE.DE4A05AD@oakland.edu>
Sender: owner-ontology@majordomo.ieee.org


o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

DLOG.  Note D83

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

Transformations of Type B^2 -> B^2 (concl.)

Figure 70-b shows another way to picture the action of the tangent functor
on the logical transformation F<u, v> = <((u)(v)), ((u, v))>, roughly in
the style of the "bundle of universes" type of diagram.  [NB.  I can't
really do justice to the original Figure in ascii graphics, but this
collection of pictures may serve as a construction kit, with some
assembly required, to convey the general idea.]

o-----------------------o  o-----------------------o  o-----------------------o
| dU                    |  | dU                    |  | dU                    |
|      o--o   o--o      |  |      o--o   o--o      |  |      o--o   o--o      |
|     /////\ /////\     |  |     /XXXX\ /XXXX\     |  |     /\\\\\ /\\\\\     |
|    ///////o//////\    |  |    /XXXXXXoXXXXXX\    |  |    /\\\\\\o\\\\\\\    |
|   //////// \//////\   |  |   /XXXXXX/ \XXXXXX\   |  |   /\\\\\\/ \\\\\\\\   |
|  o///////   \//////o  |  |  oXXXXXX/   \XXXXXXo  |  |  o\\\\\\/   \\\\\\\o  |
|  |/////o     o/////|  |  |  |XXXXXo     oXXXXX|  |  |  |\\\\\o     o\\\\\|  |
|  |/du//|     |//dv/|  |  |  |XXXXX|     |XXXXX|  |  |  |\du\\|     |\\dv\|  |
|  |/////o     o/////|  |  |  |XXXXXo     oXXXXX|  |  |  |\\\\\o     o\\\\\|  |
|  o//////\   ///////o  |  |  oXXXXXX\   /XXXXXXo  |  |  o\\\\\\\   /\\\\\\o  |
|   \//////\ ////////   |  |   \XXXXXX\ /XXXXXX/   |  |   \\\\\\\\ /\\\\\\/   |
|    \//////o///////    |  |    \XXXXXXoXXXXXX/    |  |    \\\\\\\o\\\\\\/    |
|     \///// \/////     |  |     \XXXX/ \XXXX/     |  |     \\\\\/ \\\\\/     |
|      o--o   o--o      |  |      o--o   o--o      |  |      o--o   o--o      |
|                       |  |                       |  |                       |
o-----------------------o  o-----------------------o  o-----------------------o
 =      du' @ (u)(v)       o-----------------------o          dv' @ (u)(v)   =
  =                        | dU'                   |                        =
   =                       |      o--o   o--o      |                       =
    =                      |     /////\ /\\\\\     |                      =
     =                     |    ///////o\\\\\\\    |                     =
      =                    |   ////////X\\\\\\\\   |                    =
       =                   |  o///////XXX\\\\\\\o  |                   =
        =                  |  |/////oXXXXXo\\\\\|  |                  =
         = = = = = = = = = = =|/du'/|XXXXX|\dv'\|= = = = = = = = = = =
                           |  |/////oXXXXXo\\\\\|  |
                           |  o//////\XXX/\\\\\\o  |
                           |   \//////\X/\\\\\\/   |
                           |    \//////o\\\\\\/    |
                           |     \///// \\\\\/     |
                           |      o--o   o--o      |
                           |                       |
                           o-----------------------o

o-----------------------o  o-----------------------o  o-----------------------o
| dU                    |  | dU                    |  | dU                    |
|      o--o   o--o      |  |      o--o   o--o      |  |      o--o   o--o      |
|     /    \ /////\     |  |     /\\\\\ /XXXX\     |  |     /\\\\\ /\\\\\     |
|    /      o//////\    |  |    /\\\\\\oXXXXXX\    |  |    /\\\\\\o\\\\\\\    |
|   /      //\//////\   |  |   /\\\\\\//\XXXXXX\   |  |   /\\\\\\/ \\\\\\\\   |
|  o      ////\//////o  |  |  o\\\\\\////\XXXXXXo  |  |  o\\\\\\/   \\\\\\\o  |
|  |     o/////o/////|  |  |  |\\\\\o/////oXXXXX|  |  |  |\\\\\o     o\\\\\|  |
|  | du  |/////|//dv/|  |  |  |\\\\\|/////|XXXXX|  |  |  |\du\\|     |\\dv\|  |
|  |     o/////o/////|  |  |  |\\\\\o/////oXXXXX|  |  |  |\\\\\o     o\\\\\|  |
|  o      \//////////o  |  |  o\\\\\\\////XXXXXXo  |  |  o\\\\\\\   /\\\\\\o  |
|   \      \/////////   |  |   \\\\\\\\//XXXXXX/   |  |   \\\\\\\\ /\\\\\\/   |
|    \      o///////    |  |    \\\\\\\oXXXXXX/    |  |    \\\\\\\o\\\\\\/    |
|     \    / \/////     |  |     \\\\\/ \XXXX/     |  |     \\\\\/ \\\\\/     |
|      o--o   o--o      |  |      o--o   o--o      |  |      o--o   o--o      |
|                       |  |                       |  |                       |
o-----------------------o  o-----------------------o  o-----------------------o
 =      du' @ (u) v        o-----------------------o          dv' @ (u) v    =
  =                        | dU'                   |                        =
   =                       |      o--o   o--o      |                       =
    =                      |     /////\ /\\\\\     |                      =
     =                     |    ///////o\\\\\\\    |                     =
      =                    |   ////////X\\\\\\\\   |                    =
       =                   |  o///////XXX\\\\\\\o  |                   =
        =                  |  |/////oXXXXXo\\\\\|  |                  =
         = = = = = = = = = = =|/du'/|XXXXX|\dv'\|= = = = = = = = = = =
                           |  |/////oXXXXXo\\\\\|  |
                           |  o//////\XXX/\\\\\\o  |
                           |   \//////\X/\\\\\\/   |
                           |    \//////o\\\\\\/    |
                           |     \///// \\\\\/     |
                           |      o--o   o--o      |
                           |                       |
                           o-----------------------o

o-----------------------o  o-----------------------o  o-----------------------o
| dU                    |  | dU                    |  | dU                    |
|      o--o   o--o      |  |      o--o   o--o      |  |      o--o   o--o      |
|     /////\ /    \     |  |     /XXXX\ /\\\\\     |  |     /\\\\\ /\\\\\     |
|    ///////o      \    |  |    /XXXXXXo\\\\\\\    |  |    /\\\\\\o\\\\\\\    |
|   /////////\      \   |  |   /XXXXXX//\\\\\\\\   |  |   /\\\\\\/ \\\\\\\\   |
|  o//////////\      o  |  |  oXXXXXX////\\\\\\\o  |  |  o\\\\\\/   \\\\\\\o  |
|  |/////o/////o     |  |  |  |XXXXXo/////o\\\\\|  |  |  |\\\\\o     o\\\\\|  |
|  |/du//|/////|  dv |  |  |  |XXXXX|/////|\\\\\|  |  |  |\du\\|     |\\dv\|  |
|  |/////o/////o     |  |  |  |XXXXXo/////o\\\\\|  |  |  |\\\\\o     o\\\\\|  |
|  o//////\////      o  |  |  oXXXXXX\////\\\\\\o  |  |  o\\\\\\\   /\\\\\\o  |
|   \//////\//      /   |  |   \XXXXXX\//\\\\\\/   |  |   \\\\\\\\ /\\\\\\/   |
|    \//////o      /    |  |    \XXXXXXo\\\\\\/    |  |    \\\\\\\o\\\\\\/    |
|     \///// \    /     |  |     \XXXX/ \\\\\/     |  |     \\\\\/ \\\\\/     |
|      o--o   o--o      |  |      o--o   o--o      |  |      o--o   o--o      |
|                       |  |                       |  |                       |
o-----------------------o  o-----------------------o  o-----------------------o
 =      du' @  u (v)       o-----------------------o          dv' @  u (v)   =
  =                        | dU'                   |                        =
   =                       |      o--o   o--o      |                       =
    =                      |     /////\ /\\\\\     |                      =
     =                     |    ///////o\\\\\\\    |                     =
      =                    |   ////////X\\\\\\\\   |                    =
       =                   |  o///////XXX\\\\\\\o  |                   =
        =                  |  |/////oXXXXXo\\\\\|  |                  =
         = = = = = = = = = = =|/du'/|XXXXX|\dv'\|= = = = = = = = = = =
                           |  |/////oXXXXXo\\\\\|  |
                           |  o//////\XXX/\\\\\\o  |
                           |   \//////\X/\\\\\\/   |
                           |    \//////o\\\\\\/    |
                           |     \///// \\\\\/     |
                           |      o--o   o--o      |
                           |                       |
                           o-----------------------o

o-----------------------o  o-----------------------o  o-----------------------o
| dU                    |  | dU                    |  | dU                    |
|      o--o   o--o      |  |      o--o   o--o      |  |      o--o   o--o      |
|     /    \ /    \     |  |     /\\\\\ /\\\\\     |  |     /\\\\\ /\\\\\     |
|    /      o      \    |  |    /\\\\\\o\\\\\\\    |  |    /\\\\\\o\\\\\\\    |
|   /      / \      \   |  |   /\\\\\\/ \\\\\\\\   |  |   /\\\\\\/ \\\\\\\\   |
|  o      /   \      o  |  |  o\\\\\\/   \\\\\\\o  |  |  o\\\\\\/   \\\\\\\o  |
|  |     o     o     |  |  |  |\\\\\o     o\\\\\|  |  |  |\\\\\o     o\\\\\|  |
|  | du  |     |  dv |  |  |  |\\\\\|     |\\\\\|  |  |  |\du\\|     |\\dv\|  |
|  |     o     o     |  |  |  |\\\\\o     o\\\\\|  |  |  |\\\\\o     o\\\\\|  |
|  o      \   /      o  |  |  o\\\\\\\   /\\\\\\o  |  |  o\\\\\\\   /\\\\\\o  |
|   \      \ /      /   |  |   \\\\\\\\ /\\\\\\/   |  |   \\\\\\\\ /\\\\\\/   |
|    \      o      /    |  |    \\\\\\\o\\\\\\/    |  |    \\\\\\\o\\\\\\/    |
|     \    / \    /     |  |     \\\\\/ \\\\\/     |  |     \\\\\/ \\\\\/     |
|      o--o   o--o      |  |      o--o   o--o      |  |      o--o   o--o      |
|                       |  |                       |  |                       |
o-----------------------o  o-----------------------o  o-----------------------o
 =      du' @  u v         o-----------------------o          dv' @  u v     =
  =                        | dU'                   |                        =
   =                       |      o--o   o--o      |                       =
    =                      |     /////\ /\\\\\     |                      =
     =                     |    ///////o\\\\\\\    |                     =
      =                    |   ////////X\\\\\\\\   |                    =
       =                   |  o///////XXX\\\\\\\o  |                   =
        =                  |  |/////oXXXXXo\\\\\|  |                  =
         = = = = = = = = = = =|/du'/|XXXXX|\dv'\|= = = = = = = = = = =
                           |  |/////oXXXXXo\\\\\|  |
                           |  o//////\XXX/\\\\\\o  |
                           |   \//////\X/\\\\\\/   |
                           |    \//////o\\\\\\/    |
                           |     \///// \\\\\/     |
                           |      o--o   o--o      |
                           |                       |
                           o-----------------------o

o-----------------------o  o-----------------------o  o-----------------------o
| U                     |  |\U\\\\\\\\\\\\\\\\\\\\\|  |\U\\\\\\\\\\\\\\\\\\\\\|
|      o--o   o--o      |  |\\\\\\o--o\\\o--o\\\\\\|  |\\\\\\o--o\\\o--o\\\\\\|
|     /////\ /////\     |  |\\\\\/////\\/////\\\\\\|  |\\\\\/    \\/    \\\\\\|
|    ///////o//////\    |  |\\\\///////o//////\\\\\|  |\\\\/      o      \\\\\|
|   /////////\//////\   |  |\\\////////X\//////\\\\|  |\\\/      /\\      \\\\|
|  o//////////\//////o  |  |\\o///////XXX\//////o\\|  |\\o      /\\\\      o\\|
|  |/////o/////o/////|  |  |\\|/////oXXXXXo/////|\\|  |\\|     o\\\\\o     |\\|
|  |//u//|/////|//v//|  |  |\\|//u//|XXXXX|//v//|\\|  |\\|  u  |\\\\\|  v  |\\|
|  |/////o/////o/////|  |  |\\|/////oXXXXXo/////|\\|  |\\|     o\\\\\o     |\\|
|  o//////\//////////o  |  |\\o//////\XXX///////o\\|  |\\o      \\\\/      o\\|
|   \//////\/////////   |  |\\\\//////\X////////\\\|  |\\\\      \\/      /\\\|
|    \//////o///////    |  |\\\\\//////o///////\\\\|  |\\\\\      o      /\\\\|
|     \///// \/////     |  |\\\\\\/////\\/////\\\\\|  |\\\\\\    /\\    /\\\\\|
|      o--o   o--o      |  |\\\\\\o--o\\\o--o\\\\\\|  |\\\\\\o--o\\\o--o\\\\\\|
|                       |  |\\\\\\\\\\\\\\\\\\\\\\\|  |\\\\\\\\\\\\\\\\\\\\\\\|
o-----------------------o  o-----------------------o  o-----------------------o
 =          u'             o-----------------------o              v'         =
  =                        | U'                    |                        =
   =                       |      o--o   o--o      |                       =
    =                      |     /////\ /\\\\\     |                      =
     =                     |    ///////o\\\\\\\    |                     =
      =                    |   ////////X\\\\\\\\   |                    =
       =                   |  o///////XXX\\\\\\\o  |                   =
        =                  |  |/////oXXXXXo\\\\\|  |                  =
         = = = = = = = = = = =|/u'//|XXXXX|\\v'\|= = = = = = = = = = =
                           |  |/////oXXXXXo\\\\\|  |
                           |  o//////\XXX/\\\\\\o  |
                           |   \//////\X/\\\\\\/   |
                           |    \//////o\\\\\\/    |
                           |     \///// \\\\\/     |
                           |      o--o   o--o      |
                           |                       |
                           o-----------------------o
Figure 70-b.  Tangent Functor Ferris Wheel for F<u, v> = <((u)(v)), ((u, v))>

Jon Awbrey

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

References:
- ONT Re: Differential Logic
  - From: Jon Awbrey <jawbrey@oakland.edu>
- ONT Re: Differential Logic
  - From: Jon Awbrey <jawbrey@oakland.edu>
- ONT Re: Differential Logic
  - From: Jon Awbrey <jawbrey@oakland.edu>
- ONT Re: Differential Logic
  - From: Jon Awbrey <jawbrey@oakland.edu>
- ONT Re: Differential Logic
  - From: Jon Awbrey <jawbrey@oakland.edu>
- ONT Re: Differential Logic
  - From: Jon Awbrey <jawbrey@oakland.edu>
- ONT Re: Differential Logic
  - From: Jon Awbrey <jawbrey@oakland.edu>
- ONT Re: Differential Logic
  - From: Jon Awbrey <jawbrey@oakland.edu>
- ONT Re: Differential Logic
  - From: Jon Awbrey <jawbrey@oakland.edu>
- ONT Re: Differential Logic
  - From: Jon Awbrey <jawbrey@oakland.edu>
- ONT Re: Differential Logic
  - From: Jon Awbrey <jawbrey@oakland.edu>

Prev by Date: ONT Re: Differential Logic
Next by Date: ONT Re: Differential Logic
Prev by thread: ONT Re: Differential Logic
Next by thread: ONT Re: Differential Logic
Index(es):
- Date
- Thread