----------------------------------------------------------------------
-- This Agda code is designed to accompany the paper "Axioms for
-- Modelling Cubical Type Theory in a Topos". It is currently a work
-- in progress and still includes postulates/holes in certain places.
-- It also needs some tidying up and possibily reorganisation.
--
-- The idea for getting an impredicative universe of propositions Ω
-- comes from Martin Escardo, more details can be found at:
--
--          http://www.cs.bham.ac.uk/~mhe/impredicativity/          
----------------------------------------------------------------------

{-# OPTIONS --rewriting #-}
module glueing where 

open import prelude
open import impredicative
open import interval
open import cof
open import fibrations
open import equivs
open import Data.paths

----------------------------------------------------------------------
-- Glueing
----------------------------------------------------------------------

res : (Γ : Set)(Φ : Γ  Cof)  Set
res Γ Φ = Σ x  Γ , [ Φ x ]

Glue :
  {Γ : Set}
  (Φ : Γ  Cof)
  (A : res Γ Φ  Set)
  (B : Γ  Set)
  (f : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
   ---------------
  Γ  Set
Glue Φ A B f x = Σ a  ((u : [ Φ x ])  A (x , u)) ,  b  (B x)  All u  [ Φ x ] , f x u (a u)  b 

glue :
  {Γ : Set}
  {Φ : Γ  Cof}
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (f : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
   ---------------
  (xu : res Γ Φ)  A xu  Glue Φ A B f (fst xu)
glue {Γ} {Φ} {A} {B} f (x , u) a = ((λ v  moveA v a) , (f x u a ,  v  cong (λ{(u , a)  f x u a}) (symm (moveMove v))))) where
  moveA : (v : [ Φ x ])  A (x , u)  A (x , v)
  moveA v = subst  v  A (x , v)) (eq (fst (Φ x)))
  moveMove : (v : [ Φ x ])  (u , a)  (v , moveA v a)
  moveMove v = Σext (eq (fst (Φ x))) refl

unglue :
  {Γ : Set}
  {Φ : Γ  Cof}
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (f : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
   ---------------
  (x : Γ)  Glue Φ A B f x  B x
unglue _ _ (_ , b , _) = b

unglueGlue :
  {Γ : Set}
  {Φ : Γ  Cof}
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (f : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
   ---------------
  (xu : res Γ Φ)  (unglue {Φ = Φ} f (fst xu))  (glue {Φ = Φ} f xu)  f (fst xu) (snd xu)
unglueGlue f (x , u) = funext  a  refl)

glue' :
  {Γ : Set}
  {Φ : Γ  Cof}
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (f : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
   ---------------
  (x : Γ)  (a : (u : [ Φ x ])  A (x , u))   b  B x  all [ Φ x ]  u  f x u (a u)  b)   Glue Φ A B f x
glue' f x a (b , bPrf) = (a , b , bPrf)

unglueGlue' :
  {Γ : Set}
  {Φ : Γ  Cof}
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (f : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
   ---------------
  (x : Γ)  (a : (u : [ Φ x ])  A (x , u))
    (unglue {Φ = Φ} f x)  (glue' {Φ = Φ} f x a)  fst
unglueGlue' f x a = refl

glueUnglue :
  {Γ : Set}
  {Φ : Γ  Cof}
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (f : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
   ---------------
  (x : Γ)  (g : Glue Φ A B f x)
    glue' {Φ = Φ} f x (fst g) (unglue {Φ = Φ} f x g , snd (snd g))  g
glueUnglue f x g = refl

helper : {A : Set}{a a' : A}(p : a'  a)(p' : a' ~ a)(eq : reflPath' p  p')(i : Int)  a  fst p' i
helper {A} {a} .{a} refl p' eq i = subst  p'  a  fst p' i) eq refl

helper' : {A : Set}{B : Set}{a a' : A}{b : B}(f : A  B)(p : a  a')(q : f a  b)(r : f a'  b)
  subst  x  f x ~ b) p (reflPath' q)  reflPath' r
helper' _ refl refl refl = refl

glueExt :
  {Γ : Set}
  {Φ : Γ  Cof}
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (f : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
  {x : Γ}
  (g g' : Glue Φ A B f x)
  (p : fst g  fst g')
  (q : fst (snd g)  fst (snd g'))
   ---------------
  g  g'
glueExt _ (_ , _ , fa≡b) (_ , _ , fa≡b') refl refl =
  Σext refl (Σext refl (funext  u  uip (fa≡b u) (fa≡b' u))))

helper'' :
  {A : Set}
  (a a' : A)
  (p : a  a')
  {B : A  Set}
  {C : A  Set}
  (f : (x : A)  B x  C x)
  (b : B a)
  (q : b  b)  f a' (subst B p b)  subst C p (f a b)
helper'' _ _ refl _ _ refl = refl

fextunglue :
  {Γ : Set}
  {Φ : Γ  Cof}
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (f : (x : Γ)(v : [ Φ x ])  A (x , v)  B x)
   -------------
  (x : Γ)  ((v : [ Φ x ])  Fext (f x v))  Fib B  Fext (unglue {Φ = Φ} f x)
fextunglue {Γ} {Φ} {A} {B} f x fext β b ψ q = ((g , gPath) ,  u  Σext (extendsQ u) (extendsQ' u))) where
  qa : (v : [ Φ x ])   qa  ((u : [ ψ ])  A (x , v))  (ψ , f x v  qa)  b 
  fst (qa v) u = fst (fst q u) v
  snd (qa v) u = trans (snd q u) (snd (snd (fst q u)) v)
  a : (v : [ Φ x ])  A (x , v)
  a v = fst (fst (fext v b ψ (qa v)))
  fa≡b : (v : [ Φ x ])  [ ψ ]  f x v (a v)  b
  fa≡b v u =
   let step1 = cong (f x v) (symm (Σeq₁ (snd (fext v b ψ (qa v)) u)))
       step2 = snd (snd (fst q u)) v
   in trans (snd q u) (trans step2 step1)
  h : (v : [ Φ x ])  (f x v (a v)) ~ b
  h v = snd (fst (fext v b ψ (qa v)))
  qb : [ ψ  Φ x ]  Π  _  B x)
  qb = _∪_ {φ = ψ} {ψ = Φ x}  _ _  b)  v  fst (h v)) {p = agree} where
    agree : prf ((ψ ,  _ _  b))  (Φ x ,  v  fst (h v))))
    agree u v = funext  i 
      let rr = snd (fext v b ψ (qa v)) u in
      let ss = helper' (f x v) (Σeq₁ rr) ((trans (snd q u) (snd (snd (fst q u)) v))) (fa≡b v u) in
      helper (fa≡b v u) (h v) (trans (Σeq₂ rr) (symm ss)) i)
  pbRaw :  p  (Int  B x)  (((ψ  Φ x) , qb)  p) & (p I  b) 
  pbRaw = fill I' β  _  x) (ψ  Φ x) qb b  uv  or-elim-eq  u  qb u I) b refl rightEq uv) where
    rightEq : {v : [ Φ x ]}  qb  inr v  I  b
    rightEq {v} = snd (snd (snd (fst (fext v b ψ (qa v)))))
  pb : Int  B x
  pb = fst (pbRaw)
  fa≡pbO : (v : [ Φ x ])  f x v (a v)  pb O
  fa≡pbO v = trans step2 step1 where
    step1 : f x v (a v)  fst (h v) O
    step1 = symm (fst (snd (snd (fst (fext v b ψ (qa v))))))
    step2 : fst (h v) O  pb O
    step2 = cong  p  p O) (fst (snd pbRaw)  inr v )
  g : Glue Φ A B f x
  g = (a , pb O , fa≡pbO)
  gPath : pb O ~ b
  fst gPath = pb
  fst (snd gPath) = refl
  snd (snd gPath) = snd (snd pbRaw)
  extendsQ : (u : [ ψ ])   fst q u  g
  extendsQ u = glueExt {Φ = Φ} f (fst q u) g fstEq sndEq where
    fstEq : fst (fst q u)  a
    fstEq = funext  v  Σeq₁ (snd (fext v b ψ (qa v)) u))
    sndEq : fst (snd (fst q u))  pb O
    sndEq = trans (cong  p  p O) (fst (snd pbRaw)  inl u )) (snd q u)
  extendsQ' :  (u : [ ψ ])  subst  v  unglue {Φ = Φ} f x v ~ b) (extendsQ u)
    (reflPath' (snd q u))  gPath
  extendsQ' u = PathExt (funext  i  trans (b≡pbi i) (trans (rp≡b i) (substrp=rp i)))) where
    b≡pbi : (i : Int)  b  pb i
    b≡pbi i = cong  p  p i) (fst (snd pbRaw)  inl u )
    rp≡b : (i : Int)  fst (reflPath' (snd q u)) i  b --reflPath' (snd q u)
    rp≡b i = reflPathEval (snd q u) i
    fstSubst : {g g' : Glue Φ A B f x}(p : g  g'){q : unglue {Φ = Φ} f x g ~ b}
       fst (subst  g  unglue {Φ = Φ} f x g ~ b) p q)  fst q
    fstSubst refl = refl
    substrp=rp : (i : Int)  fst (subst  g  unglue {Φ = Φ} f x g ~ b) (extendsQ u)
      (reflPath' (snd q u))) i  fst (reflPath' (snd q u)) i
    substrp=rp i = cong  p  p i) (fstSubst (extendsQ u))

FibGlue :
  {Γ : Set}
  {Φ : Γ  Cof}
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (f : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
  (equiv : (x : Γ)(v : [ Φ x ])  Equiv (f x v))
   ---------------
  Fib A  Fib B  Fib (Glue Φ A B f)
FibGlue {Γ} {Φ} {A} {B} f equiv α β = fext2fib fext2 β where
  B' : res Γ Φ  Set
  B' (x , v) = B x
  β' : Fib B'
  β' e p ψ q b = β e (fst  p) ψ q b
  fext1 : (x : Γ)(v : [ Φ x ])  Fext (f x v)
  fext1 x v = equiv2fext α β' (λ{(x , v)  f x v}) (x , v) (equiv x v)
  fext2 : (x : Γ)  Fext (unglue {Φ = Φ} f x)
  fext2 x = fextunglue {Φ = Φ} f x (fext1 x) β

----------------------------------------------------------------------
-- Strictifying
----------------------------------------------------------------------
record _≅'_(A B : Set) : Set where
 field
  f : A  B
  g : B  A
  inv₁ : g  f  id
  inv₂ : f  g  id

postulate
 reIm :
  (φ : Cof)
  (A : [ φ ]  Set)
  (B : Set)
  (m : (u : [ φ ])  A u ≅' B)
  -> ----------------------
  Σ B'  Set , Σ m'  B' ≅' B , ((u : [ φ ])  (A u , m u)  (B' , m'))

strictify :
  {Γ : Set}
  (Φ : Γ  Cof)
  (A : res Γ Φ  Set)
  (B : Γ  Set)
  (m : (x : Γ)(u : [ Φ x ])  A (x , u) ≅' B x)
  -> ----------------------
  Γ  Set
strictify Φ A B m x = fst (reIm (Φ x)(λ u  A (x , u)) (B x) (m x))

isoB :
  {Γ : Set}
  (Φ : Γ  Cof)
  (A : res Γ Φ  Set)
  (B : Γ  Set)
  (m : (x : Γ)(u : [ Φ x ])  A (x , u) ≅' B x)
  (x : Γ)
  -> ----------------------
  strictify Φ A B m x ≅' B x
isoB Φ A B m x = fst (snd (reIm (Φ x)(λ u  A (x , u)) (B x) (m x)))
  
restrictsToA :
  {Γ : Set}
  (Φ : Γ  Cof)
  (A : res Γ Φ  Set)
  (B : Γ  Set)
  (m : (x : Γ)(u : [ Φ x ])  A (x , u) ≅' B x)
  (x : res Γ Φ)
  -> ----------------------
  A x  strictify Φ A B m (fst x)
restrictsToA Φ A B m (x , u) = Σeq₁ (snd (snd (reIm (Φ x)(λ u  A (x , u)) (B x) (m x))) u)
  
restrictsToM :
  {Γ : Set}
  (Φ : Γ  Cof)
  (A : res Γ Φ  Set)
  (B : Γ  Set)
  (m : (x : Γ)(u : [ Φ x ])  A (x , u) ≅' B x)
  (x : Γ)
  (u : [ Φ x ])
  -> ----------------------
  (A (x , u) , m x u)  (strictify Φ A B m x , isoB Φ A B m x)
restrictsToM Φ A B m x u = snd (snd (reIm (Φ x)(λ u  A (x , u)) (B x) (m x))) u

----------------------------------------------------------------------
-- Strict glueing
----------------------------------------------------------------------
SGlue :
  {Γ : Set}
  (Φ : Γ  Cof)
  (A : res Γ Φ  Set)
  (B : Γ  Set)
  (f : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
   ---------------
  Γ  Set

private
 fIso :
  {Γ : Set}
  (Φ : Γ  Cof)
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (w : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
   ---------------
  (x : Γ) (u : [ Φ x ])  A (x , u) ≅' Glue Φ A B w x
abstract
 fIso Φ {A} {B} w x u = iso where
  open _≅'_
  prfIr : {a : A (x , u)}  subst  v  A (x , v)) (equ (fst (Φ x)) u u) a  a
  prfIr {a} =
    let switch = uip (equ (fst (Φ x)) u u) refl in
    cong  p  subst  v  A (x , v)) p a) switch
  iso : A (x , u) ≅' Glue Φ A B w x
  f iso a = glue {Φ = Φ} w (x , u) a
  g iso (a , _ , _) = a u
  inv₁ iso = funext  a  prfIr)
  inv₂ iso = funext fg≡id where
    parEq : {a a' : (u : [ Φ x ])  A (x , u)}  a u  a' u  a  a'
    parEq {a} {a'} eq = funext  v  subst  v  a v  a' v) (equ (fst (Φ x)) u v) eq)
    fg≡id : (gl : Glue Φ A B w x)  (glue {Φ = Φ} w (x , u) (fst gl u))  gl
    fg≡id gl = glueExt {Φ = Φ} w (glue {Φ = Φ} w (x , u) (fst gl u)) gl fstEq sndEq where
      fstEq : fst (glue {Φ = Φ} w (x , u) (fst gl u))  fst gl
      fstEq = parEq prfIr
      sndEq : w x u (fst gl u)  fst (snd gl)
      sndEq = snd (snd gl) u
  
SGlue {Γ} Φ A B w = strictify Φ A (Glue Φ A B w) (fIso Φ w)

sglue :
  {Γ : Set}
  {Φ : Γ  Cof}
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (w : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
   ---------------
  (xu : res Γ Φ)  A xu  SGlue Φ A B w (fst xu)
abstract
 sglue {Γ} {Φ} {A} {B} w (x , u) = (_≅'_.g iso)  glue {Φ = Φ} w (x , u) where
  iso : SGlue Φ A B w x ≅' Glue Φ A B w x
  iso = isoB Φ A (Glue Φ A B w) (fIso Φ w) x

sunglue :
  {Γ : Set}
  {Φ : Γ  Cof}
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (w : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
   ---------------
  (x : Γ)  SGlue Φ A B w x  B x
abstract
 sunglue {Γ} {Φ} {A} {B} w x = (unglue {Φ = Φ} w x)  _≅'_.f iso where
  iso : SGlue Φ A B w x ≅' Glue Φ A B w x
  iso = isoB Φ A (Glue Φ A B w) (fIso Φ w) x

FibSGlue :
  {Γ : Set}
  {Φ : Γ  Cof}
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (f : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
  (equiv : (x : Γ)(v : [ Φ x ])  Equiv (f x v))
   ---------------
  Fib A  Fib B  Fib (SGlue Φ A B f)
abstract
 FibSGlue {Γ} {Φ} {A} {B} f equiv α β =
  FibIso (Glue Φ A B f) (SGlue Φ A B f) iso (FibGlue {Φ = Φ} f equiv α β) where
    iso : Glue Φ A B f  SGlue Φ A B f
    iso x = (_≅'_.g iso' , _≅'_.f iso' , (_≅'_.inv₂ iso' , _≅'_.inv₁ iso')) where
      iso' : SGlue Φ A B f x ≅' Glue Φ A B f x
      iso' = isoB Φ A (Glue Φ A B f) (fIso Φ f) x

strictness :
  {Γ : Set}
  (Φ : Γ  Cof)
  (A : res Γ Φ  Set)
  (B : Γ  Set)
  (f : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
  (x : Γ)
  (u : [ Φ x ])
   ---------------
  SGlue Φ A B f x  A (x , u)
abstract
 strictness Φ A B f x u = symm (restrictsToA Φ A (Glue Φ A B f) (fIso Φ f) (x , u))

str :
  {Γ : Set}
  {Φ : Γ  Cof}
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (f : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
  (x : Γ)
   ---------------
  Glue Φ A B f x  SGlue Φ A B f x
abstract
 str {Γ} {Φ} {A} {B} f x = _≅'_.g (isoB Φ A (Glue Φ A B f) (fIso Φ f) x)

unstr :
  {Γ : Set}
  {Φ : Γ  Cof}
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (f : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
  (x : Γ)
   ---------------
  SGlue Φ A B f x  Glue Φ A B f x
abstract
 unstr {Γ} {Φ} {A} {B} f x = _≅'_.f (isoB Φ A (Glue Φ A B f) (fIso Φ f) x)

strIsUnglue :
  {Γ : Set}
  {Φ : Γ  Cof}
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (f : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
  (x : Γ)
  (u : [ Φ x ])
   ---------------
  (g : Glue Φ A B f x)  str {Γ} {Φ} {A} {B} f x g  coe (symm (strictness Φ A B f x u)) (fst g u)
abstract
 strIsUnglue {Γ} {Φ} {A} {B} f x u g = inner (restrictsToM Φ A (Glue Φ A B f) (fIso Φ f) x u) g where
  inner : {Am Gs : Σ X  Set , X ≅' Glue Φ A B f x}(eq : Am  Gs)(g : Glue Φ A B f x)  _≅'_.g (snd Gs) g  coe (symm (symm (Σeq₁ eq))) (_≅'_.g (snd Am) g)
  inner refl b = refl

unstrStr :
  {Γ : Set}
  {Φ : Γ  Cof}
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (f : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
  (x : Γ)
   ---------------
  (unstr {Γ} {Φ} {A} {B} f x)  (str {Γ} {Φ} {A} {B} f x)  id
abstract
 unstrStr {Γ} {Φ} {A} {B} f x = _≅'_.inv₂ (isoB Φ A (Glue Φ A B f) (fIso Φ f) x)

strUnstr :
  {Γ : Set}
  {Φ : Γ  Cof}
  {A : res Γ Φ  Set}
  {B : Γ  Set}
  (f : (x : Γ)(u : [ Φ x ])  A (x , u)  B x)
  (x : Γ)
   ---------------
  (str {Γ} {Φ} {A} {B} f x)  (unstr {Γ} {Φ} {A} {B} f x)  id
abstract
 strUnstr {Γ} {Φ} {A} {B} f x = _≅'_.inv₁ (isoB Φ A (Glue Φ A B f) (fIso Φ f) x)