You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: readme.adoc
+20Lines changed: 20 additions & 0 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -1,4 +1,8 @@
1
+
// SPDX-License-Identifier: MPL-2.0
2
+
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
1
3
= echo-types
4
+
image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=openssourcesecurity[OpenSSF Best Practices,link="https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/echo-types"]
5
+
2
6
3
7
image::docs/assets/banner.png[Echo Types — Proof-Relevant Information Residues,align="center"]
4
8
@@ -19,6 +23,22 @@ Echo types target a third case:
19
23
20
24
This repository treats that third case as the primary object of study.
21
25
26
+
== Semantic fibre and warrant prototype
27
+
28
+
The public vocabulary talks about *semantic fibre*: the possible-origin
29
+
structure that still lies over an observed artefact after a declared
30
+
lossy map. An artefact used *avec fibre* carries enough such structure
31
+
for the advertised inference; an artefact used *sans fibre* is only a
32
+
target-side value. A *warrant* is the inferential licence supplied by
33
+
the fibre or residue, but it is supporting vocabulary rather than the
34
+
headline mathematical object.
35
+
36
+
`docs/echo-types/prototypes/warrant_debugger_prototype.jsx` is the
37
+
doc-side React sketch for that warrant/debugging layer. It visualises an
38
+
empty fibre contradiction and then makes repair costs explicit when a
39
+
tool weakens, widens, or softens the active obligations. It is an
40
+
explanatory prototype, not an Agda proof artefact.
41
+
22
42
== Definition (Foundation)
23
43
24
44
Given `f : A -> B`, define the fiber/echo at `y : B`:
0 commit comments