```----------------------------------------------------------------------
-- 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/
----------------------------------------------------------------------

module Data.functions where

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

----------------------------------------------------------------------
-- Dependent functions
----------------------------------------------------------------------
Π' : {Γ : Set}(A : Γ → Set)(B : (Σ x ∈ Γ , A x) → Set) → Γ → Set
Π' A B x = (a : A x) → B (x , a)

FibΠ :
{Γ : Set}
{A : Γ → Set}
{B : (Σ x ∈ Γ , A x) → Set}
(α : Fib A)
(β : Fib B)
→ -----------
Fib (Π' A B)
FibΠ {Γ} {A} {B} α β e p φ f g = (g₁ , extends) where
pₐ : (a : A (p ⟨ ! e ⟩)) → Π (A ∘ p)
pₐ a = fst (fill {A = A} (! e) α p cofFalse ∅-elim a (λ u → ∅-elim u))
pₐI≡a : (a : A (p ⟨ ! e ⟩)) → pₐ a ⟨ ! e ⟩ ≡ a
pₐI≡a a = snd (snd (fill {A = A} (! e) α p cofFalse ∅-elim a (λ u → ∅-elim u)))
q : (a : A (p ⟨ ! e ⟩)) → Int → Σ Γ A
q a i = (p i , pₐ a i)
f' : (a : A (p ⟨ ! e ⟩)) → [ φ ] → Π (B ∘ (q a))
f' a u i = f u i (pₐ a i)
b₀ : (a : A (p ⟨ ! e ⟩)) → ⟦ b ∈ (B (q a ⟨ e ⟩)) ∣ (φ , f' a) ∙ ⟨ e ⟩ ↗ b ⟧
b₀ a = (fst g (pₐ a ⟨ e ⟩) , (λ u → cong (λ f → f (pₐ a ⟨ e ⟩)) (snd g u)))
g₁ : (Π' A B) (p ⟨ ! e ⟩)
g₁ a = let b = fst (β e (q a) φ (f' a) (b₀ a)) in subst (λ a → B (p ⟨ ! e ⟩ , a)) (pₐI≡a a) b where
extends : prf ((φ , f) ∙ ⟨ ! e ⟩ ↗ g₁)
extends u = funext (λ a → substLemma (pₐI≡a a) (trans (f'I≡g₁ a) (fI≡f'I a))) where
substLemma : {a a' : A (p ⟨ ! e ⟩)}(eq : a' ≡ a){b : B (p ⟨ ! e ⟩ , a)}{b' : B (p ⟨ ! e ⟩ , a')}
→ subst (λ a → B (p ⟨ ! e ⟩ , a)) (symm eq) b ≡ b' → b ≡ subst (λ a → B (p ⟨ ! e ⟩ , a)) eq b'
substLemma refl refl = refl
f'I≡g₁ : (a : A (p ⟨ ! e ⟩)) → f' a u ⟨ ! e ⟩ ≡ fst (β e (q a) φ (f' a) (b₀ a))
f'I≡g₁ a = snd (β e (q a) φ (f' a) (b₀ a)) u
fI≡f'I : (a : A (p ⟨ ! e ⟩)) → subst (λ a₁ → B (p ⟨ ! e ⟩ , a₁)) (symm (pₐI≡a a)) (snd ((φ , f) ∙ ⟨ ! e ⟩) u a) ≡ f' a u ⟨ ! e ⟩
fI≡f'I a = congdep (λ a' → f u ⟨ ! e ⟩ a') (symm (pₐI≡a a))

Πext : {Γ : Set}{A : Γ → Set}{B : (Σ x ∈ Γ , A x) → Set}{x : Γ}{f g : Π' A B x} → ((a : A x) → f a ~ g a) → f ~ g
fst (Πext pointwise) i a = fst (pointwise a) i
fst (snd (Πext pointwise)) = funext (λ a → fst (snd (pointwise a)))
snd (snd (Πext pointwise)) = funext (λ a → snd (snd (pointwise a)))

```