7. An unfamiliar structure

This last lesson uses a structure that Definograph has no special knowledge of. Whatever it shows comes from the definition itself. You read the definition, then Definograph's figures of it, then follow where the proof of its law comes from. The exercises ask what the figures show.

The definition

These lines are from ReturnMap.lean:

structure ReturnMap where
  Source : Type
  Target : Type
  send : Source → Target
  back : Target → Source
  returns : ∀ x, back (send x) = x

example (system : ReturnMap) (unused : Nat) :
    ∀ x : system.Source, system.back (system.send x) = x :=
  system.returns

A ReturnMap bundles two types, Source and Target, a function send from Source to Target, a function back from Target to Source, and a law returns. The law says that applying send and then back gives back every input x. The dot means field access: system.send is the send field of system.

The example takes an existing system and a natural number unused, which it does not use. It states the law for system, and its proof is the law stored in system, system.returns.

The structure in the editor

With the editor set up as in Lesson 5, select the proposition in the example, from ∀ to the final = x, and run Definograph: Visualize Selection. The first step of the Visual sequence lists the parameters, system and unused, and opens system itself:

Recorded Definograph excerpt · Rendered 2 October 2026 · from a saved history · Adapts to page theme · Native capture 28 September 2026 · Dates in UTC · Saved input: Lean 4.28.0 · Lean was not rerun.

Lean source (39 lines)

Lean source file: ReturnMap.lean

structure ReturnMap where
  Source : Type
  Target : Type
  send : Source → Target
  back : Target → Source
  returns : ∀ x, back (send x) = x

example (system : ReturnMap) (unused : Nat) :
    ∀ x : system.Source, system.back (system.send x) = x :=
  system.returns

def unitToBool : ReturnMap where
  Source := Unit
  Target := Bool
  send := fun _ => false
  back := fun _ => ()
  returns := by
    intro x
    cases x
    rfl

example : unitToBool.back (unitToBool.send ()) = () := rfl

theorem reverse_trip_fails :
    unitToBool.send (unitToBool.back true) ≠ true := by
  change false ≠ true
  decide

theorem send_injective (system : ReturnMap) :
    ∀ a b : system.Source, system.send a = system.send b → a = b := by
  intro a b same
  calc
    a = system.back (system.send a) := (system.returns a).symm
    _ = system.back (system.send b) := congrArg system.back same
    _ = b := system.returns b

#print axioms unitToBool
#print axioms reverse_trip_fails
#print axioms send_injective

Object structure

Inside system

ReturnMap

4 data fields · 1 law

These fields belong to this object, within the statement’s current quantifiers and assumptions.

What it contains

Field names and declared types

Arrows show function types. Set frames show membership domains, with no coordinates, shape, size, or chosen elements.

What its fields must satisfy

Read each law in declaration order.

1 / 1

1returns

Excerpt from step 1 of the Visual sequence: the structure inside system, with its data and its law.

Inside system counts "4 data fields · 1 law", and says: "These fields belong to this object, within the statement’s current quantifiers and assumptions."
What it contains draws the data: the functions send and back, and the two types they go between, system.Source and system.Target, labeled "carrier type". On a narrow screen, scroll the diagram sideways to see both types.
What its fields must satisfy lists the one law, returns. In Definograph you can read the law as a small visual sequence of its own.

Definograph has no rule for ReturnMap. It found these fields and this law in the definition.

The last step of the Visual sequence draws the round trip. On a screen narrower than the diagram, scroll the diagram sideways to see where the route ends.

Recorded Definograph output · Rendered 2 October 2026 · from a saved history · Adapts to page theme · Native capture 28 September 2026 · Dates in UTC · Saved input: Lean 4.28.0 · Lean was not rerun.

Lean source (39 lines)

Lean source file: ReturnMap.lean

structure ReturnMap where
  Source : Type
  Target : Type
  send : Source → Target
  back : Target → Source
  returns : ∀ x, back (send x) = x

example (system : ReturnMap) (unused : Nat) :
    ∀ x : system.Source, system.back (system.send x) = x :=
  system.returns

def unitToBool : ReturnMap where
  Source := Unit
  Target := Bool
  send := fun _ => false
  back := fun _ => ()
  returns := by
    intro x
    cases x
    rfl

example : unitToBool.back (unitToBool.send ()) = () := rfl

theorem reverse_trip_fails :
    unitToBool.send (unitToBool.back true) ≠ true := by
  change false ≠ true
  decide

theorem send_injective (system : ReturnMap) :
    ∀ a b : system.Source, system.send a = system.send b → a = b := by
  intro a b same
  calc
    a = system.back (system.send a) := (system.returns a).symm
    _ = system.back (system.send b) := congrArg system.back same
    _ = b := system.returns b

#print axioms unitToBool
#print axioms reverse_trip_fails
#print axioms send_injective

In scopesystem : ReturnMapunused : Nat∀ x : system.Source

Compare

Compare the expressions with =

Read the = relation between the two expressions within this logical context.

system.back(system.send(x)) equals x

Compare the outputs of these map paths: they are required to agree.

Inside this expression 2 relations

Lean fragment and source context

Schematics describe the conditions in their logical context. Shapes and spacing carry no unstated geometric meaning.

The last step of the Visual sequence, step 5 of 5: the round trip through send and back compared with x. The map paths are required to agree; the figure does not check that they do.

Where the proof comes from

The editor can also show where the proof of the law comes from. Select system.returns in the last line of the example and run Definograph: Visualize Selection. Open Source data, and in Checker input choose the occurrence of system inside system.returns. Then choose, in turn, Check chosen occurrence, Inspect fields of original occurrence, Check field returns, Inspect type of this term and Read logical structure of this term (one layer).

The history now has four steps: Inspect fields, Check field 5 (returns is the fifth field), Inspect type and Read logical structure. Ordered provenance shows how the law was reached from system:

Lean source (39 lines)

Lean source file: ReturnMap.lean

structure ReturnMap where
  Source : Type
  Target : Type
  send : Source → Target
  back : Target → Source
  returns : ∀ x, back (send x) = x

example (system : ReturnMap) (unused : Nat) :
    ∀ x : system.Source, system.back (system.send x) = x :=
  system.returns

def unitToBool : ReturnMap where
  Source := Unit
  Target := Bool
  send := fun _ => false
  back := fun _ => ()
  returns := by
    intro x
    cases x
    rfl

example : unitToBool.back (unitToBool.send ()) = () := rfl

theorem reverse_trip_fails :
    unitToBool.send (unitToBool.back true) ≠ true := by
  change false ≠ true
  decide

theorem send_injective (system : ReturnMap) :
    ∀ a b : system.Source, system.send a = system.send b → a = b := by
  intro a b same
  calc
    a = system.back (system.send a) := (system.returns a).symm
    _ = system.back (system.send b) := congrArg system.back same
    _ = b := system.returns b

#print axioms unitToBool
#print axioms reverse_trip_fails
#print axioms send_injective

Ordered provenance · through step 4 of this attempt

Occurrence 1
First appeared in the original selected occurrence (3c9d90c7)
Outcomes 1–6 recorded by attempt 4 (44314aa1) · the checks that record made to produce this occurrence
Formation: not established · Binder-domain formation: not established
1. Direct fields listed: 5 · first appeared in attempt 1 (0b49be6f), step 1 · no kernel outcomes recorded by attempt 4 (44314aa1) for this entry
Exact context, term and type of this occurrence
Projected field 5 · returns
First appeared in attempt 2 (8a6f7071), step 2
Outcomes 7–9 recorded by attempt 4 (44314aa1)
Occurrence 2
First appeared in attempt 2 (8a6f7071), step 2
Outcomes 7–9 recorded by attempt 4 (44314aa1) · the checks that record made to produce this occurrence
Formation: not established · Binder-domain formation: not established
Exact context, term and type of this occurrence
Type of the previous occurrence
First appeared in attempt 3 (31895a57), step 3
Outcomes 10–11 recorded by attempt 4 (44314aa1)
Occurrence 3
First appeared in attempt 3 (31895a57), step 3
Outcomes 10–11 recorded by attempt 4 (44314aa1) · the checks that record made to produce this occurrence, also listed below as a formation outcome: the same recorded outcomes, not a second check
Formation: established as a proposition · Binder-domain formation: established as a type above Prop
1. Type-component outcome accepted · a proposition · first appeared in attempt 3 (31895a57), step 3 · outcomes 10–11 recorded by attempt 4 (44314aa1)
2. Logical root outcome accepted · a proposition · first appeared in attempt 4 (44314aa1), step 4 · outcomes 12–15 recorded by attempt 4 (44314aa1)
These 2 accepted outcomes are receipts of one checked judgement in this capture, not independent confirmation.
1. Logical inspection · shape forall · root outcome accepted · universal statement · binder domain a type above Prop, outcome accepted · first appeared in attempt 4 (44314aa1), step 4 · outcomes 12–15 recorded by attempt 4 (44314aa1)
Exact context, term and type of this occurrence

Excerpt from Ordered provenance: from system to its field returns, and from the field to its type, the law.

Supply reading reads one of these occurrences as a proof of another:

Lean source (39 lines)

Lean source file: ReturnMap.lean

structure ReturnMap where
  Source : Type
  Target : Type
  send : Source → Target
  back : Target → Source
  returns : ∀ x, back (send x) = x

example (system : ReturnMap) (unused : Nat) :
    ∀ x : system.Source, system.back (system.send x) = x :=
  system.returns

def unitToBool : ReturnMap where
  Source := Unit
  Target := Bool
  send := fun _ => false
  back := fun _ => ()
  returns := by
    intro x
    cases x
    rfl

example : unitToBool.back (unitToBool.send ()) = () := rfl

theorem reverse_trip_fails :
    unitToBool.send (unitToBool.back true) ≠ true := by
  change false ≠ true
  decide

theorem send_injective (system : ReturnMap) :
    ∀ a b : system.Source, system.send a = system.send b → a = b := by
  intro a b same
  calc
    a = system.back (system.send a) := (system.returns a).symm
    _ = system.back (system.send b) := congrArg system.back same
    _ = b := system.returns b

#print axioms unitToBool
#print axioms reverse_trip_fails
#print axioms send_injective

Relative to the captured environment, including its axioms, and the 3 entries and 1 frame listed, occurrence 2 is read as supplying a proof of the statement at occurrence 3.
Recorded axioms of the typing declaration: none recorded.
Occurrence 2 · First appeared in attempt 2 (8a6f7071), step 2 · Relation 1 from occurrence 1 · Projected field 5 · returns
Occurrence 3 · First appeared in attempt 3 (31895a57), step 3 · Relation 2 from occurrence 2 · Type of the previous occurrence
Outcome 8 recorded by attempt 4 (44314aa1): accepted · typing of occurrence 2.
Formation of occurrence 3: established as a proposition.
Whether the term uses each listed entry is not read here.
The statement is the type inferred for this term at the captured universe levels, not read from a source ascription or an enclosing application.
Formation rests on Outcome 11 recorded by attempt 4 (44314aa1): accepted; Outcome 13 recorded by attempt 4 (44314aa1): accepted.
Conditions: 3 ordered entries, 0 entered binders and 1 frame.
1. Context position 1 · Auxiliary entry, recorded kind auxDecl · _example
2. Context position 2 · Context entry, recorded kind default · system
3. Context position 3 · Context entry, recorded kind default · unused
1. Relation 1: projection
Exact condition entries, names and frames
1. Judgement group 1 · formation read from its accepted outcomes.
  These receipts concern one checked judgement in this capture, not independent confirmation. Each keeps its recorded outcome.
  1. Outcome 11 recorded by attempt 4 (44314aa1): accepted · type component · the same receipt also serves the target’s typing, one receipt in two roles
  2. Outcome 13 recorded by attempt 4 (44314aa1): accepted · logical root
  Exact submitted inferred type for this judgement

Excerpt from Supply reading: the field returns of system read as supplying a proof of the law, with one frame, the projection.

Read both panels from the top, as in Lesson 6. Exercises 7.3 and 7.4 ask what they say.

Exercises

Exercise 7.1. In the figure of system, which parts of the structure are labeled "carrier type"? What does the figure say about their elements?

Hint

Read the labels in the diagram, and the note under it.

Answer

system.Source and system.Target are labeled "carrier type"; send and back are drawn as arrows between them. The note under the diagram says: "Arrows show function types. Set frames show membership domains, with no coordinates, shape, size, or chosen elements." So the figure does not say that either type has elements. Both could be empty, and then the law holds with nothing to check.

Exercise 7.2. In the round-trip figure, where does the route start, which functions does it pass through, and what is its end compared with? Does the figure say anything about a round trip that starts in system.Target?

Hint

Read In scope first.

Answer

The route starts at x, which In scope lists as ∀ x : system.Source. It passes through send and then back, and its end, system.back(system.send(x)), is compared with x: "Compare the outputs of these map paths: they are required to agree."

Nothing in scope ranges over system.Target, so the figure says nothing about the opposite round trip, and the law does not give it. For example, let Source be Unit, a type with one value, and Target be Bool, with values false and true. Let send always return false, and back return the single unit value. The law holds, but starting from true, send (back true) = false. ReturnMap.lean builds this record as unitToBool and checks the failure at true.

Exercise 7.3. In the provenance and supply figures, which relations lead from system to the law, in order? Which occurrence is read as supplying a proof of which, and what is the one frame?

Answer

Two relations. "Projected field 5 · returns" leads from system, occurrence 1, to the field returns, occurrence 2. "Type of the previous occurrence" leads from the field to its type, the law, occurrence 3. The supply reading says that occurrence 2 is read as supplying a proof of the statement at occurrence 3, relative to "the 3 entries and 1 frames listed". The frame is "Relation 1: projection", taking the field out of system. So the proof of the law is the field returns of this system, as the source said.

Exercise 7.4. The supply reading lists unused among its entries. Does the proof use unused? What does the figure say about this?

Answer

The figure does not decide it: "Whether the term uses each listed entry is not read here." A listed entry is available, not necessarily used. The source answers the question: system.returns does not mention unused.

Explain the result

Try writing a short explanation without looking back. It should name the types and functions, state the law in the right direction, and say where its proof comes from.

A complete answer could be:

An existing system provides two types and functions between them. Its stored law says that sending a source input and then applying back returns that input. The law belongs to this record, and its proof is the record's field returns. It says nothing about the opposite round trip.

In the examples of these lessons, you could check each figure against its statement and against the checks Lean recorded. That is a claim about these examples only; the Reference says what is and is not established in general.