This file needs reorganization and clean-up.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module UF-Base where

open import SpartanMLTT

Nat : {X : 𝓀 Μ‡ } β†’ (X β†’ π“₯ Μ‡ ) β†’ (X β†’ 𝓦 Μ‡ ) β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
Nat A B = Ξ  \x β†’ A x β†’ B x

Nats-are-natural : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ ) (Ο„ : Nat A B)
                 β†’ {x y : X} (p : x ≑ y) β†’ Ο„ y ∘ transport A p ≑ transport B p ∘ Ο„ x
Nats-are-natural A B Ο„ refl = refl

NatΞ£ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ } β†’ Nat A B β†’ Ξ£ A β†’ Ξ£ B
NatΞ£ ΞΆ (x , a) = (x , ΞΆ x a)

NatΞ  : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ } β†’ Nat A B β†’ Ξ  A β†’ Ξ  B
NatΞ  f g x = f x (g x) -- (S combinator from combinatory logic!)

Ξ Ξ£-distr : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {P : (x : X) β†’ A x β†’ 𝓦 Μ‡ }
         β†’ (Ξ  \(x : X) β†’ Ξ£ \(a : A x) β†’ P x a) β†’ Ξ£ \(f : Ξ  A) β†’ Ξ  \(x : X) β†’ P x (f x)
Ξ Ξ£-distr Ο† = (Ξ» x β†’ pr₁ (Ο† x)) , Ξ» x β†’ prβ‚‚ (Ο† x)

Ξ Ξ£-distr-back : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {P : (x : X) β†’ A x β†’ 𝓦 Μ‡ }
              β†’ (Ξ£ \(f : Ξ  A) β†’ Ξ  \(x : X) β†’ P x (f x)) β†’ Ξ  \(x : X) β†’ Ξ£ \(a : A x) β†’ P x a
Ξ Ξ£-distr-back (f , Ο†) x = f x , Ο† x

left-cancellable : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
left-cancellable f = βˆ€ {x x'} β†’ f x ≑ f x' β†’ x ≑ x'

left-cancellable' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
left-cancellable' f = βˆ€ x x' β†’ f x ≑ f x' β†’ x ≑ x'

_β‰ˆ_ : {X : 𝓀 Μ‡ } {x : X} {A : X β†’ π“₯ Μ‡ } β†’ Nat (Id x) A β†’ Nat (Id x) A β†’ 𝓀 βŠ” π“₯ Μ‡
Ξ· β‰ˆ ΞΈ = βˆ€ y β†’ Ξ· y ∼ ΞΈ y

ap-const : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (y : Y) {x x' : X} (p : x ≑ x') β†’ ap (Ξ» _ β†’ y) p ≑ refl
ap-const y refl = refl

transportβ‚‚ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (A : X β†’ Y β†’ 𝓦 Μ‡ )
             {x x' : X} {y y' : Y}
          β†’ x ≑ x' β†’ y ≑ y' β†’ A x y β†’ A x' y'
transportβ‚‚ A refl refl = id

back-transportβ‚‚ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (A : X β†’ Y β†’ 𝓦 Μ‡ )
                  {x x' : X} {y y' : Y}
               β†’ x ≑ x' β†’ y ≑ y' β†’ A x' y' β†’ A x y
back-transportβ‚‚ A refl refl = id

Idtofun : {X Y : 𝓀 Μ‡ } β†’ X ≑ Y β†’ X β†’ Y
Idtofun = transport id

back-Idtofun : {X Y : 𝓀 Μ‡ } β†’ X ≑ Y β†’ Y β†’ X
back-Idtofun = back-transport id

forth-and-back-transport : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {x y : X} {a : A x}
                         β†’ (p : x ≑ y) β†’ back-transport A p (transport A p a) ≑ a
forth-and-back-transport refl = refl

back-and-forth-transport : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {x y : X} {a : A x}
                         β†’ (p : y ≑ x) β†’ transport A p (back-transport A p a) ≑ a
back-and-forth-transport refl = refl

back-transport-is-pre-comp : {X X' : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (p : X ≑ X') (g : X' β†’ Y)
                          β†’ back-transport (Ξ» - β†’ - β†’ Y) p g ≑ g ∘ Idtofun p
back-transport-is-pre-comp refl g = refl

transport-is-pre-comp : {X X' : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (p : X ≑ X') (g : X β†’ Y)
                      β†’ transport (Ξ» - β†’ - β†’ Y) p g ≑ g ∘ Idtofun (p ⁻¹)
transport-is-pre-comp refl g = refl

trans-sym : {X : 𝓀 Μ‡ } {x y : X} (r : x ≑ y) β†’ r ⁻¹ βˆ™ r ≑ refl
trans-sym refl = refl

trans-sym' : {X : 𝓀 Μ‡ } {x y : X} (r : x ≑ y) β†’ r βˆ™ r ⁻¹ ≑ refl
trans-sym' refl = refl

transport-Γ— : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ )
                {x y : X} {c : A x Γ— B x} (p : x ≑ y)
            β†’ transport (Ξ» x β†’ A x Γ— B x) p c
            ≑ (transport A p (pr₁ c) , transport B p (prβ‚‚ c))
transport-Γ— A B refl = refl

transport-comp : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
                   {x y z : X} (q : x ≑ y) (p : y ≑ z) {a : A x}
               β†’ transport A  (q βˆ™ p) a ≑ transport A p (transport A q a)
transport-comp A refl refl = refl

transport-comp' : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
                  {x y z : X} (q : x ≑ y) (p : y ≑ z)
                β†’ transport A  (q βˆ™ p) ≑ transport A p ∘ transport A q
transport-comp' A refl refl = refl

transport-ap : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (A : Y β†’ 𝓦 Μ‡ )
               (f : X β†’ Y) {x x' : X} (p : x ≑ x') {a : A(f x)}
             β†’ transport (A ∘ f) p a ≑ transport A (ap f p) a
transport-ap A f refl = refl

transport-ap' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (A : Y β†’ 𝓦 Μ‡ )
                (f : X β†’ Y) {x x' : X} (p : x ≑ x') {a : A(f x)}
              β†’ transport (A ∘ f) p ≑ transport A (ap f p)
transport-ap' A f refl = refl

nat-transport : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ }
                (f : Nat A B) {x y : X} (p : x ≑ y) {a : A x}
              β†’ f y (transport A p a) ≑ transport B p (f x a)
nat-transport f refl = refl

transport-fam : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } (P : {x : X} β†’ Y x β†’ 𝓦 Μ‡ )
               (x : X) (y : Y x) β†’ P y β†’ (x' : X) (r : x ≑ x') β†’ P(transport Y r y)
transport-fam P x y p .x refl = p

transport-rel : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } (_β‰Ί_ : {x : X} β†’ Y x β†’ Y x β†’ 𝓦 Μ‡ )
              β†’ (a x : X) (b : Y a) (v : Y x) (p : a ≑ x)
              β†’  v β‰Ί transport Y p b
              β†’ back-transport Y p v β‰Ί b
transport-rel _β‰Ί_ a .a b v refl = id

transport-rel' : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } (_β‰Ί_ : {x : X} β†’ Y x β†’ Y x β†’ 𝓦 Μ‡ )
              β†’ (a x : X) (b : Y a) (v : Y x) (r : x ≑ a)
              β†’ transport Y r v β‰Ί b
              β†’ v β‰Ί back-transport Y r b
transport-rel' _β‰Ί_ a .a b v refl = id

transport-const : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {x x' : X} {y : Y} (p : x ≑ x')
                β†’ transport (Ξ» (_ : X) β†’ Y) p y ≑ y
transport-const refl = refl

apd' : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (f : (x : X) β†’ A x) {x y : X}
       (p : x ≑ y) β†’ transport A p (f x) ≑ f y
apd' A f refl = refl

apd : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (f : (x : X) β†’ A x) {x y : X}
      (p : x ≑ y) β†’ transport A p (f x) ≑ f y
apd = apd' _

ap-id-is-id : {X : 𝓀 Μ‡ } {x y : X} (p : x ≑ y) β†’ p ≑ ap id p
ap-id-is-id refl = refl

ap-comp : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) {x y z : X} (p : x ≑ y) (q : y ≑ z)
        β†’ ap f (p βˆ™ q) ≑ ap f p βˆ™ ap f q
ap-comp f refl refl = refl

ap-sym : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) {x y : X} (p : x ≑ y)
       β†’ (ap f p) ⁻¹ ≑ ap f (p ⁻¹)
ap-sym f refl = refl

ap-ap : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } (f : X β†’ Y) (g : Y β†’ Z) {x x' : X} (r : x ≑ x')
      β†’ ap g (ap f r) ≑ ap (g ∘ f) r
ap-ap {𝓀} {π“₯} {𝓦} {X} {Y} {Z} f g = J A (Ξ» x β†’ refl)
 where
  A : (x x' : X) β†’ x ≑ x' β†’ 𝓦 Μ‡
  A x x' r = ap g (ap f r) ≑ ap (g ∘ f) r

apβ‚‚ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } (f : X β†’ Y β†’ Z) {xβ‚€ x₁ : X} {yβ‚€ y₁ : Y}
   β†’ xβ‚€ ≑ x₁ β†’ yβ‚€ ≑ y₁ β†’ f xβ‚€ yβ‚€ ≑ f x₁ y₁
apβ‚‚ f refl refl = refl

refl-left-neutral : {X : 𝓀 Μ‡ } {x y : X} {p : x ≑ y} β†’ refl βˆ™ p ≑ p
refl-left-neutral {𝓀} {X} {x} {_} {refl} = refl

refl-right-neutral : {X : 𝓀 Μ‡ } {x y : X} (p : x ≑ y) β†’ p ≑ p βˆ™ refl
refl-right-neutral p = refl

βˆ™assoc : {X : 𝓀 Μ‡ } {x y z t : X} (p : x ≑ y) (q : y ≑ z) (r : z ≑ t)
       β†’ (p βˆ™ q) βˆ™ r ≑ p βˆ™ (q βˆ™ r)
βˆ™assoc refl refl refl = refl

happly' : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (f g : Ξ  A) β†’ f ≑ g β†’ f ∼ g
happly' f g p x = ap (Ξ» - β†’ - x) p

happly : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {f g : Ξ  A} β†’ f ≑ g β†’ f ∼ g
happly = happly' _ _

sym-is-inverse : {X : 𝓀 Μ‡ } {x y : X} (p : x ≑ y)
               β†’ refl ≑ p ⁻¹ βˆ™ p
sym-is-inverse = J (Ξ» x y p β†’ refl ≑ p ⁻¹ βˆ™ p) (Ξ» x β†’ refl)

sym-is-inverse' : {X : 𝓀 Μ‡ } {x y : X} (p : x ≑ y)
                β†’ refl ≑ p βˆ™ p ⁻¹
sym-is-inverse' refl = refl

⁻¹-involutive : {X : 𝓀 Μ‡ } {x y : X} (p : x ≑ y) β†’ (p ⁻¹)⁻¹ ≑ p
⁻¹-involutive refl = refl

⁻¹-contravariant : {X : 𝓀 Μ‡ } {x y : X} (p : x ≑ y) {z : X} (q : y ≑ z)
                 β†’ q ⁻¹ βˆ™ p ⁻¹ ≑ (p βˆ™ q)⁻¹
⁻¹-contravariant refl refl = refl

left-inverse : {X : 𝓀 Μ‡ } {x y : X} (p : x ≑ y) β†’ p ⁻¹ βˆ™ p ≑ refl
left-inverse {𝓀} {X} {x} {y} refl = refl

right-inverse : {X : 𝓀 Μ‡ } {x y : X} (p : x ≑ y) β†’ refl ≑ p βˆ™ p ⁻¹
right-inverse {𝓀} {X} {x} {y} refl = refl

cancel-left : {X : 𝓀 Μ‡ } {x y z : X} {p : x ≑ y} {q r : y ≑ z}
            β†’ p βˆ™ q ≑ p βˆ™ r β†’ q ≑ r
cancel-left {𝓀} {X} {x} {y} {z} {p} {q} {r} s =
       q              β‰‘βŸ¨ refl-left-neutral ⁻¹ ⟩
       refl βˆ™ q       β‰‘βŸ¨ ap (Ξ» - β†’ - βˆ™ q) ((left-inverse p)⁻¹) ⟩
       (p ⁻¹ βˆ™ p) βˆ™ q β‰‘βŸ¨ βˆ™assoc (p ⁻¹) p q ⟩
       p ⁻¹ βˆ™ (p βˆ™ q) β‰‘βŸ¨ ap (Ξ» - β†’ p ⁻¹ βˆ™ -) s ⟩
       p ⁻¹ βˆ™ (p βˆ™ r) β‰‘βŸ¨ (βˆ™assoc (p ⁻¹) p r)⁻¹ ⟩
       (p ⁻¹ βˆ™ p) βˆ™ r β‰‘βŸ¨ ap (Ξ» - β†’ - βˆ™ r) (left-inverse p) ⟩
       refl βˆ™ r       β‰‘βŸ¨ refl-left-neutral ⟩
       r ∎

homotopies-are-natural' : {X : 𝓀 Μ‡ } {A : π“₯ Μ‡ } (f g : X β†’ A) (H : f ∼ g) {x y : X} {p : x ≑ y}
                      β†’ H x βˆ™ ap g p βˆ™ (H y)⁻¹ ≑ ap f p
homotopies-are-natural' f g H {x} {_} {refl} = trans-sym' (H x)

homotopies-are-natural : {X : 𝓀 Μ‡ } {A : π“₯ Μ‡ } (f g : X β†’ A) (H : f ∼ g) {x y : X} {p : x ≑ y}
                      β†’ H x βˆ™ ap g p ≑ ap f p βˆ™ H y
homotopies-are-natural f g H {x} {_} {refl} = refl-left-neutral ⁻¹

to-Γ—-≑ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {x x' : X} {y y' : Y}
       β†’ x ≑ x' β†’ y ≑ y' β†’ (x , y) ≑ (x' , y')
to-Γ—-≑ refl refl = refl

to-Γ—-≑' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {z z' : X Γ— Y}
        β†’ (pr₁ z ≑ pr₁ z') Γ— (prβ‚‚ z ≑ prβ‚‚ z') β†’ z ≑ z'
to-Γ—-≑' (refl , refl) = refl

from-Γ—-≑' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {z z' : X Γ— Y}
          β†’ z ≑ z' β†’ (pr₁ z ≑ pr₁ z') Γ— (prβ‚‚ z ≑ prβ‚‚ z' )
from-Γ—-≑' refl = (refl , refl)

tofrom-Γ—-≑ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {z z' : X Γ— Y}
             β†’ (p : z ≑ z')
             β†’ p ≑ to-Γ—-≑ (pr₁ (from-Γ—-≑' p)) (prβ‚‚ (from-Γ—-≑' p))
tofrom-Γ—-≑ refl = refl

from-Ξ£-≑ : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } {Οƒ Ο„ : Ξ£ Y} (r : Οƒ ≑ Ο„)
         β†’ Ξ£ \(p : pr₁ Οƒ ≑ pr₁ Ο„) β†’ transport Y p (prβ‚‚ Οƒ) ≑ (prβ‚‚ Ο„)
from-Ξ£-≑ refl = refl , refl

from-Ξ£-≑' : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } {u v : Ξ£ Y} (r : u ≑ v)
          β†’ transport Y (ap pr₁ r) (prβ‚‚ u) ≑ (prβ‚‚ v)
from-Ξ£-≑' {𝓀} {π“₯} {X} {Y} {u} {v} = J A (Ξ» u β†’ refl) {u} {v}
 where
  A : (u v : Ξ£ Y) β†’ u ≑ v β†’ π“₯ Μ‡
  A u v r = transport Y (ap pr₁ r) (prβ‚‚ u) ≑ (prβ‚‚ v)

to-Ξ£-≑ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {Οƒ Ο„ : Ξ£ A}
       β†’ (Ξ£ \(p : pr₁ Οƒ ≑ pr₁ Ο„) β†’ transport A p (prβ‚‚ Οƒ) ≑ prβ‚‚ Ο„)
       β†’ Οƒ ≑ Ο„
to-Ξ£-≑ (refl , refl) = refl

ap-pr₁-to-Ξ£-≑ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {Οƒ Ο„ : Ξ£ A}
                (w : Ξ£ \(p : pr₁ Οƒ ≑ pr₁ Ο„) β†’ transport A p (prβ‚‚ Οƒ) ≑ prβ‚‚ Ο„)
              β†’ ap pr₁ (to-Ξ£-≑ w) ≑ pr₁ w
ap-pr₁-to-Ξ£-≑ (refl , refl) = refl

to-Ξ£-≑' : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } {x : X} {y y' : Y x}
        β†’ y ≑ y' β†’ _≑_ {_} {Ξ£ Y} (x , y) (x , y')
to-Ξ£-≑' {𝓀} {π“₯} {X} {Y} {x} = ap (Ξ» - β†’ (x , -))

fromto-Ξ£-≑ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {Οƒ Ο„ : Ξ£ A} (w : Ξ£ \(p : pr₁ Οƒ ≑ pr₁ Ο„) β†’ transport A p (prβ‚‚ Οƒ) ≑ prβ‚‚ Ο„)
           β†’ from-Ξ£-≑ (to-Ξ£-≑ w) ≑ w
fromto-Ξ£-≑ (refl , refl) = refl

tofrom-Ξ£-≑ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {Οƒ Ο„ : Ξ£ A} (r : Οƒ ≑ Ο„)
           β†’ to-Ξ£-≑ (from-Ξ£-≑ r) ≑ r
tofrom-Ξ£-≑ refl = refl

\end{code}