{-# OPTIONS --erased-cubical --safe --no-sized-types --no-guardedness #-}

module Agda.Builtin.Cubical.HCompU where

open import Agda.Primitive
open import Agda.Builtin.Sigma
open import Agda.Primitive.Cubical renaming (primINeg to ~_; primIMax to _∨_; primIMin to _∧_;
                                             primHComp to hcomp; primTransp to transp; primComp to comp;
                                             itIsOne to 1=1)
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Cubical.Sub renaming (Sub to _[_↦_]; primSubOut to outS; inc to inS)

module Helpers where
    -- Homogeneous filling
    hfill :  {} {A : Set } {φ : I}
              (u :  i  Partial φ A)
              (u0 : A [ φ  u i0 ]) (i : I)  A
    hfill {φ = φ} u u0 i =
      hcomp  j  \ { (φ = i1)  u (i  j) 1=1
                     ; (i = i0)  outS u0 })
            (outS u0)

    -- Heterogeneous filling defined using comp
    fill :  { : I  Level} (A :  i  Set ( i)) {φ : I}
             (u :  i  Partial φ (A i))
             (u0 : A i0 [ φ  u i0 ]) 
              i   A i
    fill A {φ = φ} u u0 i =
      comp  j  A (i  j))
            j  \ { (φ = i1)  u (i  j) 1=1
                    ; (i = i0)  outS u0 })
           (outS {φ = φ} u0)

    module _ {} {A : Set } where
      refl : {x : A}  x  x
      refl {x = x} = λ _  x

      sym : {x y : A}  x  y  y  x
      sym p = λ i  p (~ i)

      cong :  {ℓ'} {B : A  Set ℓ'} {x y : A}
             (f : (a : A)  B a) (p : x  y)
            PathP  i  B (p i)) (f x) (f y)
      cong f p = λ i  f (p i)

    isContr :  {}  Set   Set 
    isContr A = Σ A \ x  (∀ y  x  y)

    fiber :  { ℓ'} {A : Set } {B : Set ℓ'} (f : A  B) (y : B)  Set (  ℓ')
    fiber {A = A} f y = Σ A \ x  f x  y

open Helpers

primitive
  prim^glueU : {la : Level} {φ : I} {T : I  Partial φ (Set la)}
                 {A : Set la [ φ  T i0 ]} 
                 PartialP φ (T i1)  outS A  hcomp T (outS A)
  prim^unglueU : {la : Level} {φ : I} {T : I  Partial φ (Set la)}
                   {A : Set la [ φ  T i0 ]} 
                   hcomp T (outS A)  outS A
  -- Needed for transp.
  primFaceForall : (I  I)  I

transpProof :  {l}  (e : I  Set l)  (φ : I)  (a : Partial φ (e i0))  (b : e i1 [ φ  (\ o  transp (\ i  e i) i0 (a o)) ] )  fiber (transp (\ i  e i) i0) (outS b)
transpProof e φ a b = f , \ j  comp (\ i  e i) (\ i 
                                               \ { (φ = i1)  transp (\ j  e (j  i)) (~ i) (a 1=1)
                                                 ; (j = i0)  transp (\ j  e (j  i)) (~ i) f
                                                 ; (j = i1)  g (~ i) })
                                        f
    where
      b' = outS {u = (\ o  transp (\ i  e i) i0 (a o))} b
      g : (k : I)  e (~ k)
      g k = fill (\ i  e (~ i)) (\ i  \ { (φ = i1)  transp (\ j  e (j  ~ i)) i (a 1=1)
                                          ; (φ = i0)  transp (\ j  e (~ j  ~ i)) (~ i) b' }) (inS b') k
      f = comp (\ i  e (~ i)) (\ i  \ { (φ = i1)  transp (\ j  e (j  ~ i)) i (a 1=1); (φ = i0)  transp (\ j  e (~ j  ~ i)) (~ i) b' }) b'

{-# BUILTIN TRANSPPROOF transpProof #-}