CITATION.cff

# SPDX-License-Identifier: MPL-2.0
# SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
cff-version: 1.2.0
title: "echo-types: dependent fibres and indexed structured-loss models (Agda)"
message: "Please cite this software using the author and repository information below; no verified DOI is recorded."
type: software
authors:
  - given-names: Jonathan
    orcid: "https://orcid.org/0000-0002-3078-6652"
    family-names: Jewell
    email: j.d.a.jewell@open.ac.uk
repository-code: "https://github.com/hyperpolymath/echo-types"
url: "https://github.com/hyperpolymath/echo-types"
abstract: >
  Constructive Agda formalisation of fibre-based "structured loss"
  types. Defines Echo f y := Σ (x : A) , (f x ≡ y), shows it is
  definitionally the homotopy fibre (echo↔fib), and develops a
  preorder-indexed diagram with a pointwise mediator property,
  conditional function-level results, and scoped counterexamples
  for selected lossy encodings. The ordinary checked roots use
  --safe --without-K; separate Cubical and postulated presentations
  have distinct trust boundaries. Novelty and priority are unresolved.
  See docs/foundation.adoc for dated coverage and verification limits.
keywords:
  - agda
  - indexed family
  - homotopy fibre
  - structured loss
  - reindexing
  - formal methods
  - mechanised metatheory
license: MPL-2.0
preferred-citation:
  type: software
  title: "echo-types: dependent fibres and indexed structured-loss models (Agda)"
  authors:
    - given-names: Jonathan
      orcid: "https://orcid.org/0000-0002-3078-6652"
      family-names: Jewell
  url: "https://github.com/hyperpolymath/echo-types"
  year: 2026