joins-two-branches-nothing-tells-apart.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# Two branches nothing tells apart are the answer themselves: there is nothing
# to pick between them, so the join mints no symbol at all and the firing
# answers the very term both of them are. A fork is a branch point in the
# program and not necessarily one in the value it stands for.
symbolic: |
  - λ: L_fork
    morph:
      𝑛1: $.a
      𝑛2: $.b
    join:
      𝑛3: [𝑛1, 𝑛2]
    𝑛: 𝑛3
location: 'Q.y'
input: '⟦ y ↦ ⟦ a ↦ ⟦ l ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, b ↦ ⟦ l ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, λ ⤍ L_fork ⟧.l ⟧'
result: '𝜎1:λ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝑛1·1 := 𝜎1:λ:l  # 𝕄(ξ.a)
      𝑛2·1 := 𝜎1:λ:l  # 𝕄(ξ.b)
      𝑛3·1 := 𝜎1:λ:l  # [𝑛1, 𝑛2]
      𝑛·1·1 := 𝜎1:λ:l  # 𝑛
      𝑛·1·2 := 𝜎1:λ:l  # 𝕄(𝑛·1·1)