open import 1Lab.Reflection.Univalence
open import 1Lab.Equiv.Fibrewise
open import 1Lab.Path.Cartesian
open import 1Lab.Type.Sigma
open import 1Lab.Univalence
open import 1Lab.Type.Pi
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

module 1Lab.Univalence.Fibrewise where

private variable
  β„“ β„“' β„“'' : Level
  A B X Y : Type β„“
  P Q : A β†’ Type β„“'

Univalence for type familiesπŸ”—

Any equivalence lets us compare type families and by forming the type of fibrewise equivalences between and A useful univalence-type result in this setting would be to show that equivalent type families are actually identical (over the path induced by and, indeed, we can prove this:

private module _ where private
  _ = comp

  ua-over : (e : A ≃ B) (e' : P ≃[ e ] Q) β†’ PathP (Ξ» i β†’ ua e i β†’ Type _) P Q
  ua-over e e' = ua→ λ a → ua (e' a (e .fst a) refl)

The trouble with this definition arises when we want to consider paths over it, since then we need to consider the precise definition of ua→ in terms of comp. Still, we can put together a function for showing that sections of and are identical:

  ua-over-pathp
    : (e : A ≃ B) (e' : P ≃[ e ] Q) {f : βˆ€ x β†’ P x} {g : βˆ€ x β†’ Q x}
    β†’ ((a : A) β†’ e' a _ refl .fst (f a) ≑ g (e .fst a))
    β†’ PathP (Ξ» i β†’ (x : ua e i) β†’ ua-over e e' i x) f g
  ua-over-pathp e e' {f} {g} p = funext-dep Ξ» {xβ‚€} {x₁} q i β†’
    comp (Ξ» j β†’ uaβ†’.filler {e = e} {Ξ» _ _ β†’ Type _} (Ξ» a β†’ ua (e' a (e .fst a) refl)) i j (q i)) (βˆ‚ i) Ξ» where
      k (k = i0) β†’ g (unglue (q i))
      k (i = i0) β†’ attach (βˆ‚ k) (Ξ» { (k = i0) β†’ _ ; (k = i1) β†’ _ }) (inS (p xβ‚€ (~ k)))
      k (i = i1) β†’ g x₁

For practical formalisation, we prefer to define ua-over directly as a glue type. In particular, in a context with and the type is equivalent to both (through the assumed equivalence over and (by the identity equivalence).

module _ {A B : Type β„“} {P : A β†’ Type β„“'} {Q : B β†’ Type β„“'} (e : A ≃ B) (e' : P ≃[ e ] Q) where
  ua-over : PathP (Ξ» i β†’ ua e i β†’ Type β„“') P Q
  ua-over i x = Glue (Q (unglue x)) Ξ» where
    (i = i0) β†’ P x , e' x _ refl
    (i = i1) β†’ Q x , id≃

We can then use the constructor for Glue types to put together a proof that a section of is identical to a section of when it commutes with the given equivalences.

  ua-over-pathp
    : βˆ€ {x : A} {y : B} (u : PathP (Ξ» i β†’ ua e i) x y) {x' : P x} {y' : Q y}
    β†’ e' x y (ua-pathpβ†’path e u) .fst x' ≑ y'
    β†’ PathP (Ξ» i β†’ ua-over i (u i)) x' y'
  ua-over-pathp u {x'} {y'} p i = attach (βˆ‚ i) (Ξ» { (i = i0) β†’ _ ; (i = i1) β†’ _}) (inS
    (hcomp (βˆ‚ i) Ξ» where
      j (j = i0) β†’ e' _ _ (Ξ» k β†’ unglue (u (i ∧ k))) .fst x'
      j (i = i0) β†’ e' _ _ refl .fst x'
      j (i = i1) β†’ p j))

We can also destruct a Glue type, which gives us a converse to the above.

  pathp-ua-over
    : βˆ€ {x : A} {y : B} (u : PathP (Ξ» i β†’ ua e i) x y) {x' : P x} {y' : Q y}
    β†’ PathP (Ξ» i β†’ ua-over i (u i)) x' y'
    β†’ e' x y (ua-pathpβ†’path e u) .fst x' ≑ y'
  pathp-ua-over u {x'} {y'} p i = comp (Ξ» j β†’ Q (unglue (u (~ i ∨ j)))) (βˆ‚ i) Ξ» where
    j (j = i0) β†’ e' _ _ (Ξ» k β†’ unglue (u (~ i ∧ k))) .fst x'
    j (i = i0) β†’ e' _ _ (Ξ» j β†’ unglue (u j)) .fst x'
    j (i = i1) β†’ unglue (p j)