text:
{-# OPTIONS --without-K --allow-unsolved-metas --exact-split #-}

module 16-pushouts where

import 15-pullbacks
open 15-pullbacks public

-- Section 14.1

{- We define the type of cocones with vertex X on a span. Since we will use it
   later on, we will also characterize the identity type of the type of cocones
   with a given vertex X. -}

cocone :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) → UU l4 → UU _
cocone {A = A} {B = B} f g X =
  Σ (A → X) (λ i → Σ (B → X) (λ j → (i ∘ f) ~ (j ∘ g)))

{- We characterize the identity type of the type of cocones with vertex C. -}

coherence-htpy-cocone :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c c' : cocone f g X) →
  (K : (pr1 c) ~ (pr1 c')) (L : (pr1 (pr2 c)) ~ (pr1 (pr2 c'))) → UU (l1 ⊔ l4)
coherence-htpy-cocone f g c c' K L =
  ((pr2 (pr2 c)) ∙h (L ·r g)) ~ ((K ·r f) ∙h (pr2 (pr2 c')))

htpy-cocone :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} →
  cocone f g X → cocone f g X → UU (l1 ⊔ (l2 ⊔ (l3 ⊔ l4)))
htpy-cocone f g c c' =
  Σ ((pr1 c) ~ (pr1 c'))
    ( λ K → Σ ((pr1 (pr2 c)) ~ (pr1 (pr2 c')))
      ( coherence-htpy-cocone f g c c' K))

reflexive-htpy-cocone :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  htpy-cocone f g c c
reflexive-htpy-cocone f g (pair i (pair j H)) =
  pair htpy-refl (pair htpy-refl htpy-right-unit)

htpy-cocone-eq :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c c' : cocone f g X) →
  Id c c' → htpy-cocone f g c c'
htpy-cocone-eq f g c .c refl = reflexive-htpy-cocone f g c

is-contr-total-htpy-cocone :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  is-contr (Σ (cocone f g X) (htpy-cocone f g c))
is-contr-total-htpy-cocone f g c =
  is-contr-total-Eq-structure
    ( λ i' jH' K → Σ ((pr1 (pr2 c)) ~ (pr1 jH'))
      ( coherence-htpy-cocone f g c (pair i' jH') K))
    ( is-contr-total-htpy (pr1 c))
    ( pair (pr1 c) htpy-refl)
    ( is-contr-total-Eq-structure
      ( λ j' H' → coherence-htpy-cocone f g c
        ( pair (pr1 c) (pair j' H'))
        ( htpy-refl))
      ( is-contr-total-htpy (pr1 (pr2 c)))
      ( pair (pr1 (pr2 c)) htpy-refl)
      ( is-contr-is-equiv'
        ( Σ (((pr1 c) ∘ f) ~ ((pr1 (pr2 c)) ∘ g)) (λ H' → (pr2 (pr2 c)) ~ H'))
        ( tot (λ H' M → htpy-right-unit ∙h M))
        ( is-equiv-tot-is-fiberwise-equiv (λ H' → is-equiv-htpy-concat _ _))
        ( is-contr-total-htpy (pr2 (pr2 c)))))

is-equiv-htpy-cocone-eq :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c c' : cocone f g X) →
  is-equiv (htpy-cocone-eq f g c c')
is-equiv-htpy-cocone-eq f g c =
  fundamental-theorem-id c
    ( reflexive-htpy-cocone f g c)
    ( is-contr-total-htpy-cocone f g c)
    ( htpy-cocone-eq f g c)

eq-htpy-cocone :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c c' : cocone f g X) →
  htpy-cocone f g c c' → Id c c'
eq-htpy-cocone f g c c' = inv-is-equiv (is-equiv-htpy-cocone-eq f g c c')

{- Given a cocone c on a span S with vertex X, and a type Y, the function
   cocone-map sends a function X → Y to a new cocone with vertex Y. -}

cocone-map :
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} {Y : UU l5} →
  cocone f g X → (X → Y) → cocone f g Y
cocone-map f g (pair i (pair j H)) h =
  pair (h ∘ i) (pair (h ∘ j) (h ·l H))

cocone-map-id :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  Id (cocone-map f g c id) c
cocone-map-id f g (pair i (pair j H)) =
  eq-pair refl (eq-pair refl (eq-htpy (λ s → ap-id (H s))))

cocone-map-comp :
  {l1 l2 l3 l4 l5 l6 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X)
  {Y : UU l5} (h : X → Y) {Z : UU l6} (k : Y → Z) →
  Id (cocone-map f g c (k ∘ h)) ((cocone-map f g (cocone-map f g c h) k))
cocone-map-comp f g (pair i (pair j H)) h k =
  eq-pair refl (eq-pair refl (eq-htpy (λ s → ap-comp k h (H s))))

{- A cocone c on a span S is said to satisfy the universal property of the
   pushout of S if the function cocone-map is an equivalence for every type Y.
   -}

universal-property-pushout :
  {l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} →
  cocone f g X → UU _
universal-property-pushout l f g c =
  (Y : UU l) → is-equiv (cocone-map f g {Y = Y} c)

-- Section 14.2 Suspensions

suspension-structure :
  {l1 l2 : Level} (X : UU l1) (Y : UU l2) → UU (l1 ⊔ l2)
suspension-structure X Y = Σ Y (λ N → Σ Y (λ S → (x : X) → Id N S))

suspension-cocone' :
  {l1 l2 : Level} (X : UU l1) (Y : UU l2) → UU (l1 ⊔ l2)
suspension-cocone' X Y = cocone (const X unit star) (const X unit star) Y

cocone-suspension-structure :
  {l1 l2 : Level} (X : UU l1) (Y : UU l2) →
  suspension-structure X Y → suspension-cocone' X Y
cocone-suspension-structure X Y (pair N (pair S merid)) =
  pair
    ( const unit Y N)
    ( pair
      ( const unit Y S)
      ( merid))

universal-property-suspension' :
  (l : Level) {l1 l2 : Level} (X : UU l1) (Y : UU l2)
  (susp-str : suspension-structure X Y) → UU (lsuc l ⊔ l1 ⊔ l2)
universal-property-suspension' l X Y susp-str-Y =
  universal-property-pushout l
    ( const X unit star)
    ( const X unit star)
    ( cocone-suspension-structure X Y susp-str-Y)

is-suspension :
  (l : Level) {l1 l2 : Level} (X : UU l1) (Y : UU l2) → UU (lsuc l ⊔ l1 ⊔ l2)
is-suspension l X Y =
  Σ (suspension-structure X Y) (universal-property-suspension' l X Y)

{- We define the type of suspensions at universe level l, for any type X. Since
   we would like to define type families over a suspension by the universal
   property of the suspension, we assume that the universal property of a
   suspension holds for at least level (lsuc l ⊔ l1). This is the level that
   contains both X and the suspension itself. -}

UU-Suspensions :
  (l : Level) {l1 : Level} (X : UU l1) → UU (lsuc (lsuc l) ⊔ lsuc l1)
UU-Suspensions l {l1} X = Σ (UU l) (is-suspension (lsuc l ⊔ l1) X)

{- We now work towards Lemma 17.2.2. -}

suspension-cocone :
  {l1 l2 : Level} (X : UU l1) (Z : UU l2) → UU _
suspension-cocone X Z = Σ Z (λ z1 → Σ Z (λ z2 → (x : X) → Id z1 z2))

ev-suspension :
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} →
  (susp-str-Y : suspension-structure X Y) →
  (Z : UU l3) → (Y → Z) → suspension-cocone X Z
ev-suspension (pair N (pair S merid)) Z h =
  pair (h N) (pair (h S) (h ·l merid))

universal-property-suspension :
  (l : Level) {l1 l2 : Level} (X : UU l1) (Y : UU l2) →
  suspension-structure X Y → UU (lsuc l ⊔ l1 ⊔ l2)
universal-property-suspension l X Y susp-str-Y =
  (Z : UU l) → is-equiv (ev-suspension susp-str-Y Z)

comparison-suspension-cocone :
  {l1 l2 : Level} (X : UU l1) (Z : UU l2) →
  suspension-cocone' X Z ≃ suspension-cocone X Z
comparison-suspension-cocone X Z =
  equiv-toto
    ( λ z1 → Σ Z (λ z2 → (x : X) → Id z1 z2))
    ( equiv-ev-star' Z)
    ( λ z1 →
      equiv-toto
        ( λ z2 → (x : X) → Id (z1 star) z2)
        ( equiv-ev-star' Z)
        ( λ z2 → equiv-id ((x : X) → Id (z1 star) (z2 star))))

map-comparison-suspension-cocone :
  {l1 l2 : Level} (X : UU l1) (Z : UU l2) →
  suspension-cocone' X Z → suspension-cocone X Z
map-comparison-suspension-cocone X Z =
  map-equiv (comparison-suspension-cocone X Z)

is-equiv-map-comparison-suspension-cocone :
  {l1 l2 : Level} (X : UU l1) (Z : UU l2) →
  is-equiv (map-comparison-suspension-cocone X Z)
is-equiv-map-comparison-suspension-cocone X Z =
  is-equiv-map-equiv (comparison-suspension-cocone X Z)

triangle-ev-suspension :
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} →
  (susp-str-Y : suspension-structure X Y) →
  (Z : UU l3) →
  ( ( map-comparison-suspension-cocone X Z) ∘
    ( cocone-map
      ( const X unit star)
      ( const X unit star)
      ( cocone-suspension-structure X Y susp-str-Y))) ~
  ( ev-suspension susp-str-Y Z)
triangle-ev-suspension (pair N (pair S merid)) Z h = refl

is-equiv-ev-suspension :
  { l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} →
  ( susp-str-Y : suspension-structure X Y) →
  ( up-Y : universal-property-suspension' l3 X Y susp-str-Y) →
  ( Z : UU l3) → is-equiv (ev-suspension susp-str-Y Z)
is-equiv-ev-suspension {X = X} susp-str-Y up-Y Z =
  is-equiv-comp
    ( ev-suspension susp-str-Y Z)
    ( map-comparison-suspension-cocone X Z)
    ( cocone-map
      ( const X unit star)
      ( const X unit star)
      ( cocone-suspension-structure X _ susp-str-Y))
    ( htpy-inv (triangle-ev-suspension susp-str-Y Z))
    ( up-Y Z)
    ( is-equiv-map-comparison-suspension-cocone X Z)

{- Pointed maps and pointed homotopies. -}

pointed-fam :
  {l1 : Level} (l : Level) (X : UU-pt l1) → UU (lsuc l ⊔ l1)
pointed-fam l (pair X x) = Σ (X → UU l) (λ P → P x)

pointed-Π :
  {l1 l2 : Level} (X : UU-pt l1) (P : pointed-fam l2 X) → UU (l1 ⊔ l2)
pointed-Π (pair X x) (pair P p) = Σ ((x' : X) → P x') (λ f → Id (f x) p)

pointed-htpy :
  {l1 l2 : Level} (X : UU-pt l1) (P : pointed-fam l2 X) →
  (f g : pointed-Π X P) → UU (l1 ⊔ l2)
pointed-htpy (pair X x) (pair P p) (pair f α) g =
  pointed-Π (pair X x) (pair (λ x' → Id (f x') (pr1 g x')) (α ∙ (inv (pr2 g))))

pointed-htpy-refl :
  {l1 l2 : Level} (X : UU-pt l1) (P : pointed-fam l2 X) →
  (f : pointed-Π X P) → pointed-htpy X P f f
pointed-htpy-refl (pair X x) (pair P p) (pair f α) =
  pair htpy-refl (inv (right-inv α))

pointed-htpy-eq :
  {l1 l2 : Level} (X : UU-pt l1) (P : pointed-fam l2 X) →
  (f g : pointed-Π X P) → Id f g → pointed-htpy X P f g
pointed-htpy-eq X P f .f refl = pointed-htpy-refl X P f

is-contr-total-pointed-htpy :
  {l1 l2 : Level} (X : UU-pt l1) (P : pointed-fam l2 X) (f : pointed-Π X P) →
  is-contr (Σ (pointed-Π X P) (pointed-htpy X P f))
is-contr-total-pointed-htpy (pair X x) (pair P p) (pair f α) =
  is-contr-total-Eq-structure
    ( λ g β (H : f ~ g) → Id (H x) (α ∙ (inv β)))
    ( is-contr-total-htpy f)
    ( pair f htpy-refl)
    ( is-contr-equiv'
      ( Σ (Id (f x) p) (λ β → Id β α))
      ( equiv-tot (λ β → equiv-con-inv refl β α))
      ( is-contr-total-path' α))

is-equiv-pointed-htpy-eq :
  {l1 l2 : Level} (X : UU-pt l1) (P : pointed-fam l2 X) →
  (f g : pointed-Π X P) → is-equiv (pointed-htpy-eq X P f g)
is-equiv-pointed-htpy-eq X P f =
  fundamental-theorem-id f
    ( pointed-htpy-refl X P f)
    ( is-contr-total-pointed-htpy X P f)
    ( pointed-htpy-eq X P f)

eq-pointed-htpy :
  {l1 l2 : Level} (X : UU-pt l1) (P : pointed-fam l2 X) →
  (f g : pointed-Π X P) → (pointed-htpy X P f g) → Id f g
eq-pointed-htpy X P f g = inv-is-equiv (is-equiv-pointed-htpy-eq X P f g)

-- Section 14.3 Duality of pushouts and pullbacks

{- The universal property of the pushout of a span S can also be stated as a
   pullback-property: a cocone c = (pair i (pair j H)) with vertex X
   satisfies the universal property of the pushout of S if and only if the
   square

     Y^X -----> Y^B
      |          |
      |          |
      V          V
     Y^A -----> Y^S

   is a pullback square for every type Y. Below, we first define the cone of
   this commuting square, and then we introduce the type
   pullback-property-pushout, which states that the above square is a pullback.
   -}

htpy-precomp :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
  {f g : A → B} (H : f ~ g) (C : UU l3) →
  (precomp f C) ~ (precomp g C)
htpy-precomp H C h = eq-htpy (h ·l H)

compute-htpy-precomp :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) (C : UU l3) →
  (htpy-precomp (htpy-refl' f) C) ~ htpy-refl
compute-htpy-precomp f C h = eq-htpy-htpy-refl (h ∘ f)

cone-pullback-property-pushout :
  {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (Y : UU l) →
  cone (λ (h : A → Y) → h ∘ f) (λ (h : B → Y) → h ∘ g) (X → Y)
cone-pullback-property-pushout f g {X} c Y =
  pair
    ( precomp (pr1 c) Y)
    ( pair
      ( precomp (pr1 (pr2 c)) Y)
      ( htpy-precomp (pr2 (pr2 c)) Y))

pullback-property-pushout :
  {l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  UU (l1 ⊔ (l2 ⊔ (l3 ⊔ (l4 ⊔ lsuc l))))
pullback-property-pushout l {S} {A} {B} f g {X} c =
  (Y : UU l) → is-pullback
    ( precomp f Y)
    ( precomp g Y)
    ( cone-pullback-property-pushout f g c Y)

{- In order to show that the universal property of pushouts is equivalent to
   the pullback property, we show that the maps cocone-map and the gap map fit
   in a commuting triangle, where the third map is an equivalence. The claim
   then follows from the 3-for-2 property of equivalences. -}

triangle-pullback-property-pushout-universal-property-pushout :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2}
  {B : UU l3} (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  {l : Level} (Y : UU l) →
  ( cocone-map f g c) ~
  ( ( tot (λ i' → tot (λ j' p → htpy-eq p))) ∘
    ( gap (λ h → h ∘ f) (λ h → h ∘ g) (cone-pullback-property-pushout f g c Y)))
triangle-pullback-property-pushout-universal-property-pushout
  {S = S} {A = A} {B = B} f g (pair i (pair j H)) Y h =
    eq-pair refl (eq-pair refl (inv (issec-eq-htpy (h ·l H))))

pullback-property-pushout-universal-property-pushout :
  {l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2}
  {B : UU l3} (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  universal-property-pushout l f g c → pullback-property-pushout l f g c
pullback-property-pushout-universal-property-pushout
  l f g (pair i (pair j H)) up-c Y =
  let c = (pair i (pair j H)) in
  is-equiv-right-factor
    ( cocone-map f g c)
    ( tot (λ i' → tot (λ j' p → htpy-eq p)))
    ( gap (λ h → h ∘ f) (λ h → h ∘ g) (cone-pullback-property-pushout f g c Y))
    ( triangle-pullback-property-pushout-universal-property-pushout f g c Y)
    ( is-equiv-tot-is-fiberwise-equiv
      ( λ i' → is-equiv-tot-is-fiberwise-equiv
        ( λ j' → funext (i' ∘ f) (j' ∘ g))))
    ( up-c Y)

universal-property-pushout-pullback-property-pushout :
  {l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2}
  {B : UU l3} (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  pullback-property-pushout l f g c → universal-property-pushout l f g c
universal-property-pushout-pullback-property-pushout
  l f g (pair i (pair j H)) pb-c Y =
  let c = (pair i (pair j H)) in
  is-equiv-comp
    ( cocone-map f g c)
    ( tot (λ i' → tot (λ j' p → htpy-eq p)))
    ( gap (λ h → h ∘ f) (λ h → h ∘ g) (cone-pullback-property-pushout f g c Y))
    ( triangle-pullback-property-pushout-universal-property-pushout f g c Y)
    ( pb-c Y)
    ( is-equiv-tot-is-fiberwise-equiv
      ( λ i' → is-equiv-tot-is-fiberwise-equiv
        ( λ j' → funext (i' ∘ f) (j' ∘ g))))

cocone-compose-horizontal :
  { l1 l2 l3 l4 l5 l6 : Level}
  { A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {Y : UU l5} {Z : UU l6}
  ( f : A → X) (i : A → B) (k : B → C) →
  ( c : cocone f i Y) (d : cocone (pr1 (pr2 c)) k Z) →
  cocone f (k ∘ i) Z
cocone-compose-horizontal f i k (pair j (pair g H)) (pair l (pair h K)) =
  pair
    ( l ∘ j)
    ( pair
      ( h)
      ( (l ·l H) ∙h (K ·r i)))

{-
is-pushout-rectangle-is-pushout-right-square :
  ( l : Level) { l1 l2 l3 l4 l5 l6 : Level}
  { A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {Y : UU l5} {Z : UU l6}
  ( f : A → X) (i : A → B) (k : B → C) →
  ( c : cocone f i Y) (d : cocone (pr1 (pr2 c)) k Z) →
  universal-property-pushout l f i c →
  universal-property-pushout l (pr1 (pr2 c)) k d →
  universal-property-pushout l f (k ∘ i) (cocone-compose-horizontal f i k c d)
is-pushout-rectangle-is-pushout-right-square l f i k c d up-Y up-Z =
  universal-property-pushout-pullback-property-pushout l f (k ∘ i)
    ( cocone-compose-horizontal f i k c d)
    ( λ T → is-pullback-htpy {!!} {!!} {!!} {!!} {!!} {!!} {!!})
-}

-- Exercises

-- Exercise 13.1

-- Exercise 13.2

is-equiv-universal-property-pushout :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g C) →
  is-equiv f →
  ((l : Level) → universal-property-pushout l f g c) → is-equiv (pr1 (pr2 c))
is-equiv-universal-property-pushout
  {A = A} {B} f g (pair i (pair j H)) is-equiv-f up-c =
  is-equiv-is-equiv-precomp j
    ( λ l T →
      is-equiv-is-pullback'
        ( λ (h : A → T) → h ∘ f)
        ( λ (h : B → T) → h ∘ g)
        ( cone-pullback-property-pushout f g (pair i (pair j H)) T)
        ( is-equiv-precomp-is-equiv f is-equiv-f T)
        ( pullback-property-pushout-universal-property-pushout
          l f g (pair i (pair j H)) (up-c l) T))

universal-property-pushout-is-equiv :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g C) →
  is-equiv f → is-equiv (pr1 (pr2 c)) →
  ((l : Level) → universal-property-pushout l f g c)
universal-property-pushout-is-equiv f g (pair i (pair j H)) is-equiv-f is-equiv-j l =
  let c = (pair i (pair j H)) in
  universal-property-pushout-pullback-property-pushout l f g c
    ( λ T → is-pullback-is-equiv'
      ( λ h → h ∘ f)
      ( λ h → h ∘ g)
      ( cone-pullback-property-pushout f g c T)
      ( is-equiv-precomp-is-equiv f is-equiv-f T)
      ( is-equiv-precomp-is-equiv j is-equiv-j T))

max_stars_repo_name: tadejpetric/HoTT-Intro

max_issues_repo_name: tadejpetric/HoTT-Intro

max_forks_repo_name: tadejpetric/HoTT-Intro


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of unique lists (setoid equality)
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.Unique.Setoid.Properties where

open import Data.Fin.Base using (Fin)
open import Data.List.Base
open import Data.List.Relation.Binary.Disjoint.Setoid
open import Data.List.Relation.Binary.Disjoint.Setoid.Properties
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
open import Data.List.Relation.Unary.Unique.Setoid
import Data.List.Relation.Unary.AllPairs.Properties as AllPairs
open import Data.Nat.Base
open import Function using (_∘_)
open import Relation.Binary using (Rel; Setoid)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Unary using (Pred; Decidable)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contraposition)

------------------------------------------------------------------------
-- Introduction (⁺) and elimination (⁻) rules for list operations
------------------------------------------------------------------------
-- map

module _ {a b ℓ₁ ℓ₂} (S : Setoid a ℓ₁) (R : Setoid b ℓ₂) where

  open Setoid S renaming (Carrier to A; _≈_ to _≈₁_)
  open Setoid R renaming (Carrier to B; _≈_ to _≈₂_)

  map⁺ : ∀ {f} → (∀ {x y} → f x ≈₂ f y → x ≈₁ y) →
         ∀ {xs} → Unique S xs → Unique R (map f xs)
  map⁺ inj xs! = AllPairs.map⁺ (AllPairs.map (contraposition inj) xs!)

------------------------------------------------------------------------
-- ++

module _ {a ℓ} (S : Setoid a ℓ) where

  ++⁺ : ∀ {xs ys} → Unique S xs → Unique S ys → Disjoint S xs ys → Unique S (xs ++ ys)
  ++⁺ xs! ys! xs#ys = AllPairs.++⁺ xs! ys! (Disjoint⇒AllAll S xs#ys)

------------------------------------------------------------------------
-- concat

module _ {a ℓ} (S : Setoid a ℓ) where

  concat⁺ : ∀ {xss} → All (Unique S) xss → AllPairs (Disjoint S) xss → Unique S (concat xss)
  concat⁺ xss! xss# = AllPairs.concat⁺ xss! (AllPairs.map (Disjoint⇒AllAll S) xss#)

------------------------------------------------------------------------
-- take & drop

module _ {a ℓ} (S : Setoid a ℓ) where

  drop⁺ : ∀ {xs} n → Unique S xs → Unique S (drop n xs)
  drop⁺ = AllPairs.drop⁺

  take⁺ : ∀ {xs} n → Unique S xs → Unique S (take n xs)
  take⁺ = AllPairs.take⁺

------------------------------------------------------------------------
-- applyUpTo

module _ {a ℓ} (S : Setoid a ℓ) where

  open Setoid S using (_≈_; _≉_) renaming (Carrier to A)

  applyUpTo⁺₁ : ∀ f n → (∀ {i j} → i < j → j < n → f i ≉ f j) →
                Unique S (applyUpTo f n)
  applyUpTo⁺₁ = AllPairs.applyUpTo⁺₁

  applyUpTo⁺₂ : ∀ f n → (∀ i j → f i ≉ f j) →
                Unique S (applyUpTo f n)
  applyUpTo⁺₂ = AllPairs.applyUpTo⁺₂

------------------------------------------------------------------------
-- applyDownFrom

module _ {a ℓ} (S : Setoid a ℓ) where

  open Setoid S using (_≈_; _≉_) renaming (Carrier to A)

  applyDownFrom⁺₁ : ∀ f n → (∀ {i j} → j < i → i < n → f i ≉ f j) →
                    Unique S (applyDownFrom f n)
  applyDownFrom⁺₁ = AllPairs.applyDownFrom⁺₁

  applyDownFrom⁺₂ : ∀ f n → (∀ i j → f i ≉ f j) →
                    Unique S (applyDownFrom f n)
  applyDownFrom⁺₂ = AllPairs.applyDownFrom⁺₂

------------------------------------------------------------------------
-- tabulate

module _ {a ℓ} (S : Setoid a ℓ) where

  open Setoid S renaming (Carrier to A)

  tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → f i ≈ f j → i ≡ j) →
              Unique S (tabulate f)
  tabulate⁺ f-inj = AllPairs.tabulate⁺ (_∘ f-inj)

------------------------------------------------------------------------
-- filter

module _ {a ℓ} (S : Setoid a ℓ) {p} {P : Pred _ p} (P? : Decidable P) where

  open Setoid S renaming (Carrier to A)

  filter⁺ : ∀ {xs} → Unique S xs → Unique S (filter P? xs)
  filter⁺ = AllPairs.filter⁺ P?

ext: agda


text:
{-# OPTIONS --no-positivity-check #-}

module Section5 where

open import Section4b public

-- 5. Normal form
-- ==============
--
-- As we have seen above it is not necessary to know that `nf` actually gives a proof tree in
-- η-normal form for the results above.  This is however the case.  We can mutually inductively
-- define when a proof tree is in long η-normal form, `enf`, and in applicative normal form, `anf`.  (…)

mutual
  data enf : ∀ {Γ A} → Γ ⊢ A → Set where
    ƛ : ∀ {Γ A B}
          (x : Name) {{_ : T (fresh x Γ)}} → {M : [ Γ , x ∷ A ] ⊢ B} → enf M →
          enf (ƛ x M)
    α : ∀ {Γ} {M : Γ ⊢ •} →
          anf M →
          enf M

  data anf : ∀ {Γ A} → Γ ⊢ A → Set where
    ν   : ∀ {Γ A} →
            (x : Name) (i : Γ ∋ x ∷ A) →
            anf (ν x i)
    _∙_ : ∀ {Γ A B} {M : Γ ⊢ A ⊃ B} {N : Γ ⊢ A} →
            anf M → enf N →
            anf (M ∙ N)

-- We prove that `nf M` is in long η-normal form.  For this we define a Kripke logical
-- predicate, `𝒩`, such that `𝒩 ⟦ M ⟧` and if `𝒩 a`, then `enf (reify a)`.

data 𝒩 : ∀ {Γ A} → Γ ⊩ A → Set where
  𝓃• : ∀ {Γ} {f : Γ ⊩ •} →
         (∀ {Δ} →
            (c : Δ ⊇ Γ) →
            anf (f ⟦g⟧⟨ c ⟩)) →
         𝒩 f
  𝓃⊃ : ∀ {Γ A B} {f : Γ ⊩ A ⊃ B} →
         (∀ {Δ} {a : Δ ⊩ A} →
            (c : Δ ⊇ Γ) → 𝒩 a →
            𝒩 (f ⟦∙⟧⟨ c ⟩ a)) →
         𝒩 f

-- For base type we intuitively define `𝒩 f` to hold if `anf f`.
--
-- If `f : Γ ⊩ A ⊃ B`, then `𝒩 f` is defined to hold if `𝒩 (f ∙ a)` holds for all `a : Γ ⊩ A`
-- such that `𝒩 a`.
--
-- We also define `𝒩⋆ ρ`, `ρ : Γ ⊩⋆ Δ`, to hold if every value, `a`, in `ρ` has the property `𝒩 a`.

data 𝒩⋆ : ∀ {Γ Δ} → Δ ⊩⋆ Γ → Set where
  𝓃⋆[] : ∀ {Δ} →
           𝒩⋆ ([] {w = Δ})
  𝓃⋆≔  : ∀ {Γ Δ A x} {{_ : T (fresh x Γ)}} {ρ : Δ ⊩⋆ Γ} {a : Δ ⊩ A} →
           𝒩⋆ ρ → 𝒩 a →
           𝒩⋆ [ ρ , x ≔ a ]

-- We prove the following lemmas which are used to prove Lemma 10.

cong↑⟨_⟩𝒩 : ∀ {Γ Δ A} →
              (c : Δ ⊇ Γ) → {a : Γ ⊩ A} → 𝒩 a →
              𝒩 (↑⟨ c ⟩ a)
cong↑⟨ c ⟩𝒩 (𝓃• h) = 𝓃• (λ c′    → h (c ○ c′))
cong↑⟨ c ⟩𝒩 (𝓃⊃ h) = 𝓃⊃ (λ c′ nₐ → h (c ○ c′) nₐ)

conglookup𝒩 : ∀ {Γ Δ A x} {ρ : Δ ⊩⋆ Γ} →
                 𝒩⋆ ρ → (i : Γ ∋ x ∷ A) →
                 𝒩 (lookup ρ i)
conglookup𝒩 (𝓃⋆≔ n⋆ n) zero    = n
conglookup𝒩 (𝓃⋆≔ n⋆ n) (suc i) = conglookup𝒩 n⋆ i

cong↑⟨_⟩𝒩⋆ : ∀ {Γ Δ Θ} {ρ : Δ ⊩⋆ Γ} →
               (c : Θ ⊇ Δ) → 𝒩⋆ ρ →
               𝒩⋆ (↑⟨ c ⟩ ρ)
cong↑⟨ c ⟩𝒩⋆ 𝓃⋆[]       = 𝓃⋆[]
cong↑⟨ c ⟩𝒩⋆ (𝓃⋆≔ n⋆ n) = 𝓃⋆≔ (cong↑⟨ c ⟩𝒩⋆ n⋆) (cong↑⟨ c ⟩𝒩 n)

cong↓⟨_⟩𝒩⋆ : ∀ {Γ Δ Θ} {ρ : Δ ⊩⋆ Γ} →
               (c : Γ ⊇ Θ) → 𝒩⋆ ρ →
               𝒩⋆ (↓⟨ c ⟩ ρ)
cong↓⟨ done ⟩𝒩⋆     n⋆ = 𝓃⋆[]
cong↓⟨ step c i ⟩𝒩⋆ n⋆ = 𝓃⋆≔ (cong↓⟨ c ⟩𝒩⋆ n⋆) (conglookup𝒩 n⋆ i)

-- The lemma is proved together with a corresponding lemma for substitutions:

-- Lemma 10.
mutual
  postulate
    lem₁₀ : ∀ {Γ Δ A} →
              (M : Γ ⊢ A) → {ρ : Δ ⊩⋆ Γ} → 𝒩⋆ ρ →
              𝒩 (⟦ M ⟧ ρ)

  postulate
    lem₁₀ₛ : ∀ {Γ Δ Θ} →
               (γ : Γ ⋙ Θ) → {ρ : Δ ⊩⋆ Γ} → 𝒩⋆ ρ →
               𝒩⋆ (⟦ γ ⟧ₛ ρ)

-- The main lemma is that for all values, `a`, such that `𝒩 a`, `reify a` returns a proof tree in
-- η-normal form, which is intuitively proved together with a proof that for all proof trees in
-- applicative normal form we can find a value, `a`, such that `𝒩 a`.  (…)

-- Lemma 11.
mutual
  postulate
    lem₁₁ : ∀ {Γ A} →
              {a : Γ ⊩ A} → 𝒩 a →
              enf (reify a)

  postulate
    lem₁₁ₛ : ∀ {Γ A} →
               (f : ∀ {Δ} → Δ ⊇ Γ → Δ ⊢ A) → (h : ∀ {Δ} → (c : Δ ⊇ Γ) → anf (f c)) →
               𝒩 (val f)

-- The proofs are by induction on the types.
--
-- It is straightforward to prove that `𝒩⋆ proj⟨ c ⟩⊩⋆` and then by Lemma 11 and Lemma 10 we get
-- that `nf M` is in long η-normal form. (…)

⟦ν⟧𝒩 : ∀ {x A Γ} → (i : Γ ∋ x ∷ A) → 𝒩 (⟦ν⟧ i)
⟦ν⟧𝒩 {x} i = lem₁₁ₛ (λ c → ν x (↑⟨ c ⟩ i))
                    (λ c → ν x (↑⟨ c ⟩ i))

proj⟨_⟩𝒩⋆ : ∀ {Γ Δ} → (c : Δ ⊇ Γ) → 𝒩⋆ proj⟨ c ⟩⊩⋆
proj⟨ done ⟩𝒩⋆     = 𝓃⋆[]
proj⟨ step c i ⟩𝒩⋆ = 𝓃⋆≔ proj⟨ c ⟩𝒩⋆ (⟦ν⟧𝒩 i)

refl𝒩⋆ : ∀ {Γ} → 𝒩⋆ (refl⊩⋆ {Γ})
refl𝒩⋆ = proj⟨ refl⊇ ⟩𝒩⋆

-- Theorem 7.
thm₇ : ∀ {Γ A} → (M : Γ ⊢ A) → enf (nf M)
thm₇ M = lem₁₁ (lem₁₀ M refl𝒩⋆)

-- Hence a proof tree is convertible with its normal form.
--
-- We can also use the results above to prove that if `ƛ(x : A).M ≅ ƛ(y : A).N`, then
-- `M(x = z) ≅ N(y = z)` where `z` is a fresh variable.  Hence we have that `ƛ` is one-to-one up to
-- α-conversion.

-- TODO: What to do about the above paragraph?

max_stars_repo_name: mietek/coquand

max_issues_repo_name: mietek/coquand

max_forks_repo_name: mietek/coquand


text:
{-# OPTIONS --no-positivity-check #-}

module Section4b where

open import Section4a public

-- 4.4. The inversion function
-- ---------------------------
--
-- It is possible to go from the semantics back to the proof trees by an inversion function, `reify`
-- that, given a semantic object in a particular Kripke model, returns a proof tree.  The particular
-- Kripke model that we choose has contexts as possible worlds, the order on contexts as the
-- order on worlds, and `_⊢ •` as `𝒢`.  (…)

instance
  canon : Model
  canon = record
    { 𝒲      = 𝒞
    ; _⊒_    = _⊇_
    ; refl⊒ = refl⊇
    ; _◇_    = _○_
    ; uniq⊒ = uniq⊇
    ; 𝒢      = _⊢ •
    }

-- In order to define the inversion function we need to be able to choose a unique fresh
-- name given a context.  We suppose a function `gensym : 𝒞 → Name` and a proof of
-- `T (fresh (gensym Γ) Γ)` which proves that `gensym` returns a fresh variable.  Note that `gensym`
-- is a function taking a context as an argument and it hence always returns the same variable
-- for a given context.

-- TODO: Can we do better than this?
postulate
  gensym : (Γ : 𝒞) → Σ Name (λ x → T (fresh x Γ))

-- The function `reify` is quite intricate.  (…)
--
-- The function `reify` is mutually defined with `val`, which given a function from a context
-- extension to a proof tree returns a semantic object as result.
--
-- We define an abbreviation for the semantic object corresponding to a variable, `⟦ν⟧`.
--
-- The functions `reify` and `val` are both defined by induction on the type:

mutual
  reify : ∀ {A Γ} → Γ ⊩ A → Γ ⊢ A
  reify {•}     {Γ} f = f ⟦g⟧⟨ refl⊇ ⟩
  reify {A ⊃ B} {Γ} f = let x , φ = gensym Γ in
                        let instance _ = φ in
                        ƛ x (reify (f ⟦∙⟧⟨ weak⊇ ⟩ ⟦ν⟧ zero))

  val : ∀ {A Γ} → (∀ {Δ} → Δ ⊇ Γ → Δ ⊢ A) → Γ ⊩ A
  val {•}     f = ⟦𝒢⟧ f
  val {A ⊃ B} f = ⟦ƛ⟧ (λ c a → val (λ c′ → f (c ○ c′) ∙ reify (↑⟨ c′ ⟩ a)))

  ⟦ν⟧ : ∀ {x Γ A} → Γ ∋ x ∷ A → Γ ⊩ A
  ⟦ν⟧ {x} i = val (λ c → ν x (↑⟨ c ⟩ i))

-- We also have that if two semantic objects in a Kripke model are extensionally equal, then
-- the result of applying the inversion function to them is intensionally equal.  To prove this
-- we first have to show the following two lemmas:

aux₄₄₁ : ∀ {A Γ} →
           (f f′ : ∀ {Δ} → Δ ⊇ Γ → Δ ⊢ A) → (∀ {Δ} → (c : Δ ⊇ Γ) → f c ≡ f′ c) →
           Eq (val f) (val f′)
aux₄₄₁ {•}     f f′ h = eq• (λ c        → h c)
aux₄₄₁ {A ⊃ B} f f′ h = eq⊃ (λ c {a} uₐ → aux₄₄₁ (λ c′ → f (c ○ c′) ∙ reify (↑⟨ c′ ⟩ a))
                            (λ c′       → f′ (c ○ c′) ∙ reify (↑⟨ c′ ⟩ a))
                            (λ c′       → cong (_∙ reify (↑⟨ c′ ⟩ a))
                                             (h (c ○ c′))))

aux₄₄₂⟨_⟩ : ∀ {A Γ Δ} →
              (c : Δ ⊇ Γ) (f : (∀ {Δ} → Δ ⊇ Γ → Δ ⊢ A)) →
              Eq (↑⟨ c ⟩ (val f)) (val (λ c′ → f (c ○ c′)))
aux₄₄₂⟨_⟩ {•}     c f = eq• (λ c′        → cong f refl)
aux₄₄₂⟨_⟩ {A ⊃ B} c f = eq⊃ (λ c′ {a} uₐ → aux₄₄₁ (λ c″ → f ((c ○ c′) ○ c″) ∙ reify (↑⟨ c″ ⟩ a))
                            (λ c″        → f (c ○ (c′ ○ c″)) ∙ reify (↑⟨ c″ ⟩ a))
                            (λ c″        → cong (_∙ reify (↑⟨ c″ ⟩ a))
                                              (cong f
                                                (sym (assoc○ c c′ c″)))))

-- Both lemmas are proved by induction on the type and they are used in order to prove the
-- following theorem,
-- which is shown mutually with a lemma
-- which states that `val` returns a uniform semantic object.  Both the theorem and the lemma
-- are proved by induction on the type.

-- Theorem 1.
mutual
  thm₁ : ∀ {Γ A} {a a′ : Γ ⊩ A} → Eq a a′ → reify a ≡ reify a′
  thm₁ {Γ} (eq• h) = h refl⊇
  thm₁ {Γ} (eq⊃ h) = let x , φ = gensym Γ in
                     let instance _ = φ in
                     cong (ƛ x)
                       (thm₁ (h weak⊇ (⟦ν⟧𝒰 zero)))

  ⟦ν⟧𝒰 : ∀ {x Γ A} → (i : Γ ∋ x ∷ A) → 𝒰 (⟦ν⟧ i)
  ⟦ν⟧𝒰 {x} i = aux₄₄₃ (λ c → ν x (↑⟨ c ⟩ i))

  aux₄₄₃ : ∀ {A Γ} → (f : ∀ {Δ} → Δ ⊇ Γ → Δ ⊢ A) → 𝒰 (val f)
  aux₄₄₃ {•}     f = 𝓊•
  aux₄₄₃ {A ⊃ B} f =
    𝓊⊃ (λ c {a} uₐ              → aux₄₄₃ (λ c′ → f (c ○ c′) ∙ reify (↑⟨ c′ ⟩ a)))
       (λ c {a} {a′} eqₐ uₐ uₐ′ → aux₄₄₁ (λ c′ → f (c ○ c′) ∙ reify (↑⟨ c′ ⟩ a))
                                          (λ c′ → f (c ○ c′) ∙ reify (↑⟨ c′ ⟩ a′))
                                          (λ c′ → cong (f (c ○ c′) ∙_)
                                                     (thm₁ (cong↑⟨ c′ ⟩Eq eqₐ))))
       (λ c c′ c″ {a} uₐ        →
         transEq (aux₄₄₂⟨ c′ ⟩ (λ c‴ → f (c ○ c‴) ∙ reify (↑⟨ c‴ ⟩ a)))
                 (aux₄₄₁ (λ c‴ → f (c ○ (c′ ○ c‴)) ∙ reify (↑⟨ c′ ○ c‴ ⟩ a))
                         (λ c‴ → f (c″ ○ c‴) ∙ reify (↑⟨ c‴ ⟩ (↑⟨ c′ ⟩ a)))
                         (λ c‴ → cong² _∙_
                                    (cong f
                                      (trans (assoc○ c c′ c‴)
                                             (comp○ (c ○ c′) c‴ (c″ ○ c‴))))
                                    (thm₁ (symEq (aux₄₁₂ c′ c‴ (c′ ○ c‴) uₐ))))))

-- We are now ready to define the function that given a proof tree computes its normal form.
-- For this we define the identity environment `proj⟨_⟩⊩⋆` which to each variable
-- in the context `Γ` associates the corresponding value of the variable in `Δ` (`⟦ν⟧` gives the
-- value of this variable).  The normalisation function, `nf`, is defined as the composition of the
-- evaluation function and `reify`.  This function is similar to the normalisation algorithm given
-- by Berger [3]; one difference is our use of Kripke models to deal with reduction under `λ`.
-- One other difference is that, since we use explicit contexts, we can use the context to find
-- the fresh names in the `reify` function.

proj⟨_⟩⊩⋆ : ∀ {Γ Δ} → Δ ⊇ Γ → Δ ⊩⋆ Γ
proj⟨ done ⟩⊩⋆             = []
proj⟨ step {x = x} c i ⟩⊩⋆ = [ proj⟨ c ⟩⊩⋆ , x ≔ ⟦ν⟧ i ]

refl⊩⋆ : ∀ {Γ} → Γ ⊩⋆ Γ
refl⊩⋆ = proj⟨ refl⊇ ⟩⊩⋆

-- The computation of the normal form is done by computing the semantics of the proof
-- tree in the identity environment and then inverting the result:

nf : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A
nf M = reify (⟦ M ⟧ refl⊩⋆)

-- We know by Theorem 1 that `nf` returns the same result when applied to two proof trees
-- having the same semantics:

-- Corollary 1.
cor₁ : ∀ {Γ A} → (M M′ : Γ ⊢ A) → Eq (⟦ M ⟧ refl⊩⋆) (⟦ M′ ⟧ refl⊩⋆) →
         nf M ≡ nf M′
cor₁ M M′ = thm₁

-- 4.5. Soundness and completeness of proof trees
-- ----------------------------------------------
--
-- We have in fact already shown soundness and completeness of the calculus of proof trees.
--
-- The evaluation function, `⟦_⟧`, for proof trees corresponds via the Curry-Howard isomorphism
-- to a proof of the soundness theorem of minimal logic with respect to Kripke models.
-- The function is defined by pattern matching which corresponds to a proof by case analysis
-- of the proof trees.
--
-- The inversion function `reify` is, again via the Curry-Howard isomorphism, a proof of the
-- completeness theorem of minimal logic with respect to a particular Kripke model where
-- the worlds are contexts.

-- 4.6. Completeness of the conversion rules for proof trees
-- ---------------------------------------------------------
--
-- In order to prove that the set of conversion rules is complete, i.e.,
-- `Eq (⟦ M ⟧ refl⊩⋆) (⟦ M′ ⟧ refl⊩⋆)` implies `M ≅ M′`, we must first prove Theorem 2: `M ≅ nf M`.
--
-- To prove the theorem we define a Kripke logical relation [15, 18]
-- which corresponds to Tait’s computability predicate.
--
-- A proof tree of base type is intuitively `CV`-related to a semantic object of base type if
-- they are convertible with each other.  (…)
--
-- A proof tree of function type, `A ⊃ B`, is intuitively `CV`-related to a semantic object of the
-- same type if they send `CV`-related proof trees and objects of type `A` to `CV`-related proof
-- trees and objects of type `B`.  (…)

data CV : ∀ {Γ A} → Γ ⊢ A → Γ ⊩ A → Set where
  cv• : ∀ {Γ} {M : Γ ⊢ •} {f : Γ ⊩ •} →
          (∀ {Δ} → (c : Δ ⊇ Γ) → M ▶ π⟨ c ⟩ ≅ f ⟦g⟧⟨ c ⟩) →
          CV M f
  cv⊃ : ∀ {Γ A B} {M : Γ ⊢ A ⊃ B} {f : Γ ⊩ A ⊃ B} →
          (∀ {Δ N a} → (c : Δ ⊇ Γ) → CV N a → CV ((M ▶ π⟨ c ⟩) ∙ N) (f ⟦∙⟧⟨ c ⟩ a)) →
          CV M f

-- The idea of this predicate is that we can show that if `CV M a` then `M ≅ reify a`, hence
-- if we show that `CV M (⟦ M ⟧ refl⊩⋆)`, we have a proof of Theorem 2.
--
-- Correspondingly for the environment we define:  (…)

data CV⋆ : ∀ {Γ Δ} → Δ ⋙ Γ → Δ ⊩⋆ Γ → Set where
  cv⋆[] : ∀ {Γ} →
            {γ : Γ ⋙ []} →
            CV⋆ γ []
  cv⋆≔  : ∀ {Γ Δ A x} {{_ : T (fresh x Γ)}}
            {γ : Δ ⋙ [ Γ , x ∷ A ]} {c : [ Γ , x ∷ A ] ⊇ Γ} {ρ : Δ ⊩⋆ Γ} {a : Δ ⊩ A} →
            CV⋆ (π⟨ c ⟩ ● γ) ρ → CV (ν x zero ▶ γ) a →
            CV⋆ γ [ ρ , x ≔ a ]

-- In order to prove Lemma 8 below we need to prove the following properties about `CV`:

cong≅CV : ∀ {Γ A} {M M′ : Γ ⊢ A} {a : Γ ⊩ A} →
            M ≅ M′ → CV M′ a →
            CV M a
cong≅CV p (cv• h) = cv• (λ c     → trans≅ (cong▶≅ p refl≅ₛ)
                                           (h c))
cong≅CV p (cv⊃ h) = cv⊃ (λ c cvₐ → cong≅CV (cong∙≅ (cong▶≅ p refl≅ₛ) refl≅)
                                            (h c cvₐ))

cong≅ₛCV⋆ : ∀ {Γ Δ} {γ γ′ : Δ ⋙ Γ} {ρ : Δ ⊩⋆ Γ} →
              γ ≅ₛ γ′ → CV⋆ γ′ ρ →
              CV⋆ γ ρ
cong≅ₛCV⋆ p cv⋆[]         = cv⋆[]
cong≅ₛCV⋆ p (cv⋆≔ cv⋆ cv) = cv⋆≔ (cong≅ₛCV⋆ (cong●≅ₛ refl≅ₛ p) cv⋆)
                                 (cong≅CV (cong▶≅ refl≅ p) cv)

cong↑⟨_⟩CV : ∀ {Γ Δ A} {M : Γ ⊢ A} {a : Γ ⊩ A} →
               (c : Δ ⊇ Γ) → CV M a →
               CV (M ▶ π⟨ c ⟩) (↑⟨ c ⟩ a)
cong↑⟨ c ⟩CV (cv• h) = cv• (λ c′     → trans≅ (trans≅ (conv₇≅ _ _ _)
                                                       (cong▶≅ refl≅ (conv₄≅ₛ _ _ _)))
                                               (h (c ○ c′)))
cong↑⟨ c ⟩CV (cv⊃ h) = cv⊃ (λ c′ cvₐ → cong≅CV (cong∙≅ (trans≅ (conv₇≅ _ _ _)
                                                                (cong▶≅ refl≅ (conv₄≅ₛ _ _ _)))
                                                        refl≅)
                                                (h (c ○ c′) cvₐ))

conglookupCV : ∀ {Γ Δ A x} {γ : Δ ⋙ Γ} {ρ : Δ ⊩⋆ Γ} →
                 CV⋆ γ ρ → (i : Γ ∋ x ∷ A) →
                 CV (ν x i ▶ γ) (lookup ρ i)
conglookupCV cv⋆[]         ()
conglookupCV (cv⋆≔ cv⋆ cv) zero    = cv
conglookupCV (cv⋆≔ cv⋆ cv) (suc i) = cong≅CV (trans≅ (cong▶≅ (sym≅ (conv₄≅ _ _ _)) refl≅ₛ)
                                                     (conv₇≅ _ _ _))
                                             (conglookupCV cv⋆ i)

cong↑⟨_⟩CV⋆ : ∀ {Γ Δ Θ} {γ : Δ ⋙ Γ} {ρ : Δ ⊩⋆ Γ} →
                (c : Θ ⊇ Δ) → CV⋆ γ ρ →
                CV⋆ (γ ● π⟨ c ⟩) (↑⟨ c ⟩ ρ)
cong↑⟨ c ⟩CV⋆ cv⋆[]         = cv⋆[]
cong↑⟨ c ⟩CV⋆ (cv⋆≔ cv⋆ cv) = cv⋆≔ (cong≅ₛCV⋆ (sym≅ₛ (conv₁≅ₛ _ _ _)) (cong↑⟨ c ⟩CV⋆ cv⋆))
                                   (cong≅CV (sym≅ (conv₇≅ _ _ _)) (cong↑⟨ c ⟩CV cv))

cong↓⟨_⟩CV⋆ : ∀ {Γ Δ Θ} {γ : Δ ⋙ Γ} {ρ : Δ ⊩⋆ Γ} →
                (c : Γ ⊇ Θ) → CV⋆ γ ρ →
                CV⋆ (π⟨ c ⟩ ● γ) (↓⟨ c ⟩ ρ)
cong↓⟨ done ⟩CV⋆     cv⋆ = cv⋆[]
cong↓⟨ step c i ⟩CV⋆ cv⋆ = cv⋆≔ {c = weak⊇}
                                (cong≅ₛCV⋆ (trans≅ₛ (sym≅ₛ (conv₁≅ₛ _ _ _))
                                                    (cong●≅ₛ (conv₄≅ₛ _ _ _) refl≅ₛ))
                                           (cong↓⟨ c ⟩CV⋆ cv⋆))
                                (cong≅CV (trans≅ (sym≅ (conv₇≅ _ _ _))
                                                 (cong▶≅ (conv₄≅ _ _ _) refl≅ₛ))
                                         (conglookupCV cv⋆ i))

-- Now we are ready to prove that if `γ` and `ρ` are `CV`-related, then `M ▶ γ` and `⟦ M ⟧ ρ` are
-- `CV`-related.  This lemma corresponds to Tait’s lemma saying that each term is computable
-- under substitution.  We prove the lemma
-- mutually with a corresponding lemma for substitutions.

-- Lemma 8.
mutual
  CV⟦_⟧ : ∀ {Γ Δ A} {γ : Δ ⋙ Γ} {ρ : Δ ⊩⋆ Γ} →
            (M : Γ ⊢ A) → CV⋆ γ ρ →
            CV (M ▶ γ) (⟦ M ⟧ ρ)
  CV⟦ ν x i ⟧ cv⋆ = conglookupCV cv⋆ i
  CV⟦ ƛ x M ⟧ cv⋆ = cv⊃ (λ c cvₐ → cong≅CV (trans≅ (cong∙≅ (conv₇≅ _ _ _) refl≅)
                                                    (conv₁≅ _ _ _))
                                            (CV⟦ M ⟧ (cv⋆≔ {c = weak⊇}
                                                           (cong≅ₛCV⋆ (conv₃≅ₛ _ _ _)
                                                                      (cong↑⟨ c ⟩CV⋆ cv⋆))
                                                           (cong≅CV (conv₃≅ _ _) cvₐ))))
  CV⟦ M ∙ N ⟧ cv⋆ with CV⟦ M ⟧ cv⋆
  CV⟦ M ∙ N ⟧ cv⋆ | (cv⊃ h) = cong≅CV (trans≅ (conv₆≅ _ _ _)
                                              (cong∙≅ (sym≅ (conv₅≅ _ _)) refl≅))
                                      (h refl⊇ (CV⟦ N ⟧ cv⋆))
  CV⟦ M ▶ γ ⟧ cv⋆ = cong≅CV (conv₇≅ _ _ _)
                            (CV⟦ M ⟧ (CV⋆⟦ γ ⟧ₛ cv⋆))

  CV⋆⟦_⟧ₛ : ∀ {Γ Δ Θ} {δ : Θ ⋙ Δ} {ρ : Θ ⊩⋆ Δ} →
              (γ : Δ ⋙ Γ) → CV⋆ δ ρ →
              CV⋆ (γ ● δ) (⟦ γ ⟧ₛ ρ)
  CV⋆⟦ π⟨ c ⟩ ⟧ₛ        cv⋆ = cong↓⟨ c ⟩CV⋆ cv⋆
  CV⋆⟦ γ ● γ′ ⟧ₛ        cv⋆ = cong≅ₛCV⋆ (conv₁≅ₛ _ _ _)
                                        (CV⋆⟦ γ ⟧ₛ (CV⋆⟦ γ′ ⟧ₛ cv⋆))
  CV⋆⟦ [ γ , x ≔ M ] ⟧ₛ cv⋆ = cv⋆≔ {c = weak⊇}
                                   (cong≅ₛCV⋆ (trans≅ₛ (sym≅ₛ (conv₁≅ₛ _ _ _))
                                                       (cong●≅ₛ (conv₃≅ₛ _ _ _) refl≅ₛ))
                                              (CV⋆⟦ γ ⟧ₛ cv⋆))
                                   (cong≅CV (trans≅ (sym≅ (conv₇≅ _ _ _))
                                                    (cong▶≅ (conv₃≅ _ _) refl≅ₛ))
                                            (CV⟦ M ⟧ cv⋆))

-- Both lemmas are proved by induction on the proof trees using the lemmas above.
--
-- Lemma 9 is shown mutually with a corresponding lemma for `val`:

-- Lemma 9.
mutual
  lem₉ : ∀ {Γ A} {M : Γ ⊢ A} {a : Γ ⊩ A} →
           CV M a →
           M ≅ reify a
  lem₉ (cv• h) = trans≅ (sym≅ (conv₅≅ _ _))
                        (h refl⊇)
  lem₉ (cv⊃ h) = trans≅ (conv₂≅ _ _)
                        (congƛ≅ (lem₉ (h weak⊇ (aux₄₆₈ (λ c → conv₄≅ _ _ _)))))

  aux₄₆₈ : ∀ {A Γ} {M : Γ ⊢ A} {f : ∀ {Δ} → Δ ⊇ Γ → Δ ⊢ A} →
             (∀ {Δ} → (c : Δ ⊇ Γ) → M ▶ π⟨ c ⟩ ≅ f c) →
             CV M (val f)
  aux₄₆₈ {•}                 h = cv• (λ c → h c)
  aux₄₆₈ {A ⊃ B} {M = M} {f} h = cv⊃ (λ {_} {N} {a} c cvₐ →
                                       aux₄₆₈ (λ {Δ′} c′ →
                                         begin
                                           ((M ▶ π⟨ c ⟩) ∙ N) ▶ π⟨ c′ ⟩
                                         ≅⟨ conv₆≅ _ _ _ ⟩
                                           ((M ▶ π⟨ c ⟩) ▶ π⟨ c′ ⟩) ∙ (N ▶ π⟨ c′ ⟩)
                                         ≅⟨ cong∙≅ (conv₇≅ _ _ _) refl≅ ⟩
                                           (M ▶ (π⟨ c ⟩ ● π⟨ c′ ⟩)) ∙ (N ▶ π⟨ c′ ⟩)
                                         ≅⟨ cong∙≅ (cong▶≅ refl≅ (conv₄≅ₛ _ _ _)) refl≅ ⟩
                                           (M ▶ π⟨ c ○ c′ ⟩) ∙ (N ▶ π⟨ c′ ⟩)
                                         ≅⟨ cong∙≅ (h (c ○ c′)) refl≅ ⟩
                                           f (c ○ c′) ∙ (N ▶ π⟨ c′ ⟩)
                                         ≅⟨ cong∙≅ refl≅ (lem₉ (cong↑⟨ c′ ⟩CV cvₐ)) ⟩
                                           f (c ○ c′) ∙ reify (↑⟨ c′ ⟩ a)
                                         ∎))
                                         where
                                           open ≅-Reasoning

-- In order to prove Theorem 2 we also prove that `CV⋆ π⟨ c ⟩ proj⟨ c ⟩⊩⋆`; then by this, Lemma 8
-- and Lemma 9 we get that `M ▶ π⟨ c ⟩ ≅ nf M`, where `c : Γ ⊇ Γ`.  Using the conversion rule
-- `M ≅ M ▶ π⟨ c ⟩` for `c : Γ ⊇ Γ` we get by transitivity of conversion of `_≅_` that `M ≅ nf M`.

proj⟨_⟩CV⋆ : ∀ {Γ Δ} →
               (c : Δ ⊇ Γ) →
               CV⋆ π⟨ c ⟩ proj⟨ c ⟩⊩⋆
proj⟨ done ⟩CV⋆             = cv⋆[]
proj⟨ step {x = x} c i ⟩CV⋆ = cv⋆≔ {c = weak⊇}
                                   (cong≅ₛCV⋆ (conv₄≅ₛ _ _ _) (proj⟨ c ⟩CV⋆))
                                   (aux₄₆₈ (λ c′ →
                                     begin
                                       (ν x zero ▶ π⟨ step c i ⟩) ▶ π⟨ c′ ⟩
                                     ≅⟨ cong▶≅ (conv₄≅ _ _ _) refl≅ₛ ⟩
                                       ν x i ▶ π⟨ c′ ⟩
                                     ≅⟨ conv₄≅ _ _ _ ⟩
                                       ν x (↑⟨ c′ ⟩ i)
                                     ∎))
                                     where
                                       open ≅-Reasoning

reflCV⋆ : ∀ {Γ} → CV⋆ π⟨ refl⊇ ⟩ (refl⊩⋆ {Γ})
reflCV⋆ = proj⟨ refl⊇ ⟩CV⋆

aux₄₆₉⟨_⟩ : ∀ {Γ A} →
              (c : Γ ⊇ Γ) (M : Γ ⊢ A) →
              M ▶ π⟨ c ⟩ ≅ nf M
aux₄₆₉⟨ c ⟩ M rewrite uniq⊇ refl⊇ c
              = lem₉ (CV⟦ M ⟧ proj⟨ c ⟩CV⋆)

-- Theorem 2.
thm₂ : ∀ {Γ A} → (M : Γ ⊢ A) →
         M ≅ nf M
thm₂ M = trans≅ (sym≅ (conv₅≅ _ _))
                (aux₄₆₉⟨ refl⊇ ⟩ M)

-- It is now easy to prove the completeness theorem:

-- Theorem 3.
thm₃ : ∀ {Γ A} → (M M′ : Γ ⊢ A) → Eq (⟦ M ⟧ refl⊩⋆) (⟦ M′ ⟧ refl⊩⋆) →
         M ≅ M′
thm₃ M M′ eq = begin
                 M
               ≅⟨ thm₂ M ⟩
                 nf M
               ≡⟨ cor₁ M M′ eq ⟩
                 nf M′
               ≅⟨ sym≅ (thm₂ M′) ⟩
                 M′
               ∎
               where
                 open ≅-Reasoning

-- 4.7. Completeness of the conversion rules for substitutions
-- -----------------------------------------------------------
--
-- The proof of completeness above does not imply that the set of conversion rules for substitutions
-- is complete.  In order to prove the completeness of conversion rules for the substitutions
-- we define an inversion function for semantic environments:  (…)

reify⋆ : ∀ {Γ Δ} → Δ ⊩⋆ Γ → Δ ⋙ Γ
reify⋆ []            = π⟨ done ⟩
reify⋆ [ ρ , x ≔ a ] = [ reify⋆ ρ , x ≔ reify a ]

-- The normalisation function on substitutions is defined as the inversion of the semantics
-- of the substitution in the identity environment.

nf⋆ : ∀ {Δ Γ} → Δ ⋙ Γ → Δ ⋙ Γ
nf⋆ γ = reify⋆ (⟦ γ ⟧ₛ refl⊩⋆)

-- The completeness result for substitutions follows in the same way as for proof trees, i.e.,
-- we must prove that `γ ≅ₛ nf⋆ γ`.

thm₁ₛ : ∀ {Γ Δ} {ρ ρ′ : Δ ⊩⋆ Γ} → Eq⋆ ρ ρ′ → reify⋆ ρ ≡ reify⋆ ρ′
thm₁ₛ eq⋆[]         = refl
thm₁ₛ (eq⋆≔ eq⋆ eq) = cong² (λ γ M → [ γ , _ ≔ M ]) (thm₁ₛ eq⋆) (thm₁ eq)

cor₁ₛ : ∀ {Γ Δ} → (γ γ′ : Δ ⋙ Γ) → Eq⋆ (⟦ γ ⟧ₛ refl⊩⋆) (⟦ γ′ ⟧ₛ refl⊩⋆) →
          nf⋆ γ ≡ nf⋆ γ′
cor₁ₛ γ γ′ = thm₁ₛ

lem₉ₛ : ∀ {Γ Δ} {γ : Δ ⋙ Γ} {ρ : Δ ⊩⋆ Γ} →
          CV⋆ γ ρ →
          γ ≅ₛ reify⋆ ρ
lem₉ₛ cv⋆[]         = conv₆≅ₛ _ _
lem₉ₛ (cv⋆≔ cv⋆ cv) = trans≅ₛ (conv₇≅ₛ _ _ _)
                              (cong≔≅ₛ (lem₉ₛ cv⋆) (lem₉ cv))

aux₄₆₉ₛ⟨_⟩ : ∀ {Γ Δ} →
               (c : Δ ⊇ Δ) (γ : Δ ⋙ Γ) →
               γ ● π⟨ c ⟩ ≅ₛ nf⋆ γ
aux₄₆₉ₛ⟨ c ⟩ γ rewrite uniq⊇ refl⊇ c
               = lem₉ₛ (CV⋆⟦ γ ⟧ₛ proj⟨ c ⟩CV⋆)

thm₂ₛ : ∀ {Γ Δ} → (γ : Δ ⋙ Γ) →
          γ ≅ₛ nf⋆ γ
thm₂ₛ γ = trans≅ₛ (sym≅ₛ (conv₅≅ₛ _ _))
                  (aux₄₆₉ₛ⟨ refl⊇ ⟩ γ)

thm₃ₛ : ∀ {Γ Δ} → (γ γ′ : Δ ⋙ Γ) → Eq⋆ (⟦ γ ⟧ₛ refl⊩⋆) (⟦ γ′ ⟧ₛ refl⊩⋆) →
          γ ≅ₛ γ′
thm₃ₛ γ γ′ eq⋆ = begin
                   γ
                 ≅ₛ⟨ thm₂ₛ γ ⟩
                   nf⋆ γ
                 ≡⟨ cor₁ₛ γ γ′ eq⋆ ⟩
                   nf⋆ γ′
                 ≅ₛ⟨ sym≅ₛ (thm₂ₛ γ′) ⟩
                   γ′
                 ∎
                 where
                   open ≅ₛ-Reasoning

-- 4.8. Soundness of the conversion rules
-- --------------------------------------
--
-- In order to prove the soundness of the conversion rules we first have to show:

-- NOTE: Added missing uniformity assumptions.
mutual
  𝒰⟦_⟧ : ∀ {A Γ Δ} {ρ : Δ ⊩⋆ Γ} →
           (M : Γ ⊢ A) → 𝒰⋆ ρ →
           𝒰 (⟦ M ⟧ ρ)
  𝒰⟦ ν x i ⟧ u⋆ = conglookup𝒰 u⋆ i
  𝒰⟦ ƛ x M ⟧ u⋆ = 𝓊⊃ (λ c uₐ         → 𝒰⟦ M ⟧ (𝓊⋆≔ (cong↑⟨ c ⟩𝒰⋆ u⋆) uₐ))
                     (λ c eqₐ uₐ uₐ′ → Eq⟦ M ⟧ (eq⋆≔ (cong↑⟨ c ⟩Eq⋆ (reflEq⋆ u⋆)) eqₐ)
                                                (𝓊⋆≔ (cong↑⟨ c ⟩𝒰⋆ u⋆) uₐ)
                                                (𝓊⋆≔ (cong↑⟨ c ⟩𝒰⋆ u⋆) uₐ′))
                     (λ c c′ c″ uₐ   → transEq (↑⟨ c′ ⟩Eq⟦ M ⟧ (𝓊⋆≔ (cong↑⟨ c ⟩𝒰⋆ u⋆) uₐ))
                                                (Eq⟦ M ⟧ (eq⋆≔ (aux₄₂₇ c c′ c″ u⋆)
                                                               (reflEq (cong↑⟨ c′ ⟩𝒰 uₐ)))
                                                         (𝓊⋆≔ (cong↑⟨ c′ ⟩𝒰⋆ (cong↑⟨ c ⟩𝒰⋆ u⋆))
                                                              (cong↑⟨ c′ ⟩𝒰 uₐ))
                                                         (𝓊⋆≔ (cong↑⟨ c″ ⟩𝒰⋆ u⋆)
                                                              (cong↑⟨ c′ ⟩𝒰 uₐ))))
  𝒰⟦ M ∙ N ⟧ u⋆ with 𝒰⟦ M ⟧ u⋆
  𝒰⟦ M ∙ N ⟧ u⋆ | (𝓊⊃ h₀ h₁ h₂) = h₀ refl⊇ (𝒰⟦ N ⟧ u⋆)
  𝒰⟦ M ▶ γ ⟧ u⋆ = 𝒰⟦ M ⟧ (𝒰⋆⟦ γ ⟧ₛ u⋆)

  𝒰⋆⟦_⟧ₛ : ∀ {Γ Δ Θ} {ρ : Θ ⊩⋆ Δ} →
             (γ : Δ ⋙ Γ) → 𝒰⋆ ρ →
             𝒰⋆ (⟦ γ ⟧ₛ ρ)
  𝒰⋆⟦ π⟨ c ⟩ ⟧ₛ        u⋆ = cong↓⟨ c ⟩𝒰⋆ u⋆
  𝒰⋆⟦ γ ● γ′ ⟧ₛ        u⋆ = 𝒰⋆⟦ γ ⟧ₛ (𝒰⋆⟦ γ′ ⟧ₛ u⋆)
  𝒰⋆⟦ [ γ , x ≔ M ] ⟧ₛ u⋆ = 𝓊⋆≔ (𝒰⋆⟦ γ ⟧ₛ u⋆) (𝒰⟦ M ⟧ u⋆)

  Eq⟦_⟧ : ∀ {Γ Δ A} {ρ ρ′ : Δ ⊩⋆ Γ} →
            (M : Γ ⊢ A) → Eq⋆ ρ ρ′ → 𝒰⋆ ρ → 𝒰⋆ ρ′ →
            Eq (⟦ M ⟧ ρ) (⟦ M ⟧ ρ′)
  Eq⟦ ν x i ⟧ eq⋆ u⋆ u⋆′ = conglookupEq eq⋆ i
  Eq⟦ ƛ x M ⟧ eq⋆ u⋆ u⋆′ = eq⊃ (λ c uₐ → Eq⟦ M ⟧ (eq⋆≔ (cong↑⟨ c ⟩Eq⋆ eq⋆) (reflEq uₐ))
                                                  (𝓊⋆≔ (cong↑⟨ c ⟩𝒰⋆ u⋆) uₐ)
                                                  (𝓊⋆≔ (cong↑⟨ c ⟩𝒰⋆ u⋆′) uₐ))
  Eq⟦ M ∙ N ⟧ eq⋆ u⋆ u⋆′ = cong⟦∙⟧⟨ refl⊇ ⟩Eq (Eq⟦ M ⟧ eq⋆ u⋆ u⋆′) (𝒰⟦ M ⟧ u⋆) (𝒰⟦ M ⟧ u⋆′)
                                              (Eq⟦ N ⟧ eq⋆ u⋆ u⋆′) (𝒰⟦ N ⟧ u⋆) (𝒰⟦ N ⟧ u⋆′)
  Eq⟦ M ▶ γ ⟧ eq⋆ u⋆ u⋆′ = Eq⟦ M ⟧ (Eq⋆⟦ γ ⟧ₛ eq⋆ u⋆ u⋆′) (𝒰⋆⟦ γ ⟧ₛ u⋆) (𝒰⋆⟦ γ ⟧ₛ u⋆′)

  Eq⋆⟦_⟧ₛ : ∀ {Γ Δ Θ} {ρ ρ′ : Θ ⊩⋆ Δ} →
              (γ : Δ ⋙ Γ) → Eq⋆ ρ ρ′ → 𝒰⋆ ρ → 𝒰⋆ ρ′ →
              Eq⋆ (⟦ γ ⟧ₛ ρ) (⟦ γ ⟧ₛ ρ′)
  Eq⋆⟦ π⟨ c ⟩ ⟧ₛ        eq⋆ u⋆ u⋆′ = cong↓⟨ c ⟩Eq⋆ eq⋆
  Eq⋆⟦ γ ● γ′ ⟧ₛ        eq⋆ u⋆ u⋆′ = Eq⋆⟦ γ ⟧ₛ (Eq⋆⟦ γ′ ⟧ₛ eq⋆ u⋆ u⋆′) (𝒰⋆⟦ γ′ ⟧ₛ u⋆) (𝒰⋆⟦ γ′ ⟧ₛ u⋆′)
  Eq⋆⟦ [ γ , x ≔ M ] ⟧ₛ eq⋆ u⋆ u⋆′ = eq⋆≔ (Eq⋆⟦ γ ⟧ₛ eq⋆ u⋆ u⋆′)
                                          (Eq⟦ M ⟧ eq⋆ u⋆ u⋆′)

  ↑⟨_⟩Eq⟦_⟧ : ∀ {Γ Δ Θ A} {ρ : Δ ⊩⋆ Γ} →
                (c : Θ ⊇ Δ) (M : Γ ⊢ A) → 𝒰⋆ ρ →
                Eq (↑⟨ c ⟩ (⟦ M ⟧ ρ)) (⟦ M ⟧ (↑⟨ c ⟩ ρ))
  ↑⟨ c ⟩Eq⟦ ν x i ⟧ u⋆ = conglookup↑⟨ c ⟩Eq u⋆ i
  ↑⟨ c ⟩Eq⟦ ƛ x M ⟧ u⋆ = eq⊃ (λ c′ uₐ → Eq⟦ M ⟧ (eq⋆≔ (symEq⋆ (aux₄₂₇ c c′ (c ○ c′) u⋆)) (reflEq uₐ))
                                                 (𝓊⋆≔ (cong↑⟨ c ○ c′ ⟩𝒰⋆ u⋆) uₐ)
                                                 (𝓊⋆≔ (cong↑⟨ c′ ⟩𝒰⋆ (cong↑⟨ c ⟩𝒰⋆ u⋆)) uₐ))
  ↑⟨ c ⟩Eq⟦ M ∙ N ⟧ u⋆ with 𝒰⟦ M ⟧ u⋆
  ↑⟨ c ⟩Eq⟦ M ∙ N ⟧ u⋆ | (𝓊⊃ h₀ h₁ h₂) = transEq (h₂ refl⊇ c c (𝒰⟦ N ⟧ u⋆))
                                                 (transEq (aux₄₁₃ c refl⊇ (𝒰⟦ M ⟧ u⋆) (cong↑⟨ c ⟩𝒰 (𝒰⟦ N ⟧ u⋆)))
                                                          (cong⟦∙⟧⟨ refl⊇ ⟩Eq (↑⟨ c ⟩Eq⟦ M ⟧ u⋆)
                                                                              (cong↑⟨ c ⟩𝒰 (𝒰⟦ M ⟧ u⋆))
                                                                              (𝒰⟦ M ⟧ (cong↑⟨ c ⟩𝒰⋆ u⋆))
                                                                              (↑⟨ c ⟩Eq⟦ N ⟧ u⋆)
                                                                              (cong↑⟨ c ⟩𝒰 (𝒰⟦ N ⟧ u⋆))
                                                                              (𝒰⟦ N ⟧ (cong↑⟨ c ⟩𝒰⋆ u⋆))))
  ↑⟨ c ⟩Eq⟦ M ▶ γ ⟧ u⋆ = transEq (↑⟨ c ⟩Eq⟦ M ⟧ (𝒰⋆⟦ γ ⟧ₛ u⋆))
                                 (Eq⟦ M ⟧ (↑⟨ c ⟩Eq⋆⟦ γ ⟧ₛ u⋆)
                                          (cong↑⟨ c ⟩𝒰⋆ (𝒰⋆⟦ γ ⟧ₛ u⋆))
                                          (𝒰⋆⟦ γ ⟧ₛ (cong↑⟨ c ⟩𝒰⋆ u⋆)))

  ↑⟨_⟩Eq⋆⟦_⟧ₛ : ∀ {Γ Δ Θ Ω} {ρ : Θ ⊩⋆ Δ} →
                  (c : Ω ⊇ Θ) (γ : Δ ⋙ Γ) → 𝒰⋆ ρ →
                  Eq⋆ (↑⟨ c ⟩ (⟦ γ ⟧ₛ ρ)) (⟦ γ ⟧ₛ (↑⟨ c ⟩ ρ))
  ↑⟨ c ⟩Eq⋆⟦ π⟨ c′ ⟩ ⟧ₛ       u⋆ = aux₄₂₈ c′ c u⋆
  ↑⟨ c ⟩Eq⋆⟦ γ ● γ′ ⟧ₛ        u⋆ = transEq⋆ (↑⟨ c ⟩Eq⋆⟦ γ ⟧ₛ (𝒰⋆⟦ γ′ ⟧ₛ u⋆))
                                            (Eq⋆⟦ γ ⟧ₛ (↑⟨ c ⟩Eq⋆⟦ γ′ ⟧ₛ u⋆)
                                                      (cong↑⟨ c ⟩𝒰⋆ (𝒰⋆⟦ γ′ ⟧ₛ u⋆))
                                                      (𝒰⋆⟦ γ′ ⟧ₛ (cong↑⟨ c ⟩𝒰⋆ u⋆)))
  ↑⟨ c ⟩Eq⋆⟦ [ γ , x ≔ M ] ⟧ₛ u⋆ = eq⋆≔ (↑⟨ c ⟩Eq⋆⟦ γ ⟧ₛ u⋆) (↑⟨ c ⟩Eq⟦ M ⟧ u⋆)

-- NOTE: Added missing lemmas.
module _ where
  aux₄₈₁⟨_⟩ : ∀ {Γ Δ A x} {{_ : T (fresh x Γ)}} {ρ : Δ ⊩⋆ Γ} {a : Δ ⊩ A} →
                (c : [ Γ , x ∷ A ] ⊇ Γ) → 𝒰⋆ ρ →
                Eq⋆ (↓⟨ c ⟩ [ ρ , x ≔ a ]) ρ
  aux₄₈₁⟨ c ⟩ u⋆ = transEq⋆ (aux₄₂₃ refl⊇ c u⋆) (aux₄₂₄⟨ refl⊇ ⟩ u⋆)

  aux₄₈₂⟨_⟩ : ∀ {Γ Δ} {ρ : Δ ⊩⋆ Γ} →
                (c : Γ ⊇ []) → 𝒰⋆ ρ →
                ↓⟨ c ⟩ ρ ≡ []
  aux₄₈₂⟨ done ⟩ u⋆ = refl

  aux₄₈₃ : ∀ {Γ Δ} {ρ : Δ ⊩⋆ Γ} →
             (γ : Γ ⋙ []) → 𝒰⋆ ρ →
             Eq⋆ (⟦ γ ⟧ₛ ρ) []
  aux₄₈₃ π⟨ c ⟩   u⋆ rewrite aux₄₈₂⟨ c ⟩ u⋆ = reflEq⋆ 𝓊⋆[]
  aux₄₈₃ (γ ● γ′) u⋆ = aux₄₈₃ γ (𝒰⋆⟦ γ′ ⟧ₛ u⋆)

  aux₄₈₄ : ∀ {Γ Δ A x} {{_ : T (fresh x Γ)}} {ρ : Δ ⊩⋆ Γ} {a : Δ ⊩ A} →
             (i : [ Γ , x ∷ A ] ∋ x ∷ A) → 𝒰 a →
             Eq (lookup [ ρ , x ≔ a ] i) a
  aux₄₈₄ i uₐ rewrite uniq∋ i zero = reflEq uₐ

  conv₆Eq⋆⟨_⟩ : ∀ {Γ Δ} {ρ : Δ ⊩⋆ Γ} →
                  (c : Γ ⊇ []) (γ : Γ ⋙ []) → 𝒰⋆ ρ →
                  Eq⋆ (⟦ γ ⟧ₛ ρ) (↓⟨ c ⟩⊩⋆ ρ)
  conv₆Eq⋆⟨ c ⟩ γ u⋆ rewrite aux₄₈₂⟨ c ⟩ u⋆ = aux₄₈₃ γ u⋆

  conv₇Eq⋆⟨_⟩ : ∀ {Γ Δ Θ A x} {{_ : T (fresh x Γ)}} {ρ : Θ ⊩⋆ Δ} →
                  (c : [ Γ , x ∷ A ] ⊇ Γ) (γ : Δ ⋙ [ Γ , x ∷ A ]) (i : [ Γ , x ∷ A ] ∋ x ∷ A) → 𝒰⋆ ρ →
                  Eq⋆ (⟦ γ ⟧ₛ ρ) [ ↓⟨ c ⟩ (⟦ γ ⟧ₛ ρ) , x ≔ lookup (⟦ γ ⟧ₛ ρ) i ]
  conv₇Eq⋆⟨_⟩ {x = x} {ρ = ρ} c γ i u⋆ with ⟦ γ ⟧ₛ ρ | 𝒰⋆⟦ γ ⟧ₛ u⋆
  conv₇Eq⋆⟨_⟩ {x = x} {ρ = ρ} c γ i u⋆ | [ ρ′ , .x ≔ a ] | 𝓊⋆≔ u⋆′ uₐ =
    begin
      [ ρ′ , x ≔ a ]
    Eq⋆⟨ eq⋆≔ (symEq⋆ (aux₄₈₁⟨ c ⟩ u⋆′)) (symEq (aux₄₈₄ i uₐ)) ⟩
      [ ↓⟨ c ⟩⊩⋆ [ ρ′ , x ≔ a ] , x ≔ lookup [ ρ′ , x ≔ a ] i ]
    ∎⟨ 𝓊⋆≔ (cong↓⟨ c ⟩𝒰⋆ (𝓊⋆≔ u⋆′ uₐ)) (conglookup𝒰 (𝓊⋆≔ u⋆′ uₐ) i) ⟩
   where
     open Eq⋆Reasoning

-- The soundness theorem is shown mutually with a corresponding lemma for substitutions:

-- Theorem 4.
-- NOTE: Added missing uniformity assumptions.
module _ {{_ : Model}} where
  mutual
    Eq⟦_⟧≅ : ∀ {Γ A w} {M M′ : Γ ⊢ A} {ρ : w ⊩⋆ Γ} →
               M ≅ M′ → 𝒰⋆ ρ →
               Eq (⟦ M ⟧ ρ) (⟦ M′ ⟧ ρ)
    Eq⟦ refl≅ {M = M} ⟧≅                     u⋆ = reflEq (𝒰⟦ M ⟧ u⋆)
    Eq⟦ sym≅ p ⟧≅                            u⋆ = symEq (Eq⟦ p ⟧≅ u⋆)
    Eq⟦ trans≅ p p′ ⟧≅                       u⋆ = transEq (Eq⟦ p ⟧≅ u⋆) (Eq⟦ p′ ⟧≅ u⋆)
    Eq⟦ congƛ≅ {M = M} {M′} p ⟧≅             u⋆ = eq⊃ (λ c uₐ → Eq⟦ p ⟧≅ (𝓊⋆≔ (cong↑⟨ c ⟩𝒰⋆ u⋆) uₐ))
    Eq⟦ cong∙≅ {M = M} {M′} {N} {N′} p p′ ⟧≅ u⋆ = cong⟦∙⟧⟨ refl⊇ ⟩Eq (Eq⟦ p ⟧≅ u⋆)
                                                                     (𝒰⟦ M ⟧ u⋆)
                                                                     (𝒰⟦ M′ ⟧ u⋆)
                                                                     (Eq⟦ p′ ⟧≅ u⋆)
                                                                     (𝒰⟦ N ⟧ u⋆)
                                                                     (𝒰⟦ N′ ⟧ u⋆)
    Eq⟦ cong▶≅ {M = M} {M′} {γ} {γ′} p pₛ ⟧≅ u⋆ = transEq (Eq⟦ M ⟧ (Eq⋆⟦ pₛ ⟧≅ₛ u⋆) (𝒰⋆⟦ γ ⟧ₛ u⋆) (𝒰⋆⟦ γ′ ⟧ₛ u⋆))
                                                          (transEq (Eq⟦ p ⟧≅ (𝒰⋆⟦ γ′ ⟧ₛ u⋆))
                                                                   (reflEq (𝒰⟦ M′ ⟧ (𝒰⋆⟦ γ′ ⟧ₛ u⋆))))
    Eq⟦ conv₁≅ M N γ ⟧≅                      u⋆ = Eq⟦ M ⟧ (eq⋆≔ (aux₄₂₅⟨ refl⊇ ⟩ (𝒰⋆⟦ γ ⟧ₛ u⋆))
                                                                (reflEq (𝒰⟦ N ⟧ u⋆)))
                                                          (𝓊⋆≔ (cong↑⟨ refl⊇ ⟩𝒰⋆ (𝒰⋆⟦ γ ⟧ₛ u⋆))
                                                               (𝒰⟦ N ⟧ u⋆))
                                                          (𝓊⋆≔ (𝒰⋆⟦ γ ⟧ₛ u⋆)
                                                               (𝒰⟦ N ⟧ u⋆))
    Eq⟦_⟧≅ {ρ = ρ} (conv₂≅ {x = x} c M) u⋆ =
      eq⊃ (λ c′ {a} uₐ →
        begin
          ⟦ M ⟧ ρ ⟦∙⟧⟨ c′ ⟩ a
        Eq⟨ aux₄₁₃ c′ refl⊇ (𝒰⟦ M ⟧ u⋆) uₐ ⟩
          (↑⟨ c′ ⟩ (⟦ M ⟧ ρ) ⟦∙⟧⟨ refl⊇ ⟩ a)
        Eq⟨ cong⟦∙⟧⟨ refl⊇ ⟩Eq (↑⟨ c′ ⟩Eq⟦ M ⟧ u⋆)
                               (cong↑⟨ c′ ⟩𝒰 (𝒰⟦ M ⟧ u⋆))
                               (𝒰⟦ M ⟧ (cong↑⟨ c′ ⟩𝒰⋆ u⋆))
                               (reflEq uₐ) uₐ uₐ ⟩
          ⟦ M ⟧ (↑⟨ c′ ⟩ ρ) ⟦∙⟧⟨ refl⊇ ⟩ a
        Eq⟨ cong⟦∙⟧⟨ refl⊇ ⟩Eq (Eq⟦ M ⟧ (symEq⋆ (aux₄₈₁⟨ c ⟩ (cong↑⟨ c′ ⟩𝒰⋆ u⋆)))
                                        (cong↑⟨ c′ ⟩𝒰⋆ u⋆)
                                        (cong↓⟨ c ⟩𝒰⋆ (𝓊⋆≔ (cong↑⟨ c′ ⟩𝒰⋆ u⋆) uₐ)))
                               (𝒰⟦ M ⟧ (cong↑⟨ c′ ⟩𝒰⋆ u⋆))
                               (𝒰⟦ M ⟧ (cong↓⟨ c ⟩𝒰⋆ (𝓊⋆≔ (cong↑⟨ c′ ⟩𝒰⋆ u⋆) uₐ)))
                               (reflEq uₐ) uₐ uₐ ⟩
          ⟦ M ⟧ (↓⟨ c ⟩ [ ↑⟨ c′ ⟩ ρ , x ≔ a ]) ⟦∙⟧⟨ refl⊇ ⟩ a
        ∎⟨ case (𝒰⟦ M ⟧ (cong↓⟨ c ⟩𝒰⋆ (𝓊⋆≔ (cong↑⟨ c′ ⟩𝒰⋆ u⋆) uₐ))) of
             (λ { (𝓊⊃ h₀ h₁ h₂) → h₀ refl⊇ uₐ }) ⟩)
        where
          open EqReasoning
    Eq⟦ conv₃≅ M γ ⟧≅                        u⋆ = reflEq (𝒰⟦ M ⟧ u⋆)
    Eq⟦ conv₄≅ c i j ⟧≅                      u⋆ = symEq (aux₄₂₁⟨ c ⟩ u⋆ j i)
    Eq⟦ conv₅≅ c M ⟧≅                        u⋆ = Eq⟦ M ⟧ (aux₄₂₄⟨ c ⟩ u⋆) (cong↓⟨ c ⟩𝒰⋆ u⋆) u⋆
    Eq⟦ conv₆≅ M N γ ⟧≅                      u⋆ = cong⟦∙⟧⟨ refl⊇ ⟩Eq (reflEq (𝒰⟦ M ⟧ (𝒰⋆⟦ γ ⟧ₛ u⋆)))
                                                                     (𝒰⟦ M ⟧ (𝒰⋆⟦ γ ⟧ₛ u⋆))
                                                                     (𝒰⟦ M ⟧ (𝒰⋆⟦ γ ⟧ₛ u⋆))
                                                                     (reflEq (𝒰⟦ N ⟧ (𝒰⋆⟦ γ ⟧ₛ u⋆)))
                                                                     (𝒰⟦ N ⟧ (𝒰⋆⟦ γ ⟧ₛ u⋆))
                                                                     (𝒰⟦ N ⟧ (𝒰⋆⟦ γ ⟧ₛ u⋆))
    Eq⟦ conv₇≅ M γ δ ⟧≅                      u⋆ = reflEq (𝒰⟦ M ⟧ (𝒰⋆⟦ γ ⟧ₛ (𝒰⋆⟦ δ ⟧ₛ u⋆)))

    Eq⋆⟦_⟧≅ₛ : ∀ {Γ Δ w} {γ γ′ : Γ ⋙ Δ} {ρ : w ⊩⋆ Γ} →
                 γ ≅ₛ γ′ → 𝒰⋆ ρ →
                 Eq⋆ (⟦ γ ⟧ₛ ρ) (⟦ γ′ ⟧ₛ ρ)
    Eq⋆⟦ refl≅ₛ {γ = γ} ⟧≅ₛ                    u⋆ = reflEq⋆ (𝒰⋆⟦ γ ⟧ₛ u⋆)
    Eq⋆⟦ sym≅ₛ pₛ ⟧≅ₛ                          u⋆ = symEq⋆ (Eq⋆⟦ pₛ ⟧≅ₛ u⋆)
    Eq⋆⟦ trans≅ₛ pₛ pₛ′ ⟧≅ₛ                    u⋆ = transEq⋆ (Eq⋆⟦ pₛ ⟧≅ₛ u⋆) (Eq⋆⟦ pₛ′ ⟧≅ₛ u⋆)
    Eq⋆⟦ cong●≅ₛ {γ′ = γ′} {δ} {δ′} pₛ pₛ′ ⟧≅ₛ u⋆ = transEq⋆ (Eq⋆⟦ pₛ ⟧≅ₛ (𝒰⋆⟦ δ ⟧ₛ u⋆))
                                                             (Eq⋆⟦ γ′ ⟧ₛ (Eq⋆⟦ pₛ′ ⟧≅ₛ u⋆)
                                                                         (𝒰⋆⟦ δ ⟧ₛ u⋆)
                                                                         (𝒰⋆⟦ δ′ ⟧ₛ u⋆))
    Eq⋆⟦ cong≔≅ₛ pₛ p ⟧≅ₛ                      u⋆ = eq⋆≔ (Eq⋆⟦ pₛ ⟧≅ₛ u⋆) (Eq⟦ p ⟧≅ u⋆)
    Eq⋆⟦ conv₁≅ₛ γ δ θ ⟧≅ₛ                     u⋆ = reflEq⋆ (𝒰⋆⟦ γ ⟧ₛ (𝒰⋆⟦ δ ⟧ₛ (𝒰⋆⟦ θ ⟧ₛ u⋆)))
    Eq⋆⟦ conv₂≅ₛ M γ δ ⟧≅ₛ                     u⋆ = reflEq⋆ (𝓊⋆≔ (𝒰⋆⟦ γ ⟧ₛ (𝒰⋆⟦ δ ⟧ₛ u⋆))
                                                                 (𝒰⟦ M ⟧ (𝒰⋆⟦ δ ⟧ₛ u⋆)))
    Eq⋆⟦ conv₃≅ₛ c M γ ⟧≅ₛ                     u⋆ = transEq⋆ (aux₄₂₃ refl⊇ c (𝒰⋆⟦ γ ⟧ₛ u⋆))
                                                             (aux₄₂₄⟨ refl⊇ ⟩ (𝒰⋆⟦ γ ⟧ₛ u⋆))
    Eq⋆⟦ conv₄≅ₛ c c′ c″ ⟧≅ₛ                   u⋆ = aux₄₂₆ c′ c″ c u⋆
    Eq⋆⟦ conv₅≅ₛ c γ ⟧≅ₛ                       u⋆ = Eq⋆⟦ γ ⟧ₛ (aux₄₂₄⟨ c ⟩ u⋆) (cong↓⟨ c ⟩𝒰⋆ u⋆) u⋆
    Eq⋆⟦ conv₆≅ₛ c γ ⟧≅ₛ                       u⋆ = conv₆Eq⋆⟨ c ⟩ γ u⋆
    Eq⋆⟦ conv₇≅ₛ c γ i ⟧≅ₛ                     u⋆ = conv₇Eq⋆⟨ c ⟩ γ i u⋆

-- They are both shown by induction on the rules of conversion.  Notice that the soundness
-- result holds in any Kripke model.

-- 4.9. Decision algorithm for conversion
-- --------------------------------------
--
-- We now have a decision algorithm for testing convertibility between proof trees: compute
-- the normal form and check if they are exactly the same.  This decision algorithm is correct,
-- since by Theorem 2 we have `M ≅ nf M` and `M′ ≅ nf M′` and, by hypothesis, `nf M ≡ nf M′`,
-- we get by transitivity of `_≅_`, that `M ≅ M′`.

-- Theorem 5.
thm₅ : ∀ {Γ A} → (M M′ : Γ ⊢ A) → nf M ≡ nf M′ → M ≅ M′
thm₅ M M′ p = begin
                M
              ≅⟨ thm₂ M ⟩
                nf M
              ≡⟨ p ⟩
                nf M′
              ≅⟨ sym≅ (thm₂ M′) ⟩
                M′
              ∎
              where
                open ≅-Reasoning

-- The decision algorithm is also complete since by Theorem 4 and the hypothesis, `M ≅ M′`, we get
-- `Eq (⟦ M ⟧ refl⊩⋆) (⟦ N ⟧ refl⊩⋆)` and by Corollary 1 we get `nf M ≡ nf N`.

-- NOTE: Added missing lemmas.
module _ where
  proj⟨_⟩𝒰⋆ : ∀ {Γ Δ} →
                (c : Δ ⊇ Γ) →
                𝒰⋆ proj⟨ c ⟩⊩⋆
  proj⟨ done ⟩𝒰⋆     = 𝓊⋆[]
  proj⟨ step c i ⟩𝒰⋆ = 𝓊⋆≔ proj⟨ c ⟩𝒰⋆ (⟦ν⟧𝒰 i)

  refl𝒰⋆ : ∀ {Γ} → 𝒰⋆ (refl⊩⋆ {Γ})
  refl𝒰⋆ = proj⟨ refl⊇ ⟩𝒰⋆

-- Theorem 6.
thm₆ : ∀ {Γ A} → (M M′ : Γ ⊢ A) → M ≅ M′ → nf M ≡ nf M′
thm₆ M M′ p = cor₁ M M′ (Eq⟦ p ⟧≅ refl𝒰⋆)


text:
module CombinatoryLogic.Forest where

open import Data.Product using (_,_)
open import Function using (_$_)
open import Mockingbird.Forest using (Forest)

open import CombinatoryLogic.Equality as Equality using (isEquivalence; cong)
open import CombinatoryLogic.Semantics as ⊢ using (_≈_)
open import CombinatoryLogic.Syntax as Syntax using (Combinator)

forest : Forest
forest = record
  { Bird = Combinator
  ; _≈_ = _≈_
  ; _∙_ = Syntax._∙_
  ; isForest = record
    { isEquivalence = isEquivalence
    ; cong = cong
    }
  }

open Forest forest

open import Mockingbird.Forest.Birds forest
open import Mockingbird.Forest.Extensionality forest
import Mockingbird.Problems.Chapter11 forest as Chapter₁₁
import Mockingbird.Problems.Chapter12 forest as Chapter₁₂

instance
  hasWarbler : HasWarbler
  hasWarbler = record
    { W = Syntax.W
    ; isWarbler = λ _ _ → ⊢.W
    }

  hasKestrel : HasKestrel
  hasKestrel = record
    { K = Syntax.K
    ; isKestrel = λ _ _ → ⊢.K
    }

  hasBluebird : HasBluebird
  hasBluebird = record
    { B = Syntax.B
    ; isBluebird = λ _ _ _ → ⊢.B
    }

  hasIdentity : HasIdentity
  hasIdentity = record
    { I = Syntax.I
    ; isIdentity = λ _ → Equality.prop₉
    }

  hasMockingbird : HasMockingbird
  hasMockingbird = Chapter₁₁.problem₁₄

  hasLark : HasLark
  hasLark = Chapter₁₂.problem₃

  hasComposition : HasComposition
  hasComposition = Chapter₁₁.problem₁

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.TotalFiber where

open import Cubical.Core.Everything
open import Cubical.Data.Prod
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Surjection
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.HITs.PropositionalTruncation

private
  variable
    ℓ ℓ' : Level

module _ {A : Type ℓ} {B : Type ℓ'} (f : A → B) where
  private
    ℓ'' : Level
    ℓ'' = ℓ-max ℓ ℓ'

    LiftA : Type ℓ''
    LiftA = Lift {j = ℓ'} A

  Total-fiber : Type ℓ''
  Total-fiber = Σ B \ b → fiber f b

  A→Total-fiber : A → Total-fiber
  A→Total-fiber a = f a , a , refl

  Total-fiber→A : Total-fiber → A
  Total-fiber→A (b , a , p) = a

  Total-fiber→A→Total-fiber : ∀ t → A→Total-fiber (Total-fiber→A t) ≡ t
  Total-fiber→A→Total-fiber (b , a , p) i = p i , a , λ j → p (i ∧ j)

  A→Total-fiber→A : ∀ a → Total-fiber→A (A→Total-fiber a) ≡ a
  A→Total-fiber→A a = refl

  LiftA→Total-fiber : LiftA → Total-fiber
  LiftA→Total-fiber x = A→Total-fiber (lower x)

  Total-fiber→LiftA : Total-fiber → LiftA
  Total-fiber→LiftA x = lift (Total-fiber→A x)

  Total-fiber→LiftA→Total-fiber : ∀ t → LiftA→Total-fiber (Total-fiber→LiftA t) ≡ t
  Total-fiber→LiftA→Total-fiber (b , a , p) i = p i , a , λ j → p (i ∧ j)

  LiftA→Total-fiber→LiftA : ∀ a → Total-fiber→LiftA (LiftA→Total-fiber a) ≡ a
  LiftA→Total-fiber→LiftA a = refl

  A≡Total : Lift A ≡ Total-fiber
  A≡Total = isoToPath (iso
    LiftA→Total-fiber
    Total-fiber→LiftA
    Total-fiber→LiftA→Total-fiber
    LiftA→Total-fiber→LiftA)

  -- HoTT Lemma 4.8.2
  A≃Total : Lift A ≃ Total-fiber
  A≃Total = isoToEquiv (iso
    LiftA→Total-fiber
    Total-fiber→LiftA
    Total-fiber→LiftA→Total-fiber
    LiftA→Total-fiber→LiftA)

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module LC.Simultanuous where

open import LC.Base
open import LC.Subst
open import LC.Reduction

open import Data.Nat
open import Relation.Binary.Construct.Closure.ReflexiveTransitive

-- open import Relation.Binary.PropositionalEquality hiding ([_]; preorder)

-- infixl 4 _*
-- data _* : Term → Set where
--     *-var : (M : Term) → M *
--     *-ƛ : ∀ {M} → ƛ M * → M *
--     *-∙ : ∀ {M N} → M ∙ N * → M * ∙ N *

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Categories.Sets where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation

open Precategory

module _ ℓ where
  SET : Precategory (ℓ-suc ℓ) ℓ
  SET .ob = Σ (Type ℓ) isSet
  SET .Hom[_,_] (A , _) (B , _) = A → B
  SET .id _  = λ x → x
  SET ._⋆_ f g = λ x → g (f x)
  SET .⋆IdL f = refl
  SET .⋆IdR f = refl
  SET .⋆Assoc f g h = refl

module _ {ℓ} where
  isSetExpIdeal : {A B : Type ℓ} → isSet B → isSet (A → B)
  isSetExpIdeal B/set = isSetΠ λ _ → B/set

  isSetLift : {A : Type ℓ} → isSet A → isSet (Lift {ℓ} {ℓ-suc ℓ} A)
  isSetLift = isOfHLevelLift 2

  module _ {A B : SET ℓ .ob} where
    -- monic/surjectiveness
    open import Cubical.Categories.Morphism
    isSurjSET : (f : SET ℓ [ A , B ]) → Type _
    isSurjSET f = ∀ (b : fst B) → Σ[ a ∈ fst A ] f a ≡ b

    -- isMonic→isSurjSET : {f : SET ℓ [ A , B ]}
    --                   → isEpic {C = SET ℓ} {x = A} {y = B} f
    --                   → isSurjSET f
    -- isMonic→isSurjSET ism b = {!!} , {!!}

  instance
    SET-category : isCategory (SET ℓ)
    SET-category .isSetHom {_} {B , B/set} = isSetExpIdeal B/set

private
  variable
    ℓ ℓ' : Level

open Functor

-- Hom functors
_[-,_] : (C : Precategory ℓ ℓ') → (c : C .ob) → ⦃ isCat : isCategory C ⦄ → Functor (C ^op) (SET _)
(C [-, c ]) ⦃ isCat ⦄ .F-ob x = (C [ x , c ]) , isCat .isSetHom
(C [-, c ])           .F-hom f k = f ⋆⟨ C ⟩ k
(C [-, c ])           .F-id = funExt λ _ → C .⋆IdL _
(C [-, c ])           .F-seq _ _ = funExt λ _ → C .⋆Assoc _ _ _

_[_,-] : (C : Precategory ℓ ℓ') → (c : C .ob) → ⦃ isCat : isCategory C ⦄ → Functor C (SET _)
(C [ c ,-]) ⦃ isCat ⦄ .F-ob x = (C [ c , x ]) , isCat .isSetHom
(C [ c ,-])           .F-hom f k = k ⋆⟨ C ⟩ f
(C [ c ,-])           .F-id = funExt λ _ → C .⋆IdR _
(C [ c ,-])           .F-seq _ _ = funExt λ _ → sym (C .⋆Assoc _ _ _)

module _ {C : Precategory ℓ ℓ'} ⦃ _ : isCategory C ⦄ {F : Functor C (SET ℓ')} where
  open NatTrans

  -- natural transformations by pre/post composition
  preComp : {x y : C .ob}
          → (f : C [ x , y ])
          → C [ x ,-] ⇒ F
          → C [ y ,-] ⇒ F
  preComp f α .N-ob c k = (α ⟦ c ⟧) (f ⋆⟨ C ⟩ k)
  preComp f α .N-hom {x = c} {d} k
    = (λ l → (α ⟦ d ⟧) (f ⋆⟨ C ⟩ (l ⋆⟨ C ⟩ k)))
    ≡[ i ]⟨ (λ l → (α ⟦ d ⟧) (⋆Assoc C f l k (~ i))) ⟩
      (λ l → (α ⟦ d ⟧) (f ⋆⟨ C ⟩ l ⋆⟨ C ⟩ k))
    ≡[ i ]⟨ (λ l → (α .N-hom k) i (f ⋆⟨ C ⟩ l)) ⟩
      (λ l → (F ⟪ k ⟫) ((α ⟦ c ⟧) (f ⋆⟨ C ⟩ l)))
    ∎

-- properties
-- TODO: move to own file
open CatIso renaming (inv to cInv)
open Iso

Iso→CatIso : ∀ {A B : (SET ℓ) .ob}
           → Iso (fst A) (fst B)
           → CatIso {C = SET ℓ} A B
Iso→CatIso is .mor = is .fun
Iso→CatIso is .cInv = is .inv
Iso→CatIso is .sec = funExt λ b → is .rightInv b -- is .rightInv
Iso→CatIso is .ret = funExt λ b → is .leftInv b -- is .rightInv

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Relator.Equals where

import      Lvl
open import Logic
open import Logic.Propositional
open import Type

infixl 15 _≢_

open import Type.Identity public
  using()
  renaming(Id to infixl 15 _≡_ ; intro to [≡]-intro)

_≢_ : ∀{ℓ}{T} → T → T → Stmt{ℓ}
a ≢ b = ¬(a ≡ b)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- Strictly descending lists
------------------------------------------------------------------------

{-# OPTIONS --cubical --no-import-sorts --safe #-}

open import Cubical.Core.Everything

module Cubical.Data.DescendingList.Strict
 (A : Type₀)
 (_>_ : A → A → Type₀)
 where

open import Cubical.Data.DescendingList.Base A _>_ renaming (_≥ᴴ_ to _>ᴴ_; ≥ᴴ[] to >ᴴ[]; ≥ᴴcons to >ᴴcons; DL to SDL) using ([]; cons) public


text:
-- Andreas, 2019-12-08, issue #4267, reported and test case by csattler

-- Problem: definitions from files (A1) imported by a module
-- (Issue4267) may leak into the handling of an independent module
-- (B).

-- The root issue here is that having a signature stImports that
-- simply accumulates the signatures of all visited modules is
-- unhygienic.

module Issue4267 where

open import Issue4267.A0
open import Issue4267.A1 -- importing A1 here (in main) affects how B is type-checked
open import Issue4267.B

-- After the fix of #4267, these imports should succeed without unsolved metas.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- Some results related to the For-iterated-equality predicate
-- transformer
------------------------------------------------------------------------

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

open import Equality

module For-iterated-equality
  {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection eq as Bijection using (_↔_)
open import Equivalence eq as Eq using (_≃_)
open import Equivalence.Erased eq as EEq using (_≃ᴱ_)
open import Function-universe eq as F hiding (id; _∘_)
open import H-level eq
open import List eq
open import Nat eq
open import Surjection eq as Surj using (_↠_)

private
  variable
    a b ℓ p q : Level
    A B       : Type a
    P Q R     : Type p → Type p
    x y       : A
    k         : Kind
    n         : ℕ

------------------------------------------------------------------------
-- Some lemmas related to nested occurrences of For-iterated-equality

-- Nested uses of For-iterated-equality can be merged.

For-iterated-equality-For-iterated-equality′ :
  {A : Type a} →
  ∀ m n →
  For-iterated-equality m (For-iterated-equality n P) A ↝[ a ∣ a ]
  For-iterated-equality (m + n) P A
For-iterated-equality-For-iterated-equality′ zero _ _ = F.id

For-iterated-equality-For-iterated-equality′ {P = P} {A = A}
                                             (suc m) n ext =
  ((x y : A) →
   For-iterated-equality m (For-iterated-equality n P) (x ≡ y))  ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                     For-iterated-equality-For-iterated-equality′ m n ext) ⟩□
  ((x y : A) → For-iterated-equality (m + n) P (x ≡ y))          □

-- A variant of the previous result.

For-iterated-equality-For-iterated-equality :
  {A : Type a} →
  ∀ m n →
  For-iterated-equality m (For-iterated-equality n P) A ↝[ a ∣ a ]
  For-iterated-equality (n + m) P A
For-iterated-equality-For-iterated-equality {P = P} {A = A}
                                            m n ext =
  For-iterated-equality m (For-iterated-equality n P) A  ↝⟨ For-iterated-equality-For-iterated-equality′ m n ext ⟩
  For-iterated-equality (m + n) P A                      ↝⟨ ≡⇒↝ _ $ cong (λ n → For-iterated-equality n P A) (+-comm m) ⟩□
  For-iterated-equality (n + m) P A                      □

------------------------------------------------------------------------
-- Preservation lemmas for For-iterated-equality

-- A preservation lemma for the predicate.

For-iterated-equality-cong₁ :
  {P Q : Type ℓ → Type ℓ} →
  Extensionality? k ℓ ℓ →
  ∀ n →
  (∀ {A} → P A ↝[ k ] Q A) →
  For-iterated-equality n P A ↝[ k ] For-iterated-equality n Q A
For-iterated-equality-cong₁ _ zero P↝Q = P↝Q

For-iterated-equality-cong₁ {A = A} {P = P} {Q = Q} ext (suc n) P↝Q =
  ((x y : A) → For-iterated-equality n P (x ≡ y))  ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ →
                                                       For-iterated-equality-cong₁ ext n P↝Q) ⟩□
  ((x y : A) → For-iterated-equality n Q (x ≡ y))  □

-- A variant of For-iterated-equality-cong₁.

For-iterated-equality-cong₁ᴱ-→ :
  {@0 A : Type ℓ} {@0 P Q : Type ℓ → Type ℓ} →
  ∀ n →
  (∀ {@0 A} → P A → Q A) →
  For-iterated-equality n P A → For-iterated-equality n Q A
For-iterated-equality-cong₁ᴱ-→ zero P→Q = P→Q

For-iterated-equality-cong₁ᴱ-→ {A = A} {P = P} {Q = Q} (suc n) P→Q =
  ((x y : A) → For-iterated-equality n P (x ≡ y))  →⟨ For-iterated-equality-cong₁ᴱ-→ n (λ {A} → P→Q {A = A}) ∘_ ∘_ ⟩□
  ((x y : A) → For-iterated-equality n Q (x ≡ y))  □

-- Preservation lemmas for both the predicate and the type.

For-iterated-equality-cong-→ :
  ∀ n →
  (∀ {A B} → A ↠ B → P A → Q B) →
  A ↠ B →
  For-iterated-equality n P A → For-iterated-equality n Q B
For-iterated-equality-cong-→ zero P↝Q A↠B = P↝Q A↠B

For-iterated-equality-cong-→ {P = P} {Q = Q} {A = A} {B = B}
                             (suc n) P↝Q A↠B =
  ((x y : A) → For-iterated-equality n P (x ≡ y))  ↝⟨ (Π-cong-contra-→ (_↠_.from A↠B) λ _ → Π-cong-contra-→ (_↠_.from A↠B) λ _ →
                                                       For-iterated-equality-cong-→ n P↝Q $ Surj.↠-≡ A↠B) ⟩□
  ((x y : B) → For-iterated-equality n Q (x ≡ y))  □

For-iterated-equality-cong :
  {P : Type p → Type p} {Q : Type q → Type q} →
  Extensionality? k (p ⊔ q) (p ⊔ q) →
  ∀ n →
  (∀ {A B} → A ↔ B → P A ↝[ k ] Q B) →
  A ↔ B →
  For-iterated-equality n P A ↝[ k ] For-iterated-equality n Q B
For-iterated-equality-cong _ zero P↝Q A↔B = P↝Q A↔B

For-iterated-equality-cong {A = A} {B = B} {P = P} {Q = Q}
                           ext (suc n) P↝Q A↔B =
  ((x y : A) → For-iterated-equality n P (x ≡ y))  ↝⟨ (Π-cong ext A↔B λ _ → Π-cong ext A↔B λ _ →
                                                       For-iterated-equality-cong ext n P↝Q $ inverse $ _≃_.bijection $
                                                       Eq.≃-≡ $ from-isomorphism A↔B) ⟩□
  ((x y : B) → For-iterated-equality n Q (x ≡ y))  □

------------------------------------------------------------------------
-- Some "closure properties" for the type

private

  -- A lemma.

  lift≡lift↔ : lift {ℓ = ℓ} x ≡ lift y ↔ x ≡ y
  lift≡lift↔ = inverse $ _≃_.bijection $ Eq.≃-≡ $ Eq.↔⇒≃ Bijection.↑↔

-- Closure properties for ⊤.

For-iterated-equality-↑-⊤ :
  Extensionality? k ℓ ℓ →
  ∀ n →
  (∀ {A B} → A ↔ B → P A ↝[ k ] P B) →
  P (↑ ℓ ⊤) ↝[ k ] For-iterated-equality n P (↑ ℓ ⊤)
For-iterated-equality-↑-⊤ _ zero _ = F.id

For-iterated-equality-↑-⊤ {P = P} ext (suc n) resp =
  P (↑ _ ⊤)                                                ↝⟨ For-iterated-equality-↑-⊤ ext n resp ⟩
  For-iterated-equality n P (↑ _ ⊤)                        ↝⟨ For-iterated-equality-cong ext n resp $
                                                              inverse lift≡lift↔ F.∘ inverse tt≡tt↔⊤ F.∘ Bijection.↑↔ ⟩
  For-iterated-equality n P (lift tt ≡ lift tt)            ↝⟨ inverse-ext? (λ ext → drop-⊤-left-Π ext Bijection.↑↔) ext ⟩
  ((y : ↑ _ ⊤) → For-iterated-equality n P (lift tt ≡ y))  ↝⟨ inverse-ext? (λ ext → drop-⊤-left-Π ext Bijection.↑↔) ext ⟩□
  ((x y : ↑ _ ⊤) → For-iterated-equality n P (x ≡ y))      □

For-iterated-equality-⊤ :
  Extensionality? k lzero lzero →
  ∀ n →
  (∀ {A B} → A ↔ B → P A ↝[ k ] P B) →
  P ⊤ ↝[ k ] For-iterated-equality n P ⊤
For-iterated-equality-⊤ {P = P} ext n resp =
  P ⊤                                ↝⟨ resp (inverse Bijection.↑↔) ⟩
  P (↑ _ ⊤)                          ↝⟨ For-iterated-equality-↑-⊤ ext n resp ⟩
  For-iterated-equality n P (↑ _ ⊤)  ↝⟨ For-iterated-equality-cong ext n resp Bijection.↑↔ ⟩□
  For-iterated-equality n P ⊤        □

-- Closure properties for ⊥.

For-iterated-equality-suc-⊥ :
  {P : Type p → Type p} →
  ∀ n → ⊤ ↝[ p ∣ p ] For-iterated-equality (suc n) P ⊥
For-iterated-equality-suc-⊥ {P = P} n ext =
  ⊤                                                ↝⟨ inverse-ext? Π⊥↔⊤ ext ⟩□
  ((x y : ⊥) → For-iterated-equality n P (x ≡ y))  □

For-iterated-equality-⊥ :
  {P : Type p → Type p} →
  Extensionality? k p p →
  ∀ n →
  ⊤ ↝[ k ] P ⊥ →
  ⊤ ↝[ k ] For-iterated-equality n P ⊥
For-iterated-equality-⊥ _   zero      = id
For-iterated-equality-⊥ ext (suc n) _ =
  For-iterated-equality-suc-⊥ n ext

-- A closure property for Π.

For-iterated-equality-Π :
  {A : Type a} {B : A → Type b} →
  Extensionality a b →
  ∀ n →
  (∀ {A B} → A ↔ B → Q A → Q B) →
  ({A : Type a} {B : A → Type b} →
   (∀ x → P (B x)) → Q (∀ x → B x)) →
  (∀ x → For-iterated-equality n P (B x)) →
  For-iterated-equality n Q (∀ x → B x)
For-iterated-equality-Π _ zero _ hyp = hyp

For-iterated-equality-Π {Q = Q} {P = P} {B = B} ext (suc n) resp hyp =
  (∀ x (y z : B x) → For-iterated-equality n P (y ≡ z))              ↝⟨ (λ hyp _ _ _ → hyp _ _ _) ⟩
  (∀ (f g : ∀ x → B x) x → For-iterated-equality n P (f x ≡ g x))    ↝⟨ (∀-cong _ λ _ → ∀-cong _ λ _ → For-iterated-equality-Π ext n resp hyp) ⟩
  ((f g : ∀ x → B x) → For-iterated-equality n Q (∀ x → f x ≡ g x))  ↝⟨ (∀-cong _ λ _ → ∀-cong _ λ _ → For-iterated-equality-cong _ n resp $
                                                                         from-isomorphism $ Eq.extensionality-isomorphism ext) ⟩□
  ((f g : ∀ x → B x) → For-iterated-equality n Q (f ≡ g))            □

-- A closure property for Σ.

For-iterated-equality-Σ :
  {A : Type a} {B : A → Type b} →
  ∀ n →
  (∀ {A B} → A ↔ B → R A → R B) →
  ({A : Type a} {B : A → Type b} →
   P A → (∀ x → Q (B x)) → R (Σ A B)) →
  For-iterated-equality n P A →
  (∀ x → For-iterated-equality n Q (B x)) →
  For-iterated-equality n R (Σ A B)
For-iterated-equality-Σ zero _ hyp = hyp

For-iterated-equality-Σ {R = R} {P = P} {Q = Q} {A = A} {B = B}
  (suc n) resp hyp = curry (

  ((x y : A) → For-iterated-equality n P (x ≡ y)) ×
  ((x : A) (y z : B x) → For-iterated-equality n Q (y ≡ z))            ↝⟨ (λ (hyp₁ , hyp₂) _ _ → hyp₁ _ _ , λ _ → hyp₂ _ _ _) ⟩

  (((x₁ , x₂) (y₁ , y₂) : Σ A B) →
   For-iterated-equality n P (x₁ ≡ y₁) ×
   (∀ p → For-iterated-equality n Q (subst B p x₂ ≡ y₂)))              ↝⟨ (∀-cong _ λ _ → ∀-cong _ λ _ → uncurry $
                                                                           For-iterated-equality-Σ n resp hyp) ⟩
  (((x₁ , x₂) (y₁ , y₂) : Σ A B) →
   For-iterated-equality n R (∃ λ (p : x₁ ≡ y₁) → subst B p x₂ ≡ y₂))  ↝⟨ (∀-cong _ λ _ → ∀-cong _ λ _ →
                                                                           For-iterated-equality-cong _ n resp Bijection.Σ-≡,≡↔≡) ⟩□
  ((x y : Σ A B) → For-iterated-equality n R (x ≡ y))                  □)

-- A closure property for _×_.

For-iterated-equality-× :
  {A : Type a} {B : Type b} →
  ∀ n →
  (∀ {A B} → A ↔ B → R A → R B) →
  ({A : Type a} {B : Type b} → P A → Q B → R (A × B)) →
  For-iterated-equality n P A →
  For-iterated-equality n Q B →
  For-iterated-equality n R (A × B)
For-iterated-equality-× zero _ hyp = hyp

For-iterated-equality-× {R = R} {P = P} {Q = Q} {A = A} {B = B}
  (suc n) resp hyp = curry (

  ((x y : A) → For-iterated-equality n P (x ≡ y)) ×
  ((x y : B) → For-iterated-equality n Q (x ≡ y))      ↝⟨ (λ (hyp₁ , hyp₂) _ _ → hyp₁ _ _ , hyp₂ _ _) ⟩

  (((x₁ , x₂) (y₁ , y₂) : A × B) →
   For-iterated-equality n P (x₁ ≡ y₁) ×
   For-iterated-equality n Q (x₂ ≡ y₂))                ↝⟨ (∀-cong _ λ _ → ∀-cong _ λ _ → uncurry $
                                                           For-iterated-equality-× n resp hyp) ⟩
  (((x₁ , x₂) (y₁ , y₂) : A × B) →
   For-iterated-equality n R (x₁ ≡ y₁ × x₂ ≡ y₂))      ↝⟨ (∀-cong _ λ _ → ∀-cong _ λ _ →
                                                           For-iterated-equality-cong _ n resp ≡×≡↔≡) ⟩□
  ((x y : A × B) → For-iterated-equality n R (x ≡ y))  □)

-- A closure property for ↑.

For-iterated-equality-↑ :
  {A : Type a} {Q : Type (a ⊔ ℓ) → Type (a ⊔ ℓ)} →
  Extensionality? k (a ⊔ ℓ) (a ⊔ ℓ) →
  ∀ n →
  (∀ {A B} → A ↔ B → P A ↝[ k ] Q B) →
  For-iterated-equality n P A ↝[ k ]
  For-iterated-equality n Q (↑ ℓ A)
For-iterated-equality-↑ ext n resp =
  For-iterated-equality-cong ext n resp (inverse Bijection.↑↔)

-- Closure properties for W.

For-iterated-equality-W-suc :
  {A : Type a} {B : A → Type b} →
  Extensionality b (a ⊔ b) →
  ∀ n →
  (∀ {A B} → A ↔ B → Q A → Q B) →
  ({A : Type b} {B : A → Type (a ⊔ b)} →
   (∀ x → Q (B x)) → Q (∀ x → B x)) →
  ({A : Type a} {B : A → Type (a ⊔ b)} →
   P A → (∀ x → Q (B x)) → Q (Σ A B)) →
  For-iterated-equality (suc n) P A →
  For-iterated-equality (suc n) Q (W A B)
For-iterated-equality-W-suc {Q = Q} {P = P} {B = B}
  ext n resp hyp-Π hyp-Σ fie = lemma
  where
  lemma : ∀ x y → For-iterated-equality n Q (x ≡ y)
  lemma (sup x f) (sup y g) =                                        $⟨ (λ p i → lemma (f i) _) ⟩

    (∀ p i → For-iterated-equality n Q (f i ≡ g (subst B p i)))      ↝⟨ (∀-cong _ λ _ → For-iterated-equality-Π ext n resp hyp-Π) ⟩

    (∀ p → For-iterated-equality n Q (∀ i → f i ≡ g (subst B p i)))  ↝⟨ fie _ _ ,_ ⟩

    For-iterated-equality n P (x ≡ y) ×
    (∀ p → For-iterated-equality n Q (∀ i → f i ≡ g (subst B p i)))  ↝⟨ uncurry $ For-iterated-equality-Σ n resp hyp-Σ ⟩

    For-iterated-equality n Q
      (∃ λ (p : x ≡ y) → ∀ i → f i ≡ g (subst B p i))                ↝⟨ For-iterated-equality-cong _ n resp $ _≃_.bijection $ Eq.W-≡,≡≃≡ ext ⟩□

    For-iterated-equality n Q (sup x f ≡ sup y g)                    □

For-iterated-equality-W :
  {A : Type a} {B : A → Type b} →
  Extensionality b (a ⊔ b) →
  ∀ n →
  (∀ {A B} → A ↔ B → Q A → Q B) →
  ({A : Type b} {B : A → Type (a ⊔ b)} →
   (∀ x → Q (B x)) → Q (∀ x → B x)) →
  ({A : Type a} {B : A → Type (a ⊔ b)} →
   P A → (∀ x → Q (B x)) → Q (Σ A B)) →
  (P A → Q (W A B)) →
  For-iterated-equality n P A →
  For-iterated-equality n Q (W A B)
For-iterated-equality-W _   zero    _    _     _     hyp-W = hyp-W
For-iterated-equality-W ext (suc n) resp hyp-Π hyp-Σ _     =
  For-iterated-equality-W-suc ext n resp hyp-Π hyp-Σ

-- Closure properties for _⊎_.

For-iterated-equality-⊎-suc :
  {A : Type a} {B : Type b} →
  ∀ n →
  (∀ {A B} → A ↔ B → P A → P B) →
  P ⊥ →
  For-iterated-equality (suc n) P (↑ b A) →
  For-iterated-equality (suc n) P (↑ a B) →
  For-iterated-equality (suc n) P (A ⊎ B)
For-iterated-equality-⊎-suc {P = P} n resp hyp-⊥ fie-A fie-B = λ where
  (inj₁ x) (inj₁ y) →                            $⟨ fie-A (lift x) (lift y) ⟩
    For-iterated-equality n P (lift x ≡ lift y)  ↝⟨ For-iterated-equality-cong _ n resp (Bijection.≡↔inj₁≡inj₁ F.∘ lift≡lift↔) ⟩□
    For-iterated-equality n P (inj₁ x ≡ inj₁ y)  □

  (inj₂ x) (inj₂ y) →                            $⟨ fie-B (lift x) (lift y) ⟩
    For-iterated-equality n P (lift x ≡ lift y)  ↝⟨ For-iterated-equality-cong _ n resp (Bijection.≡↔inj₂≡inj₂ F.∘ lift≡lift↔) ⟩□
    For-iterated-equality n P (inj₂ x ≡ inj₂ y)  □

  (inj₁ x) (inj₂ y) →                            $⟨ hyp-⊥ ⟩
    P ⊥                                          ↝⟨ (λ hyp → For-iterated-equality-⊥ _ n (λ _ → hyp) _) ⟩
    For-iterated-equality n P ⊥                  ↝⟨ For-iterated-equality-cong _ n resp (inverse Bijection.≡↔⊎) ⟩□
    For-iterated-equality n P (inj₁ x ≡ inj₂ y)  □

  (inj₂ x) (inj₁ y) →                            $⟨ hyp-⊥ ⟩
    P ⊥                                          ↝⟨ (λ hyp → For-iterated-equality-⊥ _ n (λ _ → hyp) _) ⟩
    For-iterated-equality n P ⊥                  ↝⟨ For-iterated-equality-cong _ n resp (inverse Bijection.≡↔⊎) ⟩□
    For-iterated-equality n P (inj₂ x ≡ inj₁ y)  □

For-iterated-equality-⊎ :
  {A : Type a} {B : Type b} →
  ∀ n →
  (∀ {A B} → A ↔ B → P A → P B) →
  P ⊥ →
  (P (↑ b A) → P (↑ a B) → P (A ⊎ B)) →
  For-iterated-equality n P (↑ b A) →
  For-iterated-equality n P (↑ a B) →
  For-iterated-equality n P (A ⊎ B)
For-iterated-equality-⊎ zero    _    _     hyp-⊎ = hyp-⊎
For-iterated-equality-⊎ (suc n) resp hyp-⊥ _     =
  For-iterated-equality-⊎-suc n resp hyp-⊥

-- Closure properties for List.

For-iterated-equality-List-suc :
  {A : Type a} →
  ∀ n →
  (∀ {A B} → A ↔ B → P A → P B) →
  P (↑ a ⊤) →
  P ⊥ →
  (∀ {A B} → P A → P B → P (A × B)) →
  For-iterated-equality (suc n) P A →
  For-iterated-equality (suc n) P (List A)
For-iterated-equality-List-suc {P = P} n resp hyp-⊤ hyp-⊥ hyp-× fie = λ where
  [] [] →                                $⟨ hyp-⊤ ⟩
    P (↑ _ ⊤)                            ↝⟨ For-iterated-equality-↑-⊤ _ n resp ⟩
    For-iterated-equality n P (↑ _ ⊤)    ↝⟨ For-iterated-equality-cong _ n resp (inverse []≡[]↔⊤ F.∘ Bijection.↑↔) ⟩□
    For-iterated-equality n P ([] ≡ [])  □

  (x ∷ xs) (y ∷ ys) →                            $⟨ For-iterated-equality-List-suc n resp hyp-⊤ hyp-⊥ hyp-× fie xs ys ⟩
    For-iterated-equality n P (xs ≡ ys)          ↝⟨ fie _ _ ,_ ⟩

    For-iterated-equality n P (x ≡ y) ×
    For-iterated-equality n P (xs ≡ ys)          ↝⟨ uncurry $ For-iterated-equality-× n resp hyp-× ⟩

    For-iterated-equality n P (x ≡ y × xs ≡ ys)  ↝⟨ For-iterated-equality-cong _ n resp (inverse ∷≡∷↔≡×≡) ⟩□

    For-iterated-equality n P (x ∷ xs ≡ y ∷ ys)  □

  [] (y ∷ ys) →                              $⟨ hyp-⊥ ⟩
    P ⊥                                      ↝⟨ (λ hyp → For-iterated-equality-⊥ _ n (λ _ → hyp) _) ⟩
    For-iterated-equality n P ⊥              ↝⟨ For-iterated-equality-cong _ n resp (inverse []≡∷↔⊥) ⟩□
    For-iterated-equality n P ([] ≡ y ∷ ys)  □

  (x ∷ xs) [] →                              $⟨ hyp-⊥ ⟩
    P ⊥                                      ↝⟨ (λ hyp → For-iterated-equality-⊥ _ n (λ _ → hyp) _) ⟩
    For-iterated-equality n P ⊥              ↝⟨ For-iterated-equality-cong _ n resp (inverse ∷≡[]↔⊥) ⟩□
    For-iterated-equality n P (x ∷ xs ≡ [])  □

For-iterated-equality-List :
  {A : Type a} →
  ∀ n →
  (∀ {A B} → A ↔ B → P A → P B) →
  P (↑ a ⊤) →
  P ⊥ →
  (∀ {A B} → P A → P B → P (A × B)) →
  (P A → P (List A)) →
  For-iterated-equality n P A →
  For-iterated-equality n P (List A)
For-iterated-equality-List zero _ _ _ _ hyp-List = hyp-List

For-iterated-equality-List (suc n) resp hyp-⊤ hyp-⊥ hyp-× _ =
  For-iterated-equality-List-suc n resp hyp-⊤ hyp-⊥ hyp-×

------------------------------------------------------------------------
-- Some "closure properties" for the predicate

-- For-iterated-equality commutes with certain type constructors
-- (assuming extensionality).

For-iterated-equality-commutes :
  Extensionality? k ℓ ℓ →
  (F : Type ℓ → Type ℓ) →
  ∀ n →
  ({A : Type ℓ} {P : A → Type ℓ} →
   F (∀ x → P x) ↝[ k ] ∀ x → F (P x)) →
  F (For-iterated-equality n P A) ↝[ k ]
  For-iterated-equality n (F ∘ P) A
For-iterated-equality-commutes _ _ zero _ = F.id

For-iterated-equality-commutes {P = P} {A = A} ext F (suc n) hyp =
  F ((x y : A) → For-iterated-equality n P (x ≡ y))            ↝⟨ hyp ⟩
  ((x : A) → F ((y : A) → For-iterated-equality n P (x ≡ y)))  ↝⟨ (∀-cong ext λ _ → hyp) ⟩
  ((x y : A) → F (For-iterated-equality n P (x ≡ y)))          ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → For-iterated-equality-commutes ext F n hyp) ⟩□
  ((x y : A) → For-iterated-equality n (F ∘ P) (x ≡ y))        □

-- A variant of For-iterated-equality-commutes.

For-iterated-equality-commutesᴱ-→ :
  {@0 A : Type ℓ} {@0 P : Type ℓ → Type ℓ}
  (@0 F : Type ℓ → Type ℓ) →
  ∀ n →
  ({@0 A : Type ℓ} {@0 P : A → Type ℓ} →
   F (∀ x → P x) → ∀ x → F (P x)) →
  F (For-iterated-equality n P A) →
  For-iterated-equality n (F ∘ P) A
For-iterated-equality-commutesᴱ-→ _ zero _ = id

For-iterated-equality-commutesᴱ-→ {A = A} {P = P} F (suc n) hyp =
  F ((x y : A) → For-iterated-equality n P (x ≡ y))            →⟨ hyp ⟩
  ((x : A) → F ((y : A) → For-iterated-equality n P (x ≡ y)))  →⟨ hyp ∘_ ⟩
  ((x y : A) → F (For-iterated-equality n P (x ≡ y)))          →⟨ For-iterated-equality-commutesᴱ-→ F n hyp ∘_ ∘_ ⟩□
  ((x y : A) → For-iterated-equality n (F ∘ P) (x ≡ y))        □

-- Another variant of For-iterated-equality-commutes.

For-iterated-equality-commutes-← :
  Extensionality? k ℓ ℓ →
  (F : Type ℓ → Type ℓ) →
  ∀ n →
  ({A : Type ℓ} {P : A → Type ℓ} →
   (∀ x → F (P x)) ↝[ k ] F (∀ x → P x)) →
  For-iterated-equality n (F ∘ P) A ↝[ k ]
  F (For-iterated-equality n P A)
For-iterated-equality-commutes-← _ _ zero _ = F.id

For-iterated-equality-commutes-← {P = P} {A = A} ext F (suc n) hyp =
  ((x y : A) → For-iterated-equality n (F ∘ P) (x ≡ y))        ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → For-iterated-equality-commutes-← ext F n hyp) ⟩
  ((x y : A) → F (For-iterated-equality n P (x ≡ y)))          ↝⟨ (∀-cong ext λ _ → hyp) ⟩
  ((x : A) → F ((y : A) → For-iterated-equality n P (x ≡ y)))  ↝⟨ hyp ⟩□
  F ((x y : A) → For-iterated-equality n P (x ≡ y))            □

-- A variant of For-iterated-equality-commutes-←.

For-iterated-equality-commutesᴱ-← :
  {@0 A : Type ℓ} {@0 P : Type ℓ → Type ℓ}
  (@0 F : Type ℓ → Type ℓ) →
  ∀ n →
  ({@0 A : Type ℓ} {@0 P : A → Type ℓ} →
   (∀ x → F (P x)) → F (∀ x → P x)) →
  For-iterated-equality n (F ∘ P) A →
  F (For-iterated-equality n P A)
For-iterated-equality-commutesᴱ-← _ zero _ = id

For-iterated-equality-commutesᴱ-← {A = A} {P = P} F (suc n) hyp =
  ((x y : A) → For-iterated-equality n (F ∘ P) (x ≡ y))        →⟨ For-iterated-equality-commutesᴱ-← F n hyp ∘_ ∘_ ⟩
  ((x y : A) → F (For-iterated-equality n P (x ≡ y)))          →⟨ hyp ∘_ ⟩
  ((x : A) → F ((y : A) → For-iterated-equality n P (x ≡ y)))  →⟨ hyp ⟩□
  F ((x y : A) → For-iterated-equality n P (x ≡ y))            □

-- For-iterated-equality commutes with certain binary type
-- constructors (assuming extensionality).

For-iterated-equality-commutes₂ :
  Extensionality? k ℓ ℓ →
  (F : Type ℓ → Type ℓ → Type ℓ) →
  ∀ n →
  ({A : Type ℓ} {P Q : A → Type ℓ} →
   F (∀ x → P x) (∀ x → Q x) ↝[ k ] ∀ x → F (P x) (Q x)) →
  F (For-iterated-equality n P A) (For-iterated-equality n Q A) ↝[ k ]
  For-iterated-equality n (λ A → F (P A) (Q A)) A
For-iterated-equality-commutes₂ _ _ zero _ = F.id

For-iterated-equality-commutes₂ {P = P} {A = A} {Q = Q}
                                ext F (suc n) hyp =
  F ((x y : A) → For-iterated-equality n P (x ≡ y))
    ((x y : A) → For-iterated-equality n Q (x ≡ y))                    ↝⟨ hyp ⟩

  ((x : A) → F ((y : A) → For-iterated-equality n P (x ≡ y))
               ((y : A) → For-iterated-equality n Q (x ≡ y)))          ↝⟨ (∀-cong ext λ _ → hyp) ⟩

  ((x y : A) → F (For-iterated-equality n P (x ≡ y))
                 (For-iterated-equality n Q (x ≡ y)))                  ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                           For-iterated-equality-commutes₂ ext F n hyp) ⟩□
  ((x y : A) → For-iterated-equality n (λ A → F (P A) (Q A)) (x ≡ y))  □

-- A variant of For-iterated-equality-commutes₂.

For-iterated-equality-commutes₂ᴱ-→ :
  {@0 A : Type ℓ} {@0 P Q : Type ℓ → Type ℓ}
  (@0 F : Type ℓ → Type ℓ → Type ℓ) →
  ∀ n →
  ({@0 A : Type ℓ} {@0 P Q : A → Type ℓ} →
   F (∀ x → P x) (∀ x → Q x) → ∀ x → F (P x) (Q x)) →
  F (For-iterated-equality n P A) (For-iterated-equality n Q A) →
  For-iterated-equality n (λ A → F (P A) (Q A)) A
For-iterated-equality-commutes₂ᴱ-→ _ zero _ = id

For-iterated-equality-commutes₂ᴱ-→ {A = A} {P = P} {Q = Q}
                                   F (suc n) hyp =
  F ((x y : A) → For-iterated-equality n P (x ≡ y))
    ((x y : A) → For-iterated-equality n Q (x ≡ y))                    →⟨ hyp ⟩

  ((x : A) → F ((y : A) → For-iterated-equality n P (x ≡ y))
               ((y : A) → For-iterated-equality n Q (x ≡ y)))          →⟨ hyp ∘_ ⟩

  ((x y : A) → F (For-iterated-equality n P (x ≡ y))
                 (For-iterated-equality n Q (x ≡ y)))                  →⟨ For-iterated-equality-commutes₂ᴱ-→ F n hyp ∘_ ∘_ ⟩□
  ((x y : A) → For-iterated-equality n (λ A → F (P A) (Q A)) (x ≡ y))  □

-- Another variant of For-iterated-equality-commutes₂.

For-iterated-equality-commutes₂-← :
  Extensionality? k ℓ ℓ →
  (F : Type ℓ → Type ℓ → Type ℓ) →
  ∀ n →
  ({A : Type ℓ} {P Q : A → Type ℓ} →
   (∀ x → F (P x) (Q x)) ↝[ k ] F (∀ x → P x) (∀ x → Q x)) →
  For-iterated-equality n (λ A → F (P A) (Q A)) A ↝[ k ]
  F (For-iterated-equality n P A) (For-iterated-equality n Q A)
For-iterated-equality-commutes₂-← _ _ zero _ = F.id

For-iterated-equality-commutes₂-← {P = P} {Q = Q} {A = A}
                                  ext F (suc n) hyp =
  ((x y : A) → For-iterated-equality n (λ A → F (P A) (Q A)) (x ≡ y))  ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                           For-iterated-equality-commutes₂-← ext F n hyp) ⟩
  ((x y : A) → F (For-iterated-equality n P (x ≡ y))
                 (For-iterated-equality n Q (x ≡ y)))                  ↝⟨ (∀-cong ext λ _ → hyp) ⟩

  ((x : A) → F ((y : A) → For-iterated-equality n P (x ≡ y))
               ((y : A) → For-iterated-equality n Q (x ≡ y)))          ↝⟨ hyp ⟩□

  F ((x y : A) → For-iterated-equality n P (x ≡ y))
    ((x y : A) → For-iterated-equality n Q (x ≡ y))                    □

-- A variant of For-iterated-equality-commutes₂-←.

For-iterated-equality-commutes₂ᴱ-← :
  {@0 A : Type ℓ} {@0 P Q : Type ℓ → Type ℓ}
  (@0 F : Type ℓ → Type ℓ → Type ℓ) →
  ∀ n →
  ({@0 A : Type ℓ} {@0 P Q : A → Type ℓ} →
   (∀ x → F (P x) (Q x)) → F (∀ x → P x) (∀ x → Q x)) →
  For-iterated-equality n (λ A → F (P A) (Q A)) A →
  F (For-iterated-equality n P A) (For-iterated-equality n Q A)
For-iterated-equality-commutes₂ᴱ-← _ zero _ = id

For-iterated-equality-commutes₂ᴱ-← {A = A} {P = P} {Q = Q}
                                   F (suc n) hyp =
  ((x y : A) → For-iterated-equality n (λ A → F (P A) (Q A)) (x ≡ y))  →⟨ For-iterated-equality-commutes₂ᴱ-← F n hyp ∘_ ∘_ ⟩
  ((x y : A) → F (For-iterated-equality n P (x ≡ y))
                 (For-iterated-equality n Q (x ≡ y)))                  →⟨ hyp ∘_ ⟩

  ((x : A) → F ((y : A) → For-iterated-equality n P (x ≡ y))
               ((y : A) → For-iterated-equality n Q (x ≡ y)))          →⟨ hyp ⟩□

  F ((x y : A) → For-iterated-equality n P (x ≡ y))
    ((x y : A) → For-iterated-equality n Q (x ≡ y))                    □

-- A corollary of For-iterated-equality-commutes₂.

For-iterated-equality-commutes-× :
  {A : Type a} →
  ∀ n →
  For-iterated-equality n P A × For-iterated-equality n Q A ↝[ a ∣ a ]
  For-iterated-equality n (λ A → P A × Q A) A
For-iterated-equality-commutes-× n ext =
  For-iterated-equality-commutes₂ ext _×_ n
    (from-isomorphism $ inverse ΠΣ-comm)

-- Some corollaries of For-iterated-equality-commutes₂ᴱ-→.

For-iterated-equality-commutesᴱ-×-→ :
  {@0 A : Type ℓ} {@0 P Q : Type ℓ → Type ℓ} →
  ∀ n →
  For-iterated-equality n P A × For-iterated-equality n Q A →
  For-iterated-equality n (λ A → P A × Q A) A
For-iterated-equality-commutesᴱ-×-→ n =
  For-iterated-equality-commutes₂ᴱ-→ _×_ n
    (λ (f , g) x → f x , g x)

For-iterated-equality-commutes-⊎ :
  {@0 A : Type ℓ} {@0 P Q : Type ℓ → Type ℓ} →
  ∀ n →
  For-iterated-equality n P A ⊎ For-iterated-equality n Q A →
  For-iterated-equality n (λ A → P A ⊎ Q A) A
For-iterated-equality-commutes-⊎ n =
  For-iterated-equality-commutes₂ᴱ-→ _⊎_ n
    [ (λ f x → inj₁ (f x)) , (λ f x → inj₂ (f x)) ]

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality