From asi
Validates covariant fibrations for dependent types in directed type theory, computes cocartesian lifts, generates transport terms, and checks Segal conditions.
npx claudepluginhub plurigrid/asi --plugin asiThis skill uses the workspace's default tool permissions.
**Status**: ✅ Production Ready
Defines dependent Yoneda lemma in Rzk as directed path induction for Segal types in directed HoTT, per Riehl-Shulman. Provides chemical semantics, GF(3) triads, and theorem proofs. Useful for synthetic ∞-categories.
Guides Next.js Cache Components and Partial Prerendering (PPR) with cacheComponents enabled. Implements 'use cache', cacheLife(), cacheTag(), revalidateTag(), static/dynamic optimization, and cache debugging.
Guides building MCP servers enabling LLMs to interact with external services via tools. Covers best practices, TypeScript/Node (MCP SDK), Python (FastMCP).
Share bugs, ideas, or general feedback.
Status: ✅ Production Ready Trit: -1 (MINUS - validator/constraint) Color: #2626D8 (Blue) Principle: Type families respect directed morphisms Frame: Covariant transport along 2-arrows
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 𝟚.
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
-- 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'
-- 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
-- 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̃)
-- 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
# 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
covariant-fibrations (-1) ⊗ directed-interval (0) ⊗ synthetic-adjunctions (+1) = 0 ✓ [Transport]
covariant-fibrations (-1) ⊗ elements-infinity-cats (0) ⊗ rezk-types (+1) = 0 ✓ [∞-Fibrations]
Skill Name: covariant-fibrations Type: Directed Transport Validator Trit: -1 (MINUS) Color: #2626D8 (Blue)
This skill connects to the K-Dense-AI/claude-scientific-skills ecosystem:
homotopy-theory: 29 citations in bib.duckdbThis skill maps to Cat# = Comod(P) as a bicomodule in the equipment structure:
Trit: 0 (ERGODIC)
Home: Prof
Poly Op: ⊗
Kan Role: Adj
Color: #26D826
The skill participates in triads satisfying:
(-1) + (0) + (+1) ≡ 0 (mod 3)
This ensures compositional coherence in the Cat# equipment structure.