Unify two developments of frames (`frame.lagda` and `Frame.lagda`)

[ayberkt]

Unify two developments of frames (`frame.lagda` and `Frame.lagda`)

[martinescardo]

@glangmead: I renamed frame to Frame-version1.

@ayberkt: I am going to close this issue. It is actually useful to have the two versions of frames for pedagogical purposes.

[glangmead]

This also causes an error on non-case-sensitive systems like macOS with the default filesystem, such that I only obtain one of the two files via git (which is the lowercase frame.lagda):

warning: the following paths have collided (e.g. case-sensitive paths
on a case-insensitive filesystem) and only one from the same
colliding group is in the working tree:

  'source/Frame.lagda'
  'source/frame.lagda'

[ayberkt]

which I believe defines σ-frames

Actually, this seems to define frames in general! Did PR #44 re-define an already existing definition then? What should we do about this?

[martinescardo]

I had forgotten that I had already defined frame. I think it is used somewhere, but I only needed a minimal definition of frame (TypeTopology defines things on demand.). We need to check and unify the two separate developments.