Higher Observational Type Theory: From Bridges to Fibrancy

Declared optional inputs. Chapter 60, Chapter 213. No later result may depend on this chapter.

Opening obstruction

Indexed bridges express heterogeneous relatedness but not transport. A higher observational construction must add fibrancy data without claiming a completed sound and normalizing calculus.

Development contract

Define the public Narya fragment used here: indexed bridges, the higher-coinductive predicate $\mathsf{isFibrant}(A)$, and its transport and lifting projections. Derive Paulin–Möhring $J$ with typal beta. Reconstruct the checked maps from a one-to-one fibrant relation to $\mathsf{isBisim}$, from $\mathsf{isBisim}$ to a bridge, from a Voevodsky equivalence to a bridge, and $\mathsf{bisim}\mathsf{\_}\mathsf{of}\mathsf{\_}\mathsf{Id}:\mathsf{Br}\mathsf{Fib}AB\to \mathsf{isBisim}(A,B)$; no round-trip equivalence is claimed. The pinned artifact checks these maps, while safe semantics, normalization, and a closed fibrant universe remain conjectural.