Record Of AIMXVII

- HTML version, org-mode source

                          ____________________

                           RECORD OF AIM XVII
                          ____________________


Table of Contents
_________________

1 Participants:
2 (7 May Tue)
.. 2.1 Supper 18:30 ~
3 8 May Wed.
.. 3.1 Agenda discussion, orientation : 9.00 - 10.00
.. 3.2 James Chapman(+all): On copatterns : 10.30 - 11.45, 14.00 - 17.30
4 9 May Thr.
.. 4.1 Yoshiki Kinoshita: Category Theoretic Structure of Setoids (with John Power)
.. 4.2 James Chapman: On copatterns: 11.00 - 12.00
.. 4.3 (James Chapman and Makoto Takeyama only): (Not) speeding up Agda type checking : 13.30 - 14.00
.. 4.4 Shuji Kinoshita: On Granström's World : 14.00 - 15.30
.. 4.5 X-Sprint : 15.45 - 18.00
5 10 May Fri. : Excursion
6 11 May Sat.
.. 6.1 James Chapman : Formalizing restriction categories : 09.00 - 10.40
.. 6.2 Bengt Nordström : Incremental Type Checking : 11.20 - 12.00, 14.00 - 15.40
.. 6.3 MT : Meta-verification and validation 16.00 - 17.00
.. 6.4 X-Sprint : 17.00 - 18.00
7 12 May Sun.
.. 7.1 Liyang Hu : Software Transactional Memory : 09.00 - 11.40
.. 7.2 X-Sprint : All : 14.00 - 17.30
.. 7.3 Wrap up
.. 7.4 JC and MT:
.. 7.5 YK and JC:
.. 7.6 SK
.. 7.7 JC and SK and MT
8 13 May Mon.
.. 8.1 X-Sprint, Wrap-up
.. 8.2 Next AIM Discussion:


1 Participants:
===============

  - James Chapman (Institute of Cybernetics)
  - Shuji Kinoshita (NAIST)
  - Yoshiki Kinoshita (Kanagawa U)
  - Bengt Nordström (Chalmers)
  - Makoto Takeyama (Kanagawa U)
  - Liyang Hu (Tsuru Capital LLC / U Nottingham)


2 (7 May Tue)
=============

2.1 Supper 18:30 ~
~~~~~~~~~~~~~~~~~~


3 8 May Wed.
============

3.1 Agenda discussion, orientation : 9.00 - 10.00
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

§ 3.1.1 Planned schedule: [http://wiki.portal.chalmers.se/agda/uploads/Main.AIMXVII/AIMXVIITImeTalbe.pdf]

  (Excursion moved to Friday due to the forcasted rain on Saturday.)


§ 3.1.2 Actual

  ---------------------------------------------------------------------------------------------
   Wed  JC       10.30 - 11.45  On Copatterns                                                  
        JC, All  14.00 - 17.30  Continued to discussion sprint? on copatterns                  
  ---------------------------------------------------------------------------------------------
   Thr  YK       09.00 - 10.40  Category Theoretic Structure of Setoids                        
        JC       11.00 - 12.00  On Copatterns (cont.)                                          
        (JC,MT)  13.30 - 14.00  ((Not) speeding up Agda type checking)                         
        SK       14.00 - 15.30  On Granström's Worlds                                          
        All      15.45 - 18.00  X-Sprint                                                       
                 15.45 - 17.50  - JC,MT,BN : Discussion on Copatterns (cont.)                  
                                - BN: Explanation of batch type checking                       
                                - SK: Agda formalisation of the category of Granström's worlds 
  ---------------------------------------------------------------------------------------------
   Fri           Excursion                                                                     
  ---------------------------------------------------------------------------------------------
   Sat  JC       09.00 - 11:00  Formalizing restriction categories                             
        BN       11.20 - 12:00  Incremental Type checking                                      
        BN       14.00 - 15.40  Incremental Type checking (Cont.)                              
        MT       16.00 - 17.00  Meta-verifcation and validation                                
        All      17.00 - 18.00  X-Sprint                                                       
  ---------------------------------------------------------------------------------------------
   Sun  LH       09.00 - 11.30  Software Transactional Memory                                  
        All      14.00 - 17.00  X-Sprint                                                       
   Mon  All      09.00 - 12.00  X-Sprint, wrap-up.                                             
  ---------------------------------------------------------------------------------------------


3.2 James Chapman(+all): On copatterns : 10.30 - 11.45, 14.00 - 17.30
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

§ 3.2.1 Summary

  JC led the discussion on coinduction and copatterns based on
  ,----
  | Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer.
  | Copatterns - Programming Infinite Structures by Observations -. POPL 2013
  | http://www.tcs.ifi.lmu.de/~abel/popl13.pdf
  `----
  up to Section 5.1
  - BN: Analysing general scheme of coinductive definition with nested
    (co)patterns are too complex. We should study simple copatterns /
    corecursors like we do for inductive types.
  - Lots of discussions on the sense of "values" and "getting stuck"
  - Extension to dependent types where type equality involves
    computation seems non trivial.


§ 3.2.2 More details

  - BN: If we take "observers define a coinductive type" seriously, a
    suitable notation for declaring typing of observers is something
    like
    ,----
    | Stream A = { X : Type ; head : X → A ; tail : X → X }
    `----
    not like field label declarations
    ,----
    | Stream A = { head : A ; tail : Stream A}
    `----
  - BN: It is hard to try reasoning about the general definition schema
    with nested (co)patterns as in the paper. *We could study what
    corresponds to the recursor / elimination principle for coinductive
    types and explain general definitions in terms of that.* (Like the
    pattern matching definition of `_+_' is understood in terms of the
    recursor on ℕ.)
  - The sense of "values" (which affects the sense of "not getting
    stuck", "progress" and "coverage")
    - To say any expression of a negative type is a value seems rough.
      Is the expression "f ∘ g" a value? (function types are negative.)
    - What the values of a coinductive type are is not explained as
      clearly as those of an inductive type.
      - Is there a problem with the usual "a stream value is one that
        has cons-headed form with head and tail revealed"? Or is a
        stream value anything that we know for sure we can make into a
        cons? (Is the latter just turning the theorem "don't go wrong"
        to a definition?)
      - Is it inappropriate to ask what they are?
    - Values usually are considered for the purpose of conversion
      checking (besides for being answers). But the paper's type system
      does not require conversion checking, so the role of value-ness in
      that regard is unclear.
  - The sense of polarity of types? Positive = defined by introduction,
    Negative = defined by elimination?
  - Relationship between the polarity of types and the bidirectional
    checking? Here checking vs inferring more or less align with
    polarity of the type (positive → checked against (at first);
    negative → inferred). Is there some significance to this? How does
    this relate to the usual alignment with the form of the term
    (introductory → checked against a type; neutral → inferred)?
  - Why the main function must have positive type? Not all objects of
    negative type seem infinite or unprintable.
  - What is the status of the reduction relation generated from the
    observation rules of a program in Sec 4? Is this the operational
    semantics of the program? Non-deterministic without a strategy?
    (while evaluation contexts usually are considered in order to
    specify a strategy?)
  - It seems non-trivial extend all this to dependent types where type
    conversion checking involves computation, particularly Lemma 7.
  - Missing lemma to apply Lemma 8 for Theorem 4?
    - "If Γ ⊢ E[f] : B then Γ | Σ(f) ⊢ E : B"
    Ok by induction on E.
  - BN: Starting with general copatterns makes it hard to see what is
    happening. What it means to be an object of a coinductive type
    should be defined to be being able to prove that the (simple)
    observations on that objet is defined. Type system should guarantee
    that complex observations are defined.
  - The sense of values and getting stuck again.
    - Is the seemingly non-deterministic reduction relation in Sec 4 CR?
    - Is the sense of "getting stuck" dependent on reduction strategies?
      - Usually a programming langauge semantics comes with a
        deterministic strategy and no questions arise about CR or
        various senses of getting stuck. The paper is more in the lambda
        calculus tradition?
  - Finished for today at the end of Sec 5.1


4 9 May Thr.
============

4.1 Yoshiki Kinoshita: Category Theoretic Structure of Setoids (with John Power)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

  Discussed the paper
  ,----
  | Power, J. and Kinoshita, Y.
  | Category theoretic structure of setoids.
  | Theoretical Computer Science. ISSN 0304-3975 (In Press)
  | http://opus.bath.ac.uk/34231/1/main.pdf
  `----
  - Mathematical formulation of a setoid where the equivalence relation
    is replaced by family of sets with refl, sym and trans witnessed by
    families of functions without coherence requirements.
  - Discussion on the sense of formalising naive set theory based
    mathematics in Agda.
  - Structures on the category Equiv of equivalence relations (complete,
    cocomplete, exponentials) and Setoid of setoids (products,
    coproducts, exponentials, no equalisers and coequalisers).
  - Equiv-enriched Seotid and its weak eqaulisers (inserters).
  - Discussion on the senses of the terms "proof irrelevance"
    1. Identifying all proofs (1a. of certain propositions, or 1b. that
       appear as function arguments at positions that are declared
       irrelevant.)
       - justified by not analysing proofs / not using proofs relevantly
         in computation.
    2. Never comparing two proofs (while not positively identifying the
       two).
    3. Only caring about existence / non-existence of proofs
    - 1. is the usual technical meaning, but how to call 2? How does 3
      relate with 1 and 2 exactly?


4.2 James Chapman: On copatterns: 11.00 - 12.00
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

  Continued the discussion from Wednesday.
  - Still trying to understand the sense of "not getting stuck" from the
    definition of copattern coverage.
    - Why don't we see "getting stuck on a variable"? What is preventing
      computation under context in this system?


4.3 (James Chapman and Makoto Takeyama only): (Not) speeding up Agda type checking : 13.30 - 14.00
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

  Experimented on how to speed up type checking / lessen memory usage on
  JC's category theory code.
  - Use of "abstract" helped slightly but there were not much
    opportunity for it for the code already heavily annotated for
    irrelevance.
  - Moving let definitions to where clause helped one file but made
    things worse for the overall build.
  - Splitting files up


4.4 Shuji Kinoshita: On Granström's Wold : 14.00 - 15.30
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

  Discussed the paper
  ,----
  | Johan G. Granström. A new paradigm for component-based development.
  | JOURNAL OF SOFTWARE, VOL. 7, NO. 5, MAY 2012
  | https://www.academypublisher.com/~academz3/ojs/index.php/jsw/article/view/jsw070511361148
  `----
  - Worlds, world maps, the category of world
  - Things that were figured out during discussion, which turned out to
    be written in the later part of the paper:
    - For w = (C, R), w ⇒ X is like the W-type W(C,R), but parameterised
      in the type X of leaves. W(C,R) ≅ w ⇒ 1.
    - w ⇒ X is the free monad on the functor ⟦ w ⟧ X = Σ c : C . R c → X
    - a world map w₁ ⊸ w₂ is a container map w₂ → w₁̂̂*
  - The equality on programs seems a usual inductive predicate - why is
    it called a new primitiv of type theory?
  - It was not clear what exactly is new compared with the original
    Hancock-Setzer or with container works.


4.5 X-Sprint : 15.45 - 18.00
~~~~~~~~~~~~~~~~~~~~~~~~~~~~

§ 4.5.1 JC and MT, BN

  Continued copatterns discussion.
  - In the statement of case 4 of Lemma 14, ⊬v e : B should be read ⊢ e
    : B and ⊬v e : B for the proof of Thm 15 (Progress)?
  - In the proof of Progress, why is E₁, and not E₂, shown to be a value
    context?
  - From the statement of Progress, "not getting stuck" is seen to apply
    only for closed terms.
  - To say any expresssion of a negative type is a value still felt
    unsatisfactory as an explanation of what a value of a coinductive
    types is.
  - Looked for an answer for the above in Granström's thesis, which
    turned into a wild goose chase. Found no Easter eggs.


§ 4.5.2 BN

  Worked on the explanation of batch type-checking.


§ 4.5.3 SK

  Worked on Agda formalisation of Granström's worlds.


5 10 May Fri. : Excursion
=========================

  - 09.11 - 10.24 : From Shonan OVA to Enoshima Station
    [http://goo.gl/maps/vUe0Y]
  - 10.24 - 15.40 : Walk along Sagami Bay beach
    [http://goo.gl/maps/aDwyo]
    - 12.40 - 14.40 : Lunch: Shabu Shabu 'Viking' buffet
  - 16.10 - 16.40 : To Inamuragasaki Onsen [http://goo.gl/maps/YXtlZ]
  - 16.40 - 19.00 : Bath
    [http://inamuragasaki-onsen.com/ofuro/index.html]
  - 19.00 - 20.40 : Dinner [http://www.main-inamuragasaki.jp/index.html]
  - 20.40 - 21.10 : To Shonan OVA


6 11 May Sat.
=============

6.1 James Chapman : Formalizing restriction categories : 09.00 - 10.40
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

  Discussed the paper
  ,----
  | James Chapman, Tarmo Uustalu and Niccolò Veltri.
  | Formalizing restriction categories. PCC 2013
  | slides url?
  `----


§ 6.1.1 Formalising frameworks of Cockett and Lacks "Restriction Categories"

  - Partial map categories
  - Restriction categories


§ 6.1.2 Categoraical Approaches to Partiality

  - Partial map categories. Partial map synthed from toal maps
  - Partial product categories (di Paola, Heller; Robinson, Rosolini),
    Restriction categories (Cockett, Lack) - axiomatic approaches
  - Partila map classification - sometimes pmaps are the Kleisili maps
    of a monad on the toal map category
  - Recusion categories (di Paorla, Heller). Turing categories (Cockett,
    HExtra) - computational.


§ 6.1.3 Restriction Categories

  - For f : A → B, has f̅ : A → A, which
    - R1 : f ∘ f̅ = f
    - R2 : f̅ ∘ g̅ = g̅ ∘ f̅
    - R3 : g̅ ∘ f̅ = rest(g ∘ f̅)
    - R4 : ...
  - <Looking at Agda code> type in types. Het equality. With many axioms
    for extensionality and quotienting.


§ 6.1.4 Restriction Categories: Examples


§ 6.1.5 Stable Systems of Monics


§ 6.1.6 Partial Map Categories


§ 6.1.7 Partial Map Categories : Examples


§ 6.1.8 From Partial Map Categories to Restriction category


§ 6.1.9 From Restriction category to Partial map cat

  - Needs idempotent splitting.
  - X &#8773; Par(Total(X), M)


§ 6.1.10 Wrap-up

  - Check up the notion of stable factorization system
  - Check up those old papers from late 80's referred in Robin's paper,
    like those of Giuseppe Rossolini.
  - Also the relationship between Set and Rel as detailed in Peter
    Johnstone's book.


6.2 Bengt Nordström : Incremental Type Checking : 11.20 - 12.00, 14.00 - 15.40
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

§ 6.2.1 Syntax

  ,----
  | a ::= i | (a e) -- application, avoiding beta-redex
  | e ::= a | Set | &#928; e f | fun f
  | f ::= lam x e
  `----


§ 6.2.2 Declarations

  ,----
  | c&#8321; : t&#8321; ; ... ; cn / tn
  `----


§ 6.2.3 Steps

  1. No defined constant
  2. With definition
  - c&#8321; = e&#8321; ; ... ; cn : tn


§ 6.2.4 With the usual type systems.


§ 6.2.5 Incremental type checking

  In situation
  ,----
  | ? &#8712; t
  `----
  1. Refinigning with constant c results in
  ,----
  | c ?&#8321; ... ?n &#8712; t
  | ?&#8321; &#8712; A&#8321; ... ?n &#8712; An
  `----
  1. Refinieng with Set is an error
  2. with &#928; is error
  3. with fun, the result is
  ,----
  | fun (lam ?&#8321; ?&#8322;)
  `----


§ 6.2.6 Rep. of Terms under construction

  - is a tree with (nodes and) leaves being placeholders.
  - a sate is like
  ,----
  | q&#8321; = c&#8321; q11 ... q1n1
  | q&#8322; = c&#8322; q21 ... q2n2
  | ...
  `----
  plus constant declarations and definitions and constraints.


§ 6.2.7 Thin expressions

  ,----
  | e ::= c q1 .. qn 
  |     | Set
  |     | &#928; q q&#8242;
  |     | &#955; q'
  |     | q
  | q' := lam q&#8321; q&#8322;
  `----


§ 6.2.8 Commands from a state to state

  1. q := thin-e -- refinement
  2. c :: thin-e -- type declaration
  3. c = thin-e -- definition
  4. q&#8321; := q&#8320; -- deletion; delete what's bound to q&#8321; and replace with q&#8320;


§ 6.2.9 Batch type checking

  too complex to understand. The goal is to simplify and understand.


§ 6.2.10 Batch checking algorithm

  ,----
  | -- induction over G
  | checkType e (G : Well typed context) : Result Ok
  | checkType a G =
  |   Ok := checkObj a Set G
  | checkType Set G = Ok
  | checkType (Pi e f) G =
  |   Ok := checkType e G
  |   x  := fresh G -- get a new constant in G
  |   Ok := checkType (apply f x) (update G x e)
  | checkType (fun f) = error
  | ...
  `----


§ 6.2.11 Question:

  In inferring type of an application (f : Pi a b)(e : a), apply b e
  must reduce beta-redexes. Is this avoidable?
  - Yes, if you take the closure value approach.
  - B wants values to be expressions. Can't expressions be extended?
  - Yes, but then you must consider their reductions too (those like
    explicit substitution calculus).


§ 6.2.12 Wrap-up

  - A lot of discussion on having separate worlds of expressions and
    values or having values to be certain expressions.
  - You can write in Haskell in the way BN wants to write with
    do-notation.
  - that last question above.


6.3 MT : Meta-verification and validation 16.00 - 17.00
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

  Discussed how parts of validation could be verification about
  properties of formal assurance cases as objects.


§ 6.3.1 Wrap-up

  Consider having composable primitives of validation / verification
  activities and proving something about properties of those
  combination. Cf. Simon Peyton Jones' paper "Composing contracts: an
  adventure in financial engineering."


6.4 X-Sprint : 17.00 - 18.00
~~~~~~~~~~~~~~~~~~~~~~~~~~~~

  - BN:
  - JC:
  - LH:
  - MT: investigated the possiblities of binary distribution of Agda on
    Windows independent of Haskelll Platform. There seems to be no
    problems technically, as libraries seems to be all statically linked
    on Windows. Statically linked GNU GMP library etc cause problems in
    terms of licenses.
  - YK:


7 12 May Sun.
=============

7.1 Liyang Hu : Software Transactional Memory : 09.00 - 11.40
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

§ 7.1.1 Background (1hr)

  - IO monad, IORef a
    ,----
    | data IO a = ...
    | data IORef a = ...
    `----
  - STM monad, TVar a
    ,----
    | data STM a = ...
    | instance Monad STM where ...
    | data TVar a = ...
    | readTVar :: TVar a &#8594; STM a
    | writeTVar :: a &#8594; TVar a &#8594; STM()
    | atomically :: STM a &#8594; IO a
    | retry :: STM a
    | orElse :: STM a &#8594; STM a &#8594; STM a
    | forkIO :: IO () &#8594; IO ()
    `----


§ 7.1.2 The Language (Hutton's Razor)

  - STM level
  ,----
  | data Expression&#8242; : Set where
  |   #_ : (m : &#8469;) &#8594; Expression&#8242;
  |   _&#8853;_ : (a b : Expression&#8242;) &#8594; Expression&#8242;
  |   read : (v : Variable) &#8594; Expression&#8242;
  |   write : (v : Variable)(e : Expression&#8242;) &#8594; Expression&#8242;
  `----
  - IO level
  ,----
  | data Expression
  |   #_ : (m : &#8469;) &#8594; Expression
  |   _&#8853;_ : (a b : Expression) &#8594; Expression
  |   atomic : (e : Expression&#8242;) &#8594; Expression
  `----
  - No fork, but instead non-deterministic semantics.


§ 7.1.3 Heaps and Variables

  ,----
  | postulate &#8739;Heap&#8739; : &#8469;
  | Heap : Set
  | Heap = Vec &#8469; &#8739;Heap&#8739;
  | Variables = Fin &#8739;Heap&#8739;
  `----


§ 7.1.4 1 step reduction

  (&#8614; ~ "stop the world semantics")
  ,----
  | data _&#8614;&#8242;_ : Rel(Heap × Expression&#8242;)
  |   &#8614;&#8242;-&#8853;&#8469; : &#8704; {h m n} &#8594; (h , # m) &#8853; # n &#8614;&#8242; (h, #(m + n))
  |   ...
  |   &#8614;&#8242;-read : h , reav v &#8614;&#8242; h , # h[v]
  |   &#8614;&#8242;-write : h , write v (# n) &#8614;&#8242; h [ v ]:= m , # m
  |   ...
  `----


§ 7.1.5 Action

  &#964; silent action c2 c3


§ 7.1.6 Labeled Transition System

  Action &#8594; Rel(Heap × Expression)

  &#8614;-atomic : &#8704; {h e h' e'} &#8594; (e&#8614;*m : h, e &#8614;* h' , # m) &#8594; (c3 &#9655; h ,
    atomic e) &#8614; (h' , # m)

  &#8614;-mutate : &#8704; h' {h e} &#8594; (&#964; &#9655; h , atomic e) &#8614; (h' , atomic e)


§ 7.1.7 Transaction Log and Consistency

  - Log-based implementation of transaction: read-log and wright-log
  ,----
  | data Logs : Set where
  |   constrocutre _&_
  |   field
  |     &#961; &#969; : Vec (Maybe &#8469;) &#8739;HEap&#8739;
  | 
  | Write : Logs &#8594; Variables &#8594; &#8469; &#8594; Logs
  | Read : Heap &#8594; Logs Variable &#8594; Logs × &#8469;
  | -- check if you yourself have written; then return that
  | .. ow, check if you have read before; then return that
  | .. ow, read heap and record that fact in read log.
  `----


§ 7.1.8 Consistency

  ,----
  | Consistent: Heap &#8594; Logs &#8594; Set
  | Consistent h (&#961; & _) = &#8704; v m &#8594; &#961; [ v ] &#8801; Just m &#8594; h [ v ] &#8801; m
  `----
  Consistency is decidable - sicne Heap is finite.

  ,----
  | Update-lookup : Heap &#8594; Logs &#8594; Variable &#8594; &#8469;
  | -- if you have written, what you wrote; else read from heap
  | Update h l = tabulate (Update-lookup h l)
  `----


§ 7.1.9 Log-Based Semantics

  (&#8611; ~ log-based, non-stop-the-world semantics) Heap are not updated by
  this one-step (write goes to log)
  - STM level
  ,----
  | data _&#8866;_&#8611;&#8242;_ (h : Heap) : Rel(Logs × Expression&#8242;) where
  | ...
  `----
  - IO level
  ,----
  | TState = Maybe (Expression&#8242; × Log)
  | data _&#9655;_&#8611;_ : Action &#8594; Rel(Heap × TState × Expression)
  | ....
  `----
  &#8611;-mutate allows heap to be changed in anyway.


§ 7.1.10 Bisimilarity of Semantics (between &#8614; version and &#8611; version)


7.2 X-Sprint : All : 14.00 - 17.30
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


7.3 Wrap up
~~~~~~~~~~~


7.4 JC and MT:
~~~~~~~~~~~~~~

  Discussed copatterns and termination/productivity.


7.5 YK and JC:
~~~~~~~~~~~~~~

  - Looked at Agda formalisation of each other on
    - Category theory, Yoneda lemma
    - Normalisation by Evaluation
  - Planning to put up a category theory library on a git hub.


7.6 SK
~~~~~~

  Formalising Granstroem's worlds. 20% remaining.


7.7 JC and SK and MT
~~~~~~~~~~~~~~~~~~~~

  Pullback. Discussed the situation of
  ,----
  | DirectedContainer ---------> Comonad Set
  |   |                             |
  |   |                             |
  |   v                             v
  | Container -----------------> Endo Set
  `----
  in the context of JG's Worlds.

  There's a progression of
  ,----
  | World --> Endo Set --> Mnd Set
  | w         &#10214;w&#10215;          w=>_
  `----


8 13 May Mon.
=============

8.1 X-Sprint, Wrap-up
~~~~~~~~~~~~~~~~~~~~~

§ 8.1.1 SK: Agda code formalising Granström's World

  World, world map, composition, id, unit-laws, lifting-laws,


§ 8.1.2 LH: Discussion on formulation of bisimilarity


§ 8.1.3 JC, MT, BN: nothing to add to yesterday


§ 8.1.4 YK: Yoneda lemma and NbE for category

  - NbE for monoid expression via Yoneda applied to monoids as 1-object
    categories, using free monoid on "strict setoids"
  - NbE for path expression of a graph free categories on a graph.


8.2 Next AIM Discussion:
~~~~~~~~~~~~~~~~~~~~~~~~

  It would be good to have the next AIM in Gothenburg. BN will talk with
  Ulf and Nisse about dates / place in Gothenburg to make sure they can
  attend.