open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

module Prim.HCompU where

Primitive: Composition for universesπŸ”—

This module binds the operations prim^glueU and prim^unglueU, which expose the fibrancy structure of the universe as being a Glue-like type former. Additionally, we prove extend-transp-fibre, which is used internally for composition in the universe.

primitive
  prim^glueU
    : {β„“ : Level} {Ο† : I} {T : I β†’ Partial Ο† (Type β„“)}
      {A : Type β„“ [ Ο† ↦ T i0 ]}
    β†’ PartialP Ο† (T i1) β†’ outS A β†’ primHComp T (outS A)

  prim^unglueU
    : {β„“ : Level} {Ο† : I} {T : I β†’ Partial Ο† (Type β„“)}
      {A : Type β„“ [ Ο† ↦ T i0 ]}
    β†’ primHComp T (outS A) β†’ outS A

  -- Needed for transp.
  primFaceForall : (I β†’ I) β†’ I

extend-transp-fibre
  : βˆ€ {l} (e : I β†’ Type l) (Ο† : I)
    (a : Partial Ο† (e i0))
    (b : e i1 [ Ο† ↦ (Ξ» o β†’ transp e i0 (a o)) ])
  β†’ fibre (transp e i0) (outS b)
extend-transp-fibre e Ο† a b = _ , Ξ» j β†’
  comp e (Ο† ∨ βˆ‚ j) Ξ» where
    i (Ο† = i1) β†’ coe0β†’i e i (a 1=1)
    i (j = i0) β†’ coe0β†’i e i (g i1)
    i (j = i1) β†’ g (~ i)
    i (i = i0) β†’ g i1
  where
    g : βˆ€ i β†’ e (~ i)
    g k = fill (Ξ» i β†’ e (~ i)) (βˆ‚ Ο†) k Ξ» where
      i (Ο† = i1) β†’ coe0β†’i e (~ i) (a 1=1)
      i (Ο† = i0) β†’ coe1β†’i e (~ i) (outS b)
      i (i = i0) β†’ outS b

{-# BUILTIN TRANSPPROOF extend-transp-fibre #-}