home / skills / plurigrid / asi / covariant-fibrations

covariant-fibrations skill

safe

This skill helps you validate covariant fibrations and transport along directed intervals, ensuring correct type propagation in dependent type workflows.

npx playbooks add skill plurigrid/asi --skill covariant-fibrations

Review the files below or copy the command above to add this skill to your agents.

Files (2)

SKILL.md

3.1 KB

---
name: covariant-fibrations
description: Riehl-Shulman covariant fibrations for dependent types over directed
  intervals in synthetic ∞-categories.
license: UNLICENSED
metadata:
  trit: -1
  source: local
---

# Covariant Fibrations Skill: Directed Transport

**Status**: ✅ Production Ready
**Trit**: -1 (MINUS - validator/constraint)
**Color**: #2626D8 (Blue)
**Principle**: Type families respect directed morphisms
**Frame**: Covariant transport along 2-arrows

---

## Overview

**Covariant Fibrations** are type families B : A → U where transport goes *with* the direction of morphisms. In directed type theory, this ensures type families correctly propagate along the directed interval 𝟚.

1. **Directed interval 𝟚**: Type with 0 → 1 (not invertible)
2. **Covariant transport**: f : a → a' induces B(a) → B(a')
3. **Segal condition**: Composition witness for ∞-categories
4. **Fibration condition**: Lift existence (not uniqueness)

## Core Formula

```
For P : A → U covariant fibration:
  transport_P : (f : Hom_A(a, a')) → P(a) → P(a')
  
Covariance: transport respects composition
  transport_{g∘f} = transport_g ∘ transport_f
```

```haskell
-- Directed type theory (Narya-style)
covariant_fibration : (A : Type) → (P : A → Type) → Type
covariant_fibration A P = 
  (a a' : A) → (f : Hom A a a') → P a → P a'
```

## Key Concepts

### 1. Covariant Transport

```agda
-- Transport along directed morphisms
cov-transport : {A : Type} {P : A → Type} 
              → is-covariant P
              → {a a' : A} → Hom A a a' → P a → P a'
cov-transport cov f pa = cov.transport f pa

-- Functoriality
cov-comp : cov-transport (g ∘ f) ≡ cov-transport g ∘ cov-transport f
```

### 2. Cocartesian Lifts

```agda
-- Cocartesian lift characterizes covariant fibrations
is-cocartesian : {E B : Type} (p : E → B) 
               → {e : E} {b' : B} → Hom B (p e) b' → Type
is-cocartesian p {e} {b'} f = 
  Σ (e' : E), Σ (f̃ : Hom E e e'), (p f̃ ≡ f) × is-initial(f̃)
```

### 3. Segal Types with Covariance

```agda
-- Covariant families over Segal types
covariant-segal : (A : Segal) → (P : A → Type) → Type
covariant-segal A P = 
  (x y z : A) → (f : Hom x y) → (g : Hom y z) →
  cov-transport (g ∘ f) ≡ cov-transport g ∘ cov-transport f
```

## Commands

```bash
# Validate covariance conditions
just covariant-check fibration.rzk

# Compute cocartesian lifts
just cocartesian-lift base-morphism.rzk

# Generate transport terms
just cov-transport source target
```

## Integration with GF(3) Triads

```
covariant-fibrations (-1) ⊗ directed-interval (0) ⊗ synthetic-adjunctions (+1) = 0 ✓  [Transport]
covariant-fibrations (-1) ⊗ elements-infinity-cats (0) ⊗ rezk-types (+1) = 0 ✓  [∞-Fibrations]
```

## Related Skills

- **directed-interval** (0): Base directed type 𝟚
- **synthetic-adjunctions** (+1): Generate adjunctions from fibrations
- **segal-types** (-1): Validate Segal conditions

---

**Skill Name**: covariant-fibrations
**Type**: Directed Transport Validator
**Trit**: -1 (MINUS)
**Color**: #2626D8 (Blue)

Overview

This skill implements covariant fibrations: type families that transport along directed morphisms in synthetic ∞-categories. It verifies functorial, cocartesian-lift, and Segal-style conditions so dependent types respect the direction of the interval 𝟚. Use it to assert and compute directed transport and cocartesian lifts for dependent families over Segal or ∞-type bases.

How this skill works

The tool inspects a family P : A → Type and checks that for every arrow f : Hom_A(a,a') there is a transport map P(a) → P(a') that composes correctly. It verifies covariance by checking transport_{g∘f} = transport_g ∘ transport_f and searches for cocartesian lifts witnessing the fibration condition. Commands also produce explicit transport terms and can compute candidate lifts or counterexamples when conditions fail.

When to use it

When you need directed transport maps for dependent types over a directed interval or Segal-type base.
When proving a type family is a covariant fibration (functoriality and lift existence).
When constructing or checking cocartesian lifts for morphisms in a base category.
When validating Segal conditions in combination with covariance requirements.
When generating concrete transport terms or debugging covariance failures in models of synthetic ∞-categories.

Best practices

Model the base A as a Segal or properly compositional type to ensure composition checks are meaningful.
Provide explicit Hom witnesses for arrows and composition to make transport proofs constructive.
Prefer computing cocartesian lifts only when required; existence checks can be expensive in large contexts.
Use small, canonical representatives for P(a) when generating transport terms to keep outputs readable.
Combine with directed-interval tooling to validate noninvertibility and directionality assumptions.

Example use cases

Validate a dependent family P over a Segal type A satisfies covariant transport and composition laws.
Compute a cocartesian lift of a given base morphism to produce a transported element in the fiber.
Generate transport terms for proof scripts that require explicit P(a) → P(a') maps.
Debug why a candidate family fails covariance by isolating failing composition or lift cases.
Integrate covariance checks into a pipeline that builds synthetic adjunctions or ∞-fibrations.

FAQ

Does the skill require uniqueness of lifts?

No. The fibration condition enforces existence of cocartesian lifts, not uniqueness; initiality of the lift is checked when appropriate.

Can it handle noninvertible directed intervals like 𝟚?

Yes. The skill is designed for directed intervals with noninvertible arrows and ensures transport follows the forward direction.