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

module 22-descent where

import 21-cubical-diagrams
open 21-cubical-diagrams public

-- Section 18.1 Five equivalent characterizations of pushouts

dep-cocone :
  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  ( f : S → A) (g : S → B) (c : cocone f g X) (P : X → UU l5) →
  UU (l1 ⊔ l2 ⊔ l3 ⊔ l5)
dep-cocone {S = S} {A} {B} f g c P =
  Σ ((a : A) → P ((pr1 c) a)) (λ hA →
    Σ ((b : B) → P (pr1 (pr2 c) b)) (λ hB →
      (s : S) → Id (tr P (pr2 (pr2 c) s) (hA (f s))) (hB (g s))))

dep-cocone-map :
  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  ( f : S → A) (g : S → B) (c : cocone f g X) (P : X → UU l5) →
  ( (x : X) → P x) → dep-cocone f g c P
dep-cocone-map f g c P h =
  pair (λ a → h (pr1 c a)) (pair (λ b → h (pr1 (pr2 c) b)) (λ s → apd h (pr2 (pr2 c) s)))

{- Definition 18.1.1 The induction principle of pushouts -}

Ind-pushout :
  { l1 l2 l3 l4 : Level} (l : Level) →
  { S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} →
  ( f : S → A) (g : S → B) (c : cocone f g X) → UU (lsuc l ⊔ l1 ⊔ l2 ⊔ l3 ⊔ l4)
Ind-pushout l {X = X} f g c =
  (P : X → UU l) → sec (dep-cocone-map f g c P)

{- Definition 18.1.2 The dependent universal property of pushouts -}

dependent-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) → UU _
dependent-universal-property-pushout l f g {X} c =
  (P : X → UU l) → is-equiv (dep-cocone-map f g c P)

{- Remark 18.1.3. We compute the identity type of dep-cocone in order to
   express the computation rules of the induction principle for pushouts. -}

coherence-htpy-dep-cocone :
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X)
  (P : X → UU l5) (c' c'' : dep-cocone f g c P)
  (K : (pr1 c') ~ (pr1 c'')) (L : (pr1 (pr2 c')) ~ (pr1 (pr2 c''))) →
  UU (l1 ⊔ l5)
coherence-htpy-dep-cocone {S = S} f g c P
  h h' K L =
  (s : S) →
  Id ( ((pr2 (pr2 h)) s) ∙ (L (g s)))
     ( (ap (tr P (pr2 (pr2 c) s)) (K (f s))) ∙ ((pr2 (pr2 h')) s))

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

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

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

abstract
  is-contr-total-htpy-dep-cocone :
    {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
    (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (P : X → UU l5) →
    (s : dep-cocone f g c P) →
    is-contr
      ( Σ (dep-cocone f g c P)
        ( htpy-dep-cocone f g c P s))
  is-contr-total-htpy-dep-cocone
    {S = S} {A} {B} f g {X} (pair i (pair j H)) P (pair hA (pair hB hS)) =
    is-contr-total-Eq-structure
      ( λ α βγ K →
          Σ (hB ~ (pr1 βγ)) (λ L →
          coherence-htpy-dep-cocone f g
            ( pair i (pair j H)) P (pair hA (pair hB hS)) (pair α βγ) K L))
      ( is-contr-total-htpy hA)
      ( pair hA htpy-refl)
      ( is-contr-total-Eq-structure
        ( λ β γ L →
          coherence-htpy-dep-cocone f g
            ( pair i (pair j H))
            ( P)
            ( pair hA (pair hB hS))
            ( pair hA (pair β γ))
            ( htpy-refl)
            ( L))
        ( is-contr-total-htpy hB)
        ( pair hB htpy-refl)
        ( is-contr-is-equiv
          ( Σ ((s : S) → Id (tr P (H s) (hA (f s))) (hB (g s))) (λ γ → hS ~ γ))
          ( tot (htpy-concat (htpy-inv htpy-right-unit)))
          ( is-equiv-tot-is-fiberwise-equiv
            ( is-equiv-htpy-concat (htpy-inv htpy-right-unit)))
          ( is-contr-total-htpy hS)))

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

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

  issec-eq-htpy-dep-cocone :
    {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
      (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (P : X → UU l5) →
    (s t : dep-cocone f g c P) →
    ( ( htpy-dep-cocone-eq f g c P {s} {t}) ∘
      ( eq-htpy-dep-cocone f g c P s t)) ~ id
  issec-eq-htpy-dep-cocone f g c P s t =
    issec-inv-is-equiv
    ( is-equiv-htpy-dep-cocone-eq f g c P s t)

  isretr-eq-htpy-dep-cocone :
    {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
    (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (P : X → UU l5) →
    (s t : dep-cocone f g c P) →
    ( ( eq-htpy-dep-cocone f g c P s t) ∘
      ( htpy-dep-cocone-eq f g c P {s} {t})) ~ id
  isretr-eq-htpy-dep-cocone f g c P s t =
    isretr-inv-is-equiv
      ( is-equiv-htpy-dep-cocone-eq f g c P s t)

ind-pushout :
  { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} →
  ( f : S → A) (g : S → B) (c : cocone f g X) →
  Ind-pushout l f g c → (P : X → UU l) →
  dep-cocone f g c P → (x : X) → P x
ind-pushout f g c ind-c P =
  pr1 (ind-c P)

comp-pushout :
  { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} →
  ( f : S → A) (g : S → B) (c : cocone f g X) →
  ( ind-c : Ind-pushout l f g c) (P : X → UU l) (h : dep-cocone f g c P) →
  htpy-dep-cocone f g c P
    ( dep-cocone-map f g c P (ind-pushout f g c ind-c P h))
    ( h)
comp-pushout f g c ind-c P h =
  htpy-dep-cocone-eq f g c P (pr2 (ind-c P) h)

left-comp-pushout :
  { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} →
  ( f : S → A) (g : S → B) (c : cocone f g X) →
  ( ind-c : Ind-pushout l f g c) (P : X → UU l) (h : dep-cocone f g c P) →
  ( a : A) → Id (ind-pushout f g c ind-c P h (pr1 c a)) (pr1 h a)
left-comp-pushout f g c ind-c P h =
  pr1 (comp-pushout f g c ind-c P h)

right-comp-pushout :
  { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} →
  ( f : S → A) (g : S → B) (c : cocone f g X) →
  ( ind-c : Ind-pushout l f g c) (P : X → UU l) (h : dep-cocone f g c P) →
  ( b : B) → Id (ind-pushout f g c ind-c P h (pr1 (pr2 c) b)) (pr1 (pr2 h) b)
right-comp-pushout f g c ind-c P h =
  pr1 (pr2 (comp-pushout f g c ind-c P h))

path-comp-pushout :
  { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} →
  ( f : S → A) (g : S → B) (c : cocone f g X) →
  ( ind-c : Ind-pushout l f g c) (P : X → UU l) (h : dep-cocone f g c P) →
  coherence-htpy-dep-cocone f g c P
    ( dep-cocone-map f g c P (ind-pushout f g c ind-c P h))
    ( h)
    ( left-comp-pushout f g c ind-c P h)
    ( right-comp-pushout f g c ind-c P h)
path-comp-pushout f g c ind-c P h =
  pr2 (pr2 (comp-pushout f g c ind-c P h))

abstract
  uniqueness-dependent-universal-property-pushout :
    { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} →
    ( f : S → A) (g : S → B) (c : cocone f g X)
    ( dup-c : dependent-universal-property-pushout l f g c) →
    ( P : X → UU l) ( h : dep-cocone f g c P) →
    is-contr
      ( Σ ((x : X) → P x) (λ k →
          htpy-dep-cocone f g c P (dep-cocone-map f g c P k) h))
  uniqueness-dependent-universal-property-pushout f g c dup-c P h =
    is-contr-is-equiv'
      ( fib (dep-cocone-map f g c P) h)
      ( tot (λ k → htpy-dep-cocone-eq f g c P))
      ( is-equiv-tot-is-fiberwise-equiv
        ( λ k → is-equiv-htpy-dep-cocone-eq f g c P
          ( dep-cocone-map f g c P k) h))
      ( is-contr-map-is-equiv (dup-c P) h)

{- This finishes the formalization of remark 18.1.3. -}

{- Before we state the main theorem of this section, we also state a dependent
   version of the pullback property of pushouts. -}

cone-dependent-pullback-property-pushout :
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (P : X → UU l5) →
  let i = pr1 c
      j = pr1 (pr2 c)
      H = pr2 (pr2 c)
  in
  cone
    ( λ (h : (a : A) → P (i a)) → λ (s : S) → tr P (H s) (h (f s)))
    ( λ (h : (b : B) → P (j b)) → λ s → h (g s))
    ( (x : X) → P x)
cone-dependent-pullback-property-pushout f g (pair i (pair j H)) P =
  pair
    ( λ h → λ a → h (i a))
    ( pair
      ( λ h → λ b → h (j b))
      ( λ h → eq-htpy (λ s → apd h (H s))))

dependent-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))))
dependent-pullback-property-pushout l {S} {A} {B} f g {X}
  (pair i (pair j H)) =
  (P : X → UU l) →
  is-pullback
    ( λ (h : (a : A) → P (i a)) → λ s → tr P (H s) (h (f s)))
    ( λ (h : (b : B) → P (j b)) → λ s → h (g s))
    ( cone-dependent-pullback-property-pushout f g (pair i (pair j H)) P)

{- Theorem 18.1.4 The following properties are all equivalent:

   1. universal-property-pushout
   2. pullback-property-pushout
   3. dependent-pullback-property-pushout
   4. dependent-universal-property-pushout
   5. Ind-pushout

   We have already shown that 1 ↔ 2. Therefore we will first show that
   3 ↔ 4 ↔ 5. Finally, we will show that 2 ↔ 3. Here are the precise references
   to the proofs of those parts:

   Proof of 1 → 2.
   pullback-property-pushout-universal-property-pushout

   Proof of 2 → 1
   universal-property-pushout-pullback-property-pushout

   Proof of 2 → 3
   dependent-pullback-property-pullback-property-pushout

   Proof of 3 → 2
   pullback-property-dependent-pullback-property-pushout

   Proof of 3 → 4
   dependent-universal-property-dependent-pullback-property-pushout

   Proof of 4 → 3
   dependent-pullback-property-dependent-universal-property-pushout

   Proof of 4 → 5
   Ind-pushout-dependent-universal-property-pushout

   Proof of 5 → 4
   dependent-universal-property-pushout-Ind-pushout
   -}

{- Proof of Theorem 18.1.4, (v) implies (iv). -}

dependent-naturality-square :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f f' : (x : A) → B x)
  {x x' : A} (p : Id x x') {q : Id (f x) (f' x)} {q' : Id (f x') (f' x')} →
  Id ((apd f p) ∙ q') ((ap (tr B p) q) ∙ (apd f' p)) →
  Id (tr (λ y → Id (f y) (f' y)) p q) q'
dependent-naturality-square f f' refl {q} {q'} s =
  inv (s ∙ (right-unit ∙ (ap-id q)))

htpy-eq-dep-cocone-map :
  { 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) →
  ( H : Ind-pushout l f g c) { P : X → UU l} (h h' : (x : X) → P x) →
  Id (dep-cocone-map f g c P h) (dep-cocone-map f g c P h') → h ~ h'
htpy-eq-dep-cocone-map f g c ind-c {P} h h' p =
  ind-pushout f g c ind-c
    ( λ x → Id (h x) (h' x))
    ( pair
      ( pr1 (htpy-dep-cocone-eq f g c P p))
      ( pair
        ( pr1 (pr2 (htpy-dep-cocone-eq f g c P p)))
        ( λ s →
          dependent-naturality-square h h' (pr2 (pr2 c) s)
            ( pr2 (pr2 (htpy-dep-cocone-eq f g c P p)) s))))

dependent-universal-property-pushout-Ind-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) → Ind-pushout l f g c) →
  ((l : Level) → dependent-universal-property-pushout l f g c)
dependent-universal-property-pushout-Ind-pushout f g c ind-c l P =
  is-equiv-has-inverse
    ( ind-pushout f g c (ind-c l) P)
    ( pr2 (ind-c l P))
    ( λ h → eq-htpy (htpy-eq-dep-cocone-map f g c (ind-c l)
      ( ind-pushout f g c (ind-c l) P (dep-cocone-map f g c P h))
      ( h)
      ( pr2 (ind-c l P) (dep-cocone-map f g c P h))))

{- Proof of Theorem 18.1.4, (iv) implies (v). -}

Ind-pushout-dependent-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) → dependent-universal-property-pushout l f g c) →
  ((l : Level) → Ind-pushout l f g c)
Ind-pushout-dependent-universal-property-pushout f g c dup-c l P =
  pr1 (dup-c l P)

{- Proof of Theorem 18.1.4, (iv) implies (iii). -}

triangle-dependent-pullback-property-pushout :
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (P : X → UU l5) →
  let i = pr1 c
      j = pr1 (pr2 c)
      H = pr2 (pr2 c)
  in
  ( dep-cocone-map f g c P) ~
  ( ( tot (λ h → tot (λ h' → htpy-eq))) ∘
    ( gap
      ( λ (h : (a : A) → P (i a)) → λ s → tr P (H s) (h (f s)))
      ( λ (h : (b : B) → P (j b)) → λ s → h (g s))
      ( cone-dependent-pullback-property-pushout f g c P)))
triangle-dependent-pullback-property-pushout f g (pair i (pair j H)) P h =
  eq-pair refl (eq-pair refl (inv (issec-eq-htpy (λ x → apd h (H x)))))

dependent-pullback-property-dependent-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) → dependent-universal-property-pushout l f g c) →
  ((l : Level) → dependent-pullback-property-pushout l f g c)
dependent-pullback-property-dependent-universal-property-pushout
  f g (pair i (pair j H)) I l P =
  let c = (pair i (pair j H)) in
  is-equiv-right-factor
    ( dep-cocone-map f g c P)
    ( tot (λ h → tot λ h' → htpy-eq))
    ( gap
      ( λ h x → tr P (H x) (h (f x)))
      ( λ h x → h (g x))
      ( cone-dependent-pullback-property-pushout f g c P))
    ( triangle-dependent-pullback-property-pushout f g c P)
    ( is-equiv-tot-is-fiberwise-equiv
      ( λ h → is-equiv-tot-is-fiberwise-equiv
        ( λ h' → funext (λ x → tr P (H x) (h (f x))) (λ x → h' (g x)))))
    ( I l P)

{- Proof of Theorem 18.1.4, (iv) implies (iii). -}

dependent-universal-property-dependent-pullback-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) → dependent-pullback-property-pushout l f g c) →
  ((l : Level) → dependent-universal-property-pushout l f g c)
dependent-universal-property-dependent-pullback-property-pushout
  f g (pair i (pair j H)) dpullback-c l P =
  let c = (pair i (pair j H)) in
  is-equiv-comp
    ( dep-cocone-map f g c P)
    ( tot (λ h → tot λ h' → htpy-eq))
    ( gap
      ( λ h x → tr P (H x) (h (f x)))
      ( λ h x → h (g x))
      ( cone-dependent-pullback-property-pushout f g c P))
    ( triangle-dependent-pullback-property-pushout f g c P)
    ( dpullback-c l P)
    ( is-equiv-tot-is-fiberwise-equiv
      ( λ h → is-equiv-tot-is-fiberwise-equiv
        ( λ h' → funext (λ x → tr P (H x) (h (f x))) (λ x → h' (g x)))))

{- Proof of Theorem 18.1.4, (iii) implies (ii). -}

concat-eq-htpy :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (x : A) → B x}
  (H : f ~ g) (K : g ~ h) → Id (eq-htpy (H ∙h K)) ((eq-htpy H) ∙ (eq-htpy K))
concat-eq-htpy {A = A} {B} {f} H K =
  ind-htpy f
    ( λ g H →
      ( h : (x : A) → B x) (K : g ~ h) →
      Id (eq-htpy (H ∙h K)) ((eq-htpy H) ∙ (eq-htpy K)))
    ( λ h K → ap (concat' f (eq-htpy K)) (inv (eq-htpy-htpy-refl _))) H _ K

pullback-property-dependent-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) →
  dependent-pullback-property-pushout l f g c →
  pullback-property-pushout l f g c
pullback-property-dependent-pullback-property-pushout
  l f g (pair i (pair j H)) dpb Y =
  is-pullback-htpy
    ( λ h s → tr (λ x → Y) (H s) (h (f s)))
    ( λ h → eq-htpy (λ s → inv (tr-triv (H s) (h (f s)))))
    ( λ h s → h (g s))
    ( htpy-refl)
    { c = pair
      ( λ h a → h (i a))
      ( pair (λ h b → h (j b)) (λ h → eq-htpy (h ·l H)))}
    ( cone-dependent-pullback-property-pushout
      f g (pair i (pair j H)) (λ x → Y))
    ( pair
      ( λ h → refl)
      ( pair
        ( λ h → refl)
        ( λ h → right-unit ∙
          ( ( ap eq-htpy
              ( eq-htpy (λ s →
                inv-con
                  ( tr-triv (H s) (h (i (f s))))
                  ( ap h (H s))
                  ( apd h (H s))
                  ( inv (apd-triv h (H s)))))) ∙
            ( concat-eq-htpy
              ( λ s → inv (tr-triv (H s) (h (i (f s)))))
              ( λ s → apd h (H s)))))))
    ( dpb (λ x → Y))

{- Proof of Theorem 18.1.4, (ii) implies (iii). -}

{- We first define the family of lifts, which is indexed by maps Y → X. -}

fam-lifts :
  {l1 l2 l3 : Level} (Y : UU l1) {X : UU l2} (P : X → UU l3) →
  (Y → X) → UU (l1 ⊔ l3)
fam-lifts Y P h = (y : Y) → P (h y)

tr-fam-lifts' :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4) →
  (h : B → X) {f g : A → B} (H : f ~ g) →
  fam-lifts A P (h ∘ f) → fam-lifts A P (h ∘ g)
tr-fam-lifts' P h {f} {g} H k s = tr (P ∘ h) (H s) (k s)

TR-EQ-HTPY-FAM-LIFTS :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4) →
  (h : B → X) {f g : A → B} (H : f ~ g) → UU (l1 ⊔ l4)
TR-EQ-HTPY-FAM-LIFTS {A = A} P h H =
  tr (fam-lifts A P) (eq-htpy (h ·l H)) ~ (tr-fam-lifts' P h H)

tr-eq-htpy-fam-lifts-htpy-refl :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4) →
  (h : B → X) (f : A → B) → TR-EQ-HTPY-FAM-LIFTS P h (htpy-refl' f)
tr-eq-htpy-fam-lifts-htpy-refl P h f k =
  ap (λ t → tr (fam-lifts _ P) t k) (eq-htpy-htpy-refl (h ∘ f))

abstract
  tr-eq-htpy-fam-lifts :
    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4) →
    (h : B → X) {f g : A → B} (H : f ~ g) →
    TR-EQ-HTPY-FAM-LIFTS P h H
  tr-eq-htpy-fam-lifts P h {f} =
    ind-htpy f
      ( λ g H → TR-EQ-HTPY-FAM-LIFTS P h H)
      ( tr-eq-htpy-fam-lifts-htpy-refl P h f)

  compute-tr-eq-htpy-fam-lifts :
    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4) →
    (h : B → X) (f : A → B) →
    Id  ( tr-eq-htpy-fam-lifts P h (htpy-refl' f))
        ( tr-eq-htpy-fam-lifts-htpy-refl P h f)
  compute-tr-eq-htpy-fam-lifts P h f =
    comp-htpy f
      ( λ g H → TR-EQ-HTPY-FAM-LIFTS P h H)
      ( tr-eq-htpy-fam-lifts-htpy-refl P h f)

{- One of the basic operations on lifts is precomposition by an ordinary
   function. -}

precompose-lifts :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (P : X → UU l4) → (f : A → B) → (h : B → X) →
  (fam-lifts B P h) → (fam-lifts A P (h ∘ f))
precompose-lifts P f h h' a = h' (f a)

{- Given two homotopic maps, their precomposition functions have different
   codomains. However, there is a commuting triangle. We obtain this triangle
   by homotopy induction. -}

TRIANGLE-PRECOMPOSE-LIFTS :
  { l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  ( P : X → UU l4) {f g : A → B} (H : f ~ g) → UU (l1 ⊔ (l2 ⊔ (l3 ⊔ l4)))
TRIANGLE-PRECOMPOSE-LIFTS {A = A} {B} {X} P {f} {g} H =
  (h : B → X) →
    ( (tr (fam-lifts A P) (eq-htpy (h ·l H))) ∘ (precompose-lifts P f h)) ~
    ( precompose-lifts P g h)

triangle-precompose-lifts-htpy-refl :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (P : X → UU l4) (f : A → B) → TRIANGLE-PRECOMPOSE-LIFTS P (htpy-refl' f)
triangle-precompose-lifts-htpy-refl {A = A} P f h h' =
  tr-eq-htpy-fam-lifts-htpy-refl P h f (λ a → h' (f a))

abstract
  triangle-precompose-lifts :
    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
    (P : X → UU l4) {f g : A → B} (H : f ~ g) →
    TRIANGLE-PRECOMPOSE-LIFTS P H
  triangle-precompose-lifts {A = A} P {f} =
    ind-htpy f
      ( λ g H → TRIANGLE-PRECOMPOSE-LIFTS P H)
      ( triangle-precompose-lifts-htpy-refl P f)

  compute-triangle-precompose-lifts :
    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
    (P : X → UU l4) (f : A → B) →
    Id
      ( triangle-precompose-lifts P (htpy-refl' f))
      ( triangle-precompose-lifts-htpy-refl P f)
  compute-triangle-precompose-lifts P f =
    comp-htpy f
      ( λ g H → TRIANGLE-PRECOMPOSE-LIFTS P H)
      ( triangle-precompose-lifts-htpy-refl P f)

{- There is a similar commuting triangle with the computed transport function.
   This time we don't use homotopy induction to construct the homotopy. We
   give an explicit definition instead. -}

triangle-precompose-lifts' :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (P : X → UU l4) {f g : A → B} (H : f ~ g) → (h : B → X) →
  ( (tr-fam-lifts' P h H) ∘ (precompose-lifts P f h)) ~
  ( precompose-lifts P g h)
triangle-precompose-lifts' P H h k = eq-htpy (λ a → apd k (H a))

compute-triangle-precompose-lifts' :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (P : X → UU l4) (f : A → B) → (h : B → X) →
  ( triangle-precompose-lifts' P (htpy-refl' f) h) ~
  ( htpy-refl' ( precompose-lifts P f h))
compute-triangle-precompose-lifts' P f h k = eq-htpy-htpy-refl _

{- There is a coherence between the two commuting triangles. This coherence
   is again constructed by homotopy induction. -}

COHERENCE-TRIANGLE-PRECOMPOSE-LIFTS :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
  {f g : A → B} (H : f ~ g) → UU (l1 ⊔ (l2 ⊔ (l3 ⊔ l4)))
COHERENCE-TRIANGLE-PRECOMPOSE-LIFTS {A = A} {B} {X} P {f} {g} H =
  (h : B → X) →
    ( triangle-precompose-lifts P H h) ~
    ( ( ( tr-eq-htpy-fam-lifts P h H) ·r (precompose-lifts P f h)) ∙h
      ( triangle-precompose-lifts' P H h))

coherence-triangle-precompose-lifts-htpy-refl :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
  (f : A → B) → COHERENCE-TRIANGLE-PRECOMPOSE-LIFTS P (htpy-refl' f)
coherence-triangle-precompose-lifts-htpy-refl P f h =
  ( htpy-eq (htpy-eq (compute-triangle-precompose-lifts P f) h)) ∙h
  ( ( ( htpy-inv htpy-right-unit) ∙h
      ( htpy-ap-concat
        ( λ h' → tr-eq-htpy-fam-lifts-htpy-refl P h f (λ a → h' (f a)))
        ( htpy-refl)
        ( triangle-precompose-lifts' P htpy-refl h)
        ( htpy-inv (compute-triangle-precompose-lifts' P f h)))) ∙h
    ( htpy-eq
      ( ap
        ( λ t →
          ( t ·r (precompose-lifts P f h)) ∙h
          ( triangle-precompose-lifts' P htpy-refl h))
        ( inv (compute-tr-eq-htpy-fam-lifts P h f)))))

abstract
  coherence-triangle-precompose-lifts :
    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
    {f g : A → B} (H : f ~ g) → COHERENCE-TRIANGLE-PRECOMPOSE-LIFTS P H
  coherence-triangle-precompose-lifts P {f} =
    ind-htpy f
      ( λ g H → COHERENCE-TRIANGLE-PRECOMPOSE-LIFTS P H)
      ( coherence-triangle-precompose-lifts-htpy-refl P f)

  compute-coherence-triangle-precompose-lifts :
    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
    (f : A → B) →
      Id  ( coherence-triangle-precompose-lifts P (htpy-refl' f))
        ( coherence-triangle-precompose-lifts-htpy-refl P f)
  compute-coherence-triangle-precompose-lifts P f =
    comp-htpy f
      ( λ g H → COHERENCE-TRIANGLE-PRECOMPOSE-LIFTS P H)
      ( coherence-triangle-precompose-lifts-htpy-refl P f)

total-lifts :
  {l1 l2 l3 : Level} (A : UU l1) {X : UU l2} (P : X → UU l3) →
  UU _
total-lifts A {X} P = type-choice-∞ {A = A} {B = λ a → X} (λ a → P)

precompose-total-lifts :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (P : X → UU l4) → (A → B) →
  total-lifts B P → total-lifts A P
precompose-total-lifts {A = A} P f =
  toto
    ( λ h → (a : A) → P (h a))
    ( λ h → h ∘ f)
    ( precompose-lifts P f)

coherence-square-inv-choice-∞ :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (P : X → UU l4) (f : A → B) →
  coherence-square
    ( precompose-total-lifts P f)
    ( inv-choice-∞ {A = B} {B = λ x → X} {C = λ x y → P y})
    ( inv-choice-∞)
    ( λ h → h ∘ f)
coherence-square-inv-choice-∞ P f = htpy-refl

{- Our goal is now to produce a homotopy between (precompose-total-lifts P f)
   and (precompose-total-lifts P g) for homotopic maps f and g, and a coherence
   filling a cilinder. -}

HTPY-PRECOMPOSE-TOTAL-LIFTS :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
  (P : X → UU l4) {f g : A → B} (H : f ~ g) →
  UU (l1 ⊔ (l2 ⊔ (l3 ⊔ l4)))
HTPY-PRECOMPOSE-TOTAL-LIFTS P {f} {g} H =
  (precompose-total-lifts P f) ~ (precompose-total-lifts P g)

htpy-precompose-total-lifts :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
  {f g : A → B} (H : f ~ g) → HTPY-PRECOMPOSE-TOTAL-LIFTS P H
htpy-precompose-total-lifts {A = A} {B} P {f} {g} H =
  htpy-toto
    { P = fam-lifts B P}
    ( fam-lifts A P)
    ( λ h → eq-htpy (h ·l H))
    ( precompose-lifts P f)
    ( triangle-precompose-lifts P H)

{- We show that when htpy-precompose-total-lifts is applied to htpy-refl, it
   computes to htpy-refl. -}

tr-id-left-subst :
  {i j : Level} {A : UU i} {B : UU j} {f : A → B} {x y : A}
  (p : Id x y) (b : B) → (q : Id (f x) b) →
  Id (tr (λ (a : A) → Id (f a) b) p q) ((inv (ap f p)) ∙ q)
tr-id-left-subst refl b q = refl

compute-htpy-precompose-total-lifts :
  { l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
  ( f : A → B) →
  ( htpy-precompose-total-lifts P (htpy-refl' f)) ~
  ( htpy-refl' (toto (fam-lifts A P) (λ h → h ∘ f) (precompose-lifts P f)))
compute-htpy-precompose-total-lifts {A = A} P f (pair h h') =
  let α = λ (t : Id (h ∘ f) (h ∘ f)) → tr (fam-lifts A P) t (λ a → h' (f a))
  in
  ap eq-pair'
    ( eq-pair
      ( eq-htpy-htpy-refl (h ∘ f))
      ( ( tr-id-left-subst
          { f = α}
          ( eq-htpy-htpy-refl (h ∘ f))
          ( λ a → h' (f a))
          ( triangle-precompose-lifts P htpy-refl h h')) ∙
        ( ( ap
            ( λ t → inv (ap α (eq-htpy-htpy-refl (λ a → h (f a)))) ∙ t)
            ( htpy-eq
              ( htpy-eq (compute-triangle-precompose-lifts P f) h) h')) ∙
          ( left-inv (triangle-precompose-lifts-htpy-refl P f h h')))))

COHERENCE-HTPY-INV-CHOICE-∞ :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
  {f g : A → B} (H : f ~ g) → UU _
COHERENCE-HTPY-INV-CHOICE-∞ P {f} {g} H =
  ( ( coherence-square-inv-choice-∞ P f) ∙h
    ( inv-choice-∞ ·l ( htpy-precompose-total-lifts P H))) ~
  ( ( ( λ h → eq-htpy (h ·l H)) ·r inv-choice-∞) ∙h
    ( coherence-square-inv-choice-∞ P g))

coherence-htpy-inv-choice-∞-htpy-refl :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
  (f : A → B) → COHERENCE-HTPY-INV-CHOICE-∞ P (htpy-refl' f)
coherence-htpy-inv-choice-∞-htpy-refl {X = X} P f =
  ( htpy-ap-concat
    ( coherence-square-inv-choice-∞ P f)
    ( inv-choice-∞ ·l ( htpy-precompose-total-lifts P htpy-refl))
    ( htpy-refl)
    ( λ h →
      ap (ap inv-choice-∞) (compute-htpy-precompose-total-lifts P f h))) ∙h
  ( htpy-inv
    ( htpy-ap-concat'
      ( ( htpy-precomp htpy-refl (Σ X P)) ·r inv-choice-∞)
      ( htpy-refl)
      ( htpy-refl)
      ( λ h → compute-htpy-precomp f (Σ X P) (inv-choice-∞ h))))

abstract
  coherence-htpy-inv-choice-∞ :
    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (P : X → UU l4)
    {f g : A → B} (H : f ~ g) → COHERENCE-HTPY-INV-CHOICE-∞ P H
  coherence-htpy-inv-choice-∞ P {f} =
    ind-htpy f
      ( λ g H → COHERENCE-HTPY-INV-CHOICE-∞ P H)
      ( coherence-htpy-inv-choice-∞-htpy-refl P f)

cone-family-dependent-pullback-property :
  {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g X) (P : X → UU l) →
  cone-family
    ( fam-lifts S P)
    ( precompose-lifts P f)
    ( precompose-lifts P g)
    ( cone-pullback-property-pushout f g c X)
    ( fam-lifts X P)
cone-family-dependent-pullback-property f g c P γ =
  pair
    ( precompose-lifts P (pr1 c) γ)
    ( pair
      ( precompose-lifts P (pr1 (pr2 c)) γ)
      ( triangle-precompose-lifts P (pr2 (pr2 c)) γ))

is-pullback-cone-family-dependent-pullback-property :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g X) →
  ((l : Level) → pullback-property-pushout l f g c) →
  {l : Level} (P : X → UU l) (γ : X → X) →
  is-pullback
    ( ( tr (fam-lifts S P) (eq-htpy (γ ·l (pr2 (pr2 c))))) ∘
      ( precompose-lifts P f (γ ∘ (pr1 c))))
    ( precompose-lifts P g (γ ∘ (pr1 (pr2 c))))
    ( cone-family-dependent-pullback-property f g c P γ)
is-pullback-cone-family-dependent-pullback-property {S = S} {A} {B} {X}
  f g (pair i (pair j H)) pb-c P =
  let c = pair i (pair j H) in
  is-pullback-family-is-pullback-tot
    ( fam-lifts S P)
    ( precompose-lifts P f)
    ( precompose-lifts P g)
    ( cone-pullback-property-pushout f g c X)
    ( cone-family-dependent-pullback-property f g c P)
    ( pb-c _ X)
    ( is-pullback-top-is-pullback-bottom-cube-is-equiv
      ( precomp i (Σ X P))
      ( precomp j (Σ X P))
      ( precomp f (Σ X P))
      ( precomp g (Σ X P))
      ( toto (fam-lifts A P) (precomp i X) (precompose-lifts P i))
      ( toto (fam-lifts B P) (precomp j X) (precompose-lifts P j))
      ( toto (fam-lifts S P) (precomp f X) (precompose-lifts P f))
      ( toto (fam-lifts S P) (precomp g X) (precompose-lifts P g))
      ( inv-choice-∞)
      ( inv-choice-∞)
      ( inv-choice-∞)
      ( inv-choice-∞)
      ( htpy-precompose-total-lifts P H)
      ( htpy-refl)
      ( htpy-refl)
      ( htpy-refl)
      ( htpy-refl)
      ( htpy-precomp H (Σ X P))
      ( coherence-htpy-inv-choice-∞ P H)
      ( is-equiv-inv-choice-∞)
      ( is-equiv-inv-choice-∞)
      ( is-equiv-inv-choice-∞)
      ( is-equiv-inv-choice-∞)
      ( pb-c _ (Σ X P)))

dependent-pullback-property-pullback-property-pushout :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g X) →
  ((l : Level) → pullback-property-pushout l f g c) →
  ((l : Level) → dependent-pullback-property-pushout l f g c)
dependent-pullback-property-pullback-property-pushout
  {S = S} {A} {B} {X}
  f g (pair i (pair j H)) pullback-c l P =
  let c = pair i (pair j H) in
  is-pullback-htpy'
    ( (tr (fam-lifts S P) (eq-htpy (id ·l H))) ∘ (precompose-lifts P f i))
    ( (tr-eq-htpy-fam-lifts P id H) ·r (precompose-lifts P f i))
    ( precompose-lifts P g j)
    ( htpy-refl)
    ( cone-family-dependent-pullback-property f g c P id)
    { c' = cone-dependent-pullback-property-pushout f g c P}
    ( pair htpy-refl
      ( pair htpy-refl
        ( htpy-right-unit ∙h (coherence-triangle-precompose-lifts P H id))))
    ( is-pullback-cone-family-dependent-pullback-property f g c pullback-c P id)

{- This concludes the proof of Theorem 18.1.4. -}

{- We give some further useful implications -}

dependent-universal-property-universal-property-pushout :
  { l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  ( f : S → A) (g : S → B) (c : cocone f g X) →
  ( (l : Level) → universal-property-pushout l f g c) →
  ( (l : Level) → dependent-universal-property-pushout l f g c)
dependent-universal-property-universal-property-pushout f g c up-X =
  dependent-universal-property-dependent-pullback-property-pushout f g c
    ( dependent-pullback-property-pullback-property-pushout f g c
      ( λ l → pullback-property-pushout-universal-property-pushout l f g c
        ( up-X l)))

-- Section 16.2 Families over pushouts

{- Definition 18.2.1 -}

Fam-pushout :
  {l1 l2 l3 : Level} (l : Level) {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) → UU (l1 ⊔ (l2 ⊔ (l3 ⊔ lsuc l)))
Fam-pushout l {S} {A} {B} f g =
  Σ ( A → UU l)
    ( λ PA → Σ (B → UU l)
      ( λ PB → (s : S) → PA (f s) ≃ PB (g s)))

{- We characterize the identity type of Fam-pushout. -}

coherence-equiv-Fam-pushout :
  { l1 l2 l3 l l' : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  { f : S → A} {g : S → B}
  ( P : Fam-pushout l f g) (Q : Fam-pushout l' f g) →
  ( eA : (a : A) → (pr1 P a) ≃ (pr1 Q a))
  ( eB : (b : B) → (pr1 (pr2 P) b) ≃ (pr1 (pr2 Q) b)) →
  UU (l1 ⊔ l ⊔ l')
coherence-equiv-Fam-pushout {S = S} {f = f} {g} P Q eA eB =
  ( s : S) →
    ( (map-equiv (eB (g s))) ∘ (map-equiv (pr2 (pr2 P) s))) ~
    ( (map-equiv (pr2 (pr2 Q) s)) ∘ (map-equiv (eA (f s))))

equiv-Fam-pushout :
  {l1 l2 l3 l l' : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  {f : S → A} {g : S → B} →
  Fam-pushout l f g → Fam-pushout l' f g → UU (l1 ⊔ l2 ⊔ l3 ⊔ l ⊔ l')
equiv-Fam-pushout {S = S} {A} {B} {f} {g} P Q =
  Σ ( (a : A) → (pr1 P a) ≃ (pr1 Q a)) ( λ eA →
    Σ ( (b : B) → (pr1 (pr2 P) b) ≃ (pr1 (pr2 Q) b))
      ( coherence-equiv-Fam-pushout P Q eA))

reflexive-equiv-Fam-pushout :
  {l1 l2 l3 l : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  {f : S → A} {g : S → B} (P : Fam-pushout l f g) →
  equiv-Fam-pushout P P
reflexive-equiv-Fam-pushout (pair PA (pair PB PS)) =
  pair (λ a → equiv-id (PA a))
    ( pair
      ( λ b → equiv-id (PB b))
      ( λ s → htpy-refl))

equiv-Fam-pushout-eq :
  {l1 l2 l3 l : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  {f : S → A} {g : S → B} {P Q : Fam-pushout l f g} →
  Id P Q → equiv-Fam-pushout P Q
equiv-Fam-pushout-eq {P = P} {.P} refl =
  reflexive-equiv-Fam-pushout P

is-contr-total-equiv-Fam-pushout :
  {l1 l2 l3 l : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  {f : S → A} {g : S → B} (P : Fam-pushout l f g) →
  is-contr (Σ (Fam-pushout l f g) (equiv-Fam-pushout P))
is-contr-total-equiv-Fam-pushout {S = S} {A} {B} {f} {g} P =
  is-contr-total-Eq-structure
    ( λ PA' t eA →
      Σ ( (b : B) → (pr1 (pr2 P) b) ≃ (pr1 t b))
        ( coherence-equiv-Fam-pushout P (pair PA' t) eA))
    ( is-contr-total-Eq-Π
      ( λ a X → (pr1 P a) ≃ X)
      ( λ a → is-contr-total-equiv (pr1 P a))
      ( pr1 P))
    ( pair (pr1 P) (λ a → equiv-id (pr1 P a)))
    ( is-contr-total-Eq-structure
      ( λ PB' PS' eB →
        coherence-equiv-Fam-pushout
          P (pair (pr1 P) (pair PB' PS'))
          (λ a → equiv-id (pr1 P a)) eB)
      ( is-contr-total-Eq-Π
        ( λ b Y → (pr1 (pr2 P) b) ≃ Y)
        ( λ b → is-contr-total-equiv (pr1 (pr2 P) b))
        ( pr1 (pr2 P)))
      ( pair (pr1 (pr2 P)) (λ b → equiv-id (pr1 (pr2 P) b)))
      ( is-contr-total-Eq-Π
        ( λ s e → (map-equiv (pr2 (pr2 P) s)) ~ (map-equiv e))
        ( λ s → is-contr-total-htpy-equiv (pr2 (pr2 P) s))
        ( pr2 (pr2 P))))

is-equiv-equiv-Fam-pushout-eq :
  {l1 l2 l3 l : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  {f : S → A} {g : S → B} (P Q : Fam-pushout l f g) →
  is-equiv (equiv-Fam-pushout-eq {P = P} {Q})
is-equiv-equiv-Fam-pushout-eq P =
  fundamental-theorem-id P
    ( reflexive-equiv-Fam-pushout P)
    ( is-contr-total-equiv-Fam-pushout P)
    ( λ Q → equiv-Fam-pushout-eq {P = P} {Q})

equiv-equiv-Fam-pushout :
  {l1 l2 l3 l : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  {f : S → A} {g : S → B} (P Q : Fam-pushout l f g) →
  Id P Q ≃ equiv-Fam-pushout P Q
equiv-equiv-Fam-pushout P Q =
  pair
    ( equiv-Fam-pushout-eq)
    ( is-equiv-equiv-Fam-pushout-eq P Q)

eq-equiv-Fam-pushout :
  {l1 l2 l3 l : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  {f : S → A} {g : S → B} {P Q : Fam-pushout l f g} →
  (equiv-Fam-pushout P Q) → Id P Q
eq-equiv-Fam-pushout {P = P} {Q} =
  inv-is-equiv (is-equiv-equiv-Fam-pushout-eq P Q)

issec-eq-equiv-Fam-pushout :
  { l1 l2 l3 l : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  { f : S → A} {g : S → B} {P Q : Fam-pushout l f g} →
  ( ( equiv-Fam-pushout-eq {P = P} {Q}) ∘
    ( eq-equiv-Fam-pushout {P = P} {Q})) ~ id
issec-eq-equiv-Fam-pushout {P = P} {Q} =
  issec-inv-is-equiv (is-equiv-equiv-Fam-pushout-eq P Q)

isretr-eq-equiv-Fam-pushout :
  {l1 l2 l3 l : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  {f : S → A} {g : S → B} {P Q : Fam-pushout l f g} →
  ( ( eq-equiv-Fam-pushout {P = P} {Q}) ∘
    ( equiv-Fam-pushout-eq {P = P} {Q})) ~ id
isretr-eq-equiv-Fam-pushout {P = P} {Q} =
  isretr-inv-is-equiv (is-equiv-equiv-Fam-pushout-eq P Q)

{- This concludes the characterization of the identity type of Fam-pushout. -}

{- Definition 18.2.2 -}

desc-fam :
  {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  {f : S → A} {g : S → B} (c : cocone f g X) →
  (P : X → UU l) → Fam-pushout l f g
desc-fam c P =
  pair
    ( P ∘ (pr1 c))
    ( pair
      ( P ∘ (pr1 (pr2 c)))
      ( λ s → (pair (tr P (pr2 (pr2 c) s)) (is-equiv-tr P (pr2 (pr2 c) s)))))

{- Theorem 18.2.3 -}

Fam-pushout-cocone-UU :
  {l1 l2 l3 : Level} (l : Level) {S : UU l1} {A : UU l2} {B : UU l3}
  {f : S → A} {g : S → B} → cocone f g (UU l) → Fam-pushout l f g
Fam-pushout-cocone-UU l =
  tot (λ PA → (tot (λ PB H s → equiv-eq (H s))))

is-equiv-Fam-pushout-cocone-UU :
  {l1 l2 l3 : Level} (l : Level) {S : UU l1} {A : UU l2} {B : UU l3}
  {f : S → A} {g : S → B} →
  is-equiv (Fam-pushout-cocone-UU l {f = f} {g})
is-equiv-Fam-pushout-cocone-UU l {f = f} {g} =
  is-equiv-tot-is-fiberwise-equiv
    ( λ PA → is-equiv-tot-is-fiberwise-equiv
      ( λ PB → is-equiv-postcomp-Π
        ( λ s → equiv-eq)
        ( λ s → univalence (PA (f s)) (PB (g s)))))

htpy-equiv-eq-ap-fam :
  {l1 l2 : Level} {A : UU l1} (B : A → UU l2) {x y : A} (p : Id x y) →
  htpy-equiv (equiv-tr B p) (equiv-eq (ap B p))
htpy-equiv-eq-ap-fam B {x} {.x} refl =
  reflexive-htpy-equiv (equiv-id (B x))

triangle-desc-fam :
  {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  {f : S → A} {g : S → B} (c : cocone f g X) →
  ( desc-fam {l = l} c) ~
  ( ( Fam-pushout-cocone-UU l {f = f} {g}) ∘ ( cocone-map f g {Y = UU l} c))
triangle-desc-fam {l = l} {S} {A} {B} {X} (pair i (pair j H)) P =
  eq-equiv-Fam-pushout
    ( pair
      ( λ a → equiv-id (P (i a)))
      ( pair
        ( λ b → equiv-id (P (j b)))
        ( λ s → htpy-equiv-eq-ap-fam P (H s))))

is-equiv-desc-fam :
  {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  {f : S → A} {g : S → B} (c : cocone f g X) →
  ((l' : Level) → universal-property-pushout l' f g c) →
  is-equiv (desc-fam {l = l} {f = f} {g} c)
is-equiv-desc-fam {l = l} {f = f} {g} c up-c =
  is-equiv-comp
    ( desc-fam c)
    ( Fam-pushout-cocone-UU l)
    ( cocone-map f g c)
    ( triangle-desc-fam c)
    ( up-c (lsuc l) (UU l))
    ( is-equiv-Fam-pushout-cocone-UU l)

equiv-desc-fam :
  {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  {f : S → A} {g : S → B} (c : cocone f g X) →
  ((l' : Level) → universal-property-pushout l' f g c) →
  (X → UU l) ≃ Fam-pushout l f g
equiv-desc-fam c up-c =
  pair
    ( desc-fam c)
    ( is-equiv-desc-fam c up-c)

{- Corollary 18.2.4 -}

uniqueness-Fam-pushout :
  {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g X) →
  ((l' : Level) → universal-property-pushout l' f g c) →
  ( P : Fam-pushout l f g) →
  is-contr
    ( Σ (X → UU l) (λ Q →
      equiv-Fam-pushout P (desc-fam c Q)))
uniqueness-Fam-pushout {l = l} f g c up-c P =
  is-contr-equiv'
    ( fib (desc-fam c) P)
    ( equiv-tot (λ Q →
      ( equiv-equiv-Fam-pushout P (desc-fam c Q)) ∘e
      ( equiv-inv (desc-fam c Q) P)))
    ( is-contr-map-is-equiv (is-equiv-desc-fam c up-c) P)

fam-Fam-pushout :
  {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  {f : S → A} {g : S → B} (c : cocone f g X) →
  (up-X : (l' : Level) → universal-property-pushout l' f g c) →
  Fam-pushout l f g → (X → UU l)
fam-Fam-pushout {f = f} {g} c up-X P =
  pr1 (center (uniqueness-Fam-pushout f g c up-X P))

issec-fam-Fam-pushout :
  {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  {f : S → A} {g : S → B} (c : cocone f g X) →
  (up-X : (l' : Level) → universal-property-pushout l' f g c) →
  ((desc-fam {l = l} c) ∘ (fam-Fam-pushout c up-X)) ~ id
issec-fam-Fam-pushout {f = f} {g} c up-X P =
  inv (eq-equiv-Fam-pushout (pr2 (center (uniqueness-Fam-pushout f g c up-X P))))

comp-left-fam-Fam-pushout :
  { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  { f : S → A} {g : S → B} (c : cocone f g X) →
  ( up-X : (l' : Level) → universal-property-pushout l' f g c) →
  ( P : Fam-pushout l f g) →
  ( a : A) → (pr1 P a) ≃ (fam-Fam-pushout c up-X P (pr1 c a))
comp-left-fam-Fam-pushout {f = f} {g} c up-X P =
  pr1 (pr2 (center (uniqueness-Fam-pushout f g c up-X P)))

comp-right-fam-Fam-pushout :
  { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  { f : S → A} {g : S → B} (c : cocone f g X) →
  ( up-X : (l' : Level) → universal-property-pushout l' f g c) →
  ( P : Fam-pushout l f g) →
  ( b : B) → (pr1 (pr2 P) b) ≃ (fam-Fam-pushout c up-X P (pr1 (pr2 c) b))
comp-right-fam-Fam-pushout {f = f} {g} c up-X P =
  pr1 (pr2 (pr2 (center (uniqueness-Fam-pushout f g c up-X P))))

comp-path-fam-Fam-pushout :
  { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  { f : S → A} {g : S → B} (c : cocone f g X) →
  ( up-X : (l' : Level) → universal-property-pushout l' f g c) →
  ( P : Fam-pushout l f g) →
  ( s : S) →
    ( ( map-equiv (comp-right-fam-Fam-pushout c up-X P (g s))) ∘
      ( map-equiv (pr2 (pr2 P) s))) ~
    ( ( tr (fam-Fam-pushout c up-X P) (pr2 (pr2 c) s)) ∘
      ( map-equiv (comp-left-fam-Fam-pushout c up-X P (f s))))
comp-path-fam-Fam-pushout {f = f} {g} c up-X P =
  pr2 (pr2 (pr2 (center (uniqueness-Fam-pushout f g c up-X P))))

{-
-- Section 18.3 The Flattening lemma for pushouts

{- Definition 18.3.1 -}

cocone-flattening-pushout :
  { l1 l2 l3 l4 l5 : Level}
  { S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  ( f : S → A) (g : S → B) (c : cocone f g X)
  ( P : Fam-pushout l5 f g)
  ( Q : X → UU l5)
  ( e : equiv-Fam-pushout P (desc-fam f g c Q)) →
  cocone
    ( toto (pr1 P) f (λ s → id))
    ( toto (pr1 (pr2 P)) g (λ s → map-equiv (pr2 (pr2 P) s)))
    ( Σ X Q)
cocone-flattening-pushout f g c P Q e =
  pair
    ( toto Q
      ( pr1 c)
      ( λ a → map-equiv (pr1 e a)))
    ( pair
      ( toto Q
        ( pr1 (pr2 c))
        ( λ b → map-equiv (pr1 (pr2 e) b)))
      ( htpy-toto Q
        ( pr2 (pr2 c))
        ( λ s → map-equiv (pr1 e (f s)))
        ( λ s → htpy-inv (pr2 (pr2 e) s))))

{- Theorem 18.3.2 The flattening lemma -}

coherence-bottom-flattening-lemma' :
  {l1 l2 l3 : Level} {B : UU l1} {Q : B → UU l2} {T : UU l3}
  {b b' : B} (α : Id b b') {y : Q b} {y' : Q b'} (β : Id (tr Q α y) y')
  (h : (b : B) → Q b → T) → Id (h b y) (h b' y')
coherence-bottom-flattening-lemma' refl refl h = refl

coherence-bottom-flattening-lemma :
  {l1 l2 l3 l4 l5 : Level}
  {A : UU l1} {B : UU l2} {P : A → UU l3} {Q : B → UU l4} {T : UU l5}
  {f f' : A → B} (H : f ~ f')
  {g : (a : A) → P a → Q (f a)}
  {g' : (a : A) → P a → Q (f' a)}
  (K : (a : A) → ((tr Q (H a)) ∘ (g a)) ~ (g' a))
  (h : (b : B) → Q b → T) → (a : A) (p : P a) →
  Id (h (f a) (g a p)) (h (f' a) (g' a p))
coherence-bottom-flattening-lemma H K h a p =
  coherence-bottom-flattening-lemma' (H a) (K a p) h

coherence-cube-flattening-lemma :
  {l1 l2 l3 l4 l5 : Level}
  {A : UU l1} {B : UU l2} {P : A → UU l3} {Q : B → UU l4} {T : UU l5}
  {f f' : A → B} (H : f ~ f')
  {g : (a : A) → P a → Q (f a)}
  {g' : (a : A) → P a → Q (f' a)}
  (K : (a : A) → ((tr Q (H a)) ∘ (g a)) ~ (g' a))
  (h : Σ B Q → T) →
  Id ( eq-htpy
       ( λ a → eq-htpy
         ( coherence-bottom-flattening-lemma H K (ev-pair h) a)))
     ( ap ev-pair
       ( htpy-precomp (htpy-toto Q H g K) T h))
coherence-cube-flattening-lemma {A = A} {B} {P} {Q} {T} {f = f} {f'} H {g} {g'} K = ind-htpy f
    ( λ f' H' →
      (g : (a : A) → P a → Q (f a)) (g' : (a : A) → P a → Q (f' a))
      (K : (a : A) → ((tr Q (H' a)) ∘ (g a)) ~ (g' a)) (h : Σ B Q → T) →
      Id ( eq-htpy
           ( λ a → eq-htpy
             ( coherence-bottom-flattening-lemma H' K (ev-pair h) a)))
         ( ap ev-pair
           ( htpy-precomp (htpy-toto Q H' g K) T h)))
    ( λ g g' K h → {!ind-htpy g (λ g' K' → (h : Σ B Q → T) →
      Id ( eq-htpy
           ( λ a → eq-htpy
             ( coherence-bottom-flattening-lemma htpy-refl (λ a → htpy-eq (K' a)) (ev-pair h) a)))
         ( ap ev-pair
           ( htpy-precomp (htpy-toto Q htpy-refl g (λ a → htpy-eq (K' a))) T h))) ? (λ a → eq-htpy (K a)) h!})
    H g g' K

flattening-pushout' :
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g X) →
  ( P : Fam-pushout l5 f g)
  ( Q : X → UU l5)
  ( e : equiv-Fam-pushout P (desc-fam f g c Q)) →
  (l : Level) →
  pullback-property-pushout l
    ( toto (pr1 P) f (λ s → id))
    ( toto (pr1 (pr2 P)) g (λ s → map-equiv (pr2 (pr2 P) s)))
    ( cocone-flattening-pushout f g c P Q e)
flattening-pushout' f g c P Q e l T =
  is-pullback-top-is-pullback-bottom-cube-is-equiv
    ( ( postcomp-Π (λ x → precomp-Π (map-equiv (pr1 e x)) (λ q → T))) ∘
      ( precomp-Π (pr1 c) (λ x → (Q x) → T)))
    ( ( postcomp-Π (λ x → precomp-Π (map-equiv (pr1 (pr2 e) x)) (λ q → T))) ∘
      ( precomp-Π (pr1 (pr2 c)) (λ x → (Q x) → T)))
    ( precomp-Π f (λ a → (pr1 P a) → T))
    ( ( postcomp-Π (λ s → precomp (map-equiv (pr2 (pr2 P) s)) T)) ∘
      ( precomp-Π g (λ b → (pr1 (pr2 P) b) → T)))
    ( precomp (toto Q (pr1 c) (λ a → map-equiv (pr1 e a))) T)
    ( precomp (toto Q (pr1 (pr2 c)) (λ b → map-equiv (pr1 (pr2 e) b))) T)
    ( precomp (toto (pr1 P) f (λ s → id)) T)
    ( precomp (toto (pr1 (pr2 P)) g (λ s → map-equiv (pr2 (pr2 P) s))) T)
    ev-pair
    ev-pair
    ev-pair
    ev-pair
    ( htpy-precomp
      ( htpy-toto Q
        ( pr2 (pr2 c))
        ( λ s → map-equiv (pr1 e (f s)))
        ( λ s → htpy-inv (pr2 (pr2 e) s)))
      ( T))
    htpy-refl
    htpy-refl
    htpy-refl
    htpy-refl
    ( λ h → eq-htpy (λ s → eq-htpy
      ( coherence-bottom-flattening-lemma
        ( pr2 (pr2 c))
        ( λ s → htpy-inv (pr2 (pr2 e) s))
        ( h)
        ( s))))
    {!!}
    is-equiv-ev-pair
    is-equiv-ev-pair
    is-equiv-ev-pair
    is-equiv-ev-pair
    {!!}

flattening-pushout :
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g X) →
  ( P : Fam-pushout l5 f g)
  ( Q : X → UU l5)
  ( e : equiv-Fam-pushout P (desc-fam f g c Q)) →
  (l : Level) →
  universal-property-pushout l
    ( toto (pr1 P) f (λ s → id))
    ( toto (pr1 (pr2 P)) g (λ s → map-equiv (pr2 (pr2 P) s)))
    ( cocone-flattening-pushout f g c P Q e)
flattening-pushout f g c P Q e l =
  universal-property-pushout-pullback-property-pushout l
    ( toto (pr1 P) f (λ s → id))
    ( toto (pr1 (pr2 P)) g (λ s → map-equiv (pr2 (pr2 P) s)))
    ( cocone-flattening-pushout f g c P Q e)
    ( flattening-pushout' f g c P Q e l)
-}

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma

record Monad (M : Set → Set) : Set₁ where
  field
    return : {A : Set} → A → M A
    _>>=_  : {A B : Set} → M A → (A → M B) → M B

open Monad ⦃ … ⦄

postulate
  F G : Set → Set

instance

  postulate
    G-monad : Monad G
    F-monad : Monad F

f : Σ Nat (λ _ → Nat) → F Nat
f p = do
  m , n ← return p
  return (m n)

-- Should jump to `m n` and list the F-monad candidate error first.

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K #-}
module Model.Nat where

open import Model.Size as MS using
  ( Size ; Sizes ; _≤_ ; _<_ ; ≤-IsProp ; nat )
open import Model.Type.Core
open import Util.HoTT.HLevel
open import Util.Prelude
open import Util.Relation.Binary.PropositionalEquality using (Σ-≡⁺)

import Data.Nat.Properties as ℕ

open Size

ℕ≤ : Size → Set
ℕ≤ n = ∃[ m ] (nat m ≤ n)

ℕ≤-IsSet : ∀ {n} → IsSet (ℕ≤ n)
ℕ≤-IsSet = Σ-IsSet ℕ.≡-irrelevant λ m → IsOfHLevel-suc 1 ≤-IsProp

abstract
  ℕ≤-≡⁺ : ∀ {n} {m m′} (m≤n : nat m ≤ n) (m′≤n : nat m′ ≤ n)
    → m ≡ m′
    → (m , m≤n) ≡ (m′ , m′≤n)
  ℕ≤-≡⁺ _ _ m≡m′ = Σ-≡⁺ (m≡m′ , ≤-IsProp _ _)

Nat : ⟦Type⟧ Sizes
Nat = record
  { ObjHSet = λ n → HLevel⁺ (ℕ≤ n) ℕ≤-IsSet
  ; eqHProp = λ { _ (n , _) (m , _) → HLevel⁺ (n ≡ m) ℕ.≡-irrelevant }
  ; eq-refl = λ _ → refl
  }

castℕ≤ : ∀ {n m} → n ≤ m → ℕ≤ n → ℕ≤ m
castℕ≤ n≤m (k , k≤n) = k , go
  where abstract go = MS.≤-trans k≤n n≤m

zero≤ : ∀ n → ℕ≤ n
zero≤ n = 0 , MS.0≤n

suc≤ : ∀ n m → m < n → ℕ≤ m → ℕ≤ n
suc≤ n m m<n (x , x≤m) = suc x , MS.n<m→Sn≤m (MS.≤→<→< x≤m m<n)

caseℕ≤ : ∀ {α} {A : Set α} {n}
  → ℕ≤ n
  → A
  → (∀ m → m < n → ℕ≤ m → A)
  → A
caseℕ≤ (zero , _) z s = z
caseℕ≤ (suc x , Sx≤n) z s = s (nat x) (MS.Sn≤m→n<m Sx≤n) (x , MS.≤-refl)

caseℕ≤-pres : ∀ {α β γ} {A : Set α} {A′ : Set β} {n n′}
  → (R : A → A′ → Set γ)
  → (i : ℕ≤ n) (i′ : ℕ≤ n′)
  → (z : A) (z′ : A′)
  → (s : ∀ m → m < n → ℕ≤ m → A) (s′ : ∀ m → m < n′ → ℕ≤ m → A′)
  → proj₁ i ≡ proj₁ i′
  → R z z′
  → (∀ m m<n m′ m′<n′ j j′
      → proj₁ j ≡ proj₁ j′
      → R (s m m<n j) (s′ m′ m′<n′ j′))
  → R (caseℕ≤ i z s) (caseℕ≤ i′ z′ s′)
caseℕ≤-pres R (zero , _) (_ , _) z z′ s s′ refl zRz′ sRs′ = zRz′
caseℕ≤-pres R (suc i , _) (_ , _) z z′ s s′ refl zRz′ sRs′
  = sRs′ _ _ _ _ _ _ refl

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Data.Nat.Properties using (+-assoc; +-comm)

module Exercises.One where

_*_ : ℕ → ℕ → ℕ
zero * y = zero
suc x * y = y + (x * y)

-- Prove that multiplication is commutative
*-idʳ : ∀ x → x * 0 ≡ 0
*-idʳ zero = refl
*-idʳ (suc x) = *-idʳ x

*-suc : ∀ x y → x + (x * y) ≡ (x * suc y)
*-suc zero y = refl
*-suc (suc x) y
  rewrite sym (+-assoc x y (x * y)) | +-comm x y |
          +-assoc y x (x * y) | *-suc x y = refl

*-comm : ∀ x y → x * y ≡ y * x
*-comm zero y rewrite *-idʳ y = refl
*-comm (suc x) y rewrite *-comm x y | *-suc y x = refl

-- Prove that if x + x ≡ y + y then x ≡ y (taken from CodeWars)
suc-injective : ∀ x y → suc x ≡ suc y → x ≡ y
suc-injective zero zero p = refl
suc-injective (suc x) (suc .x) refl = refl

xxyy : ∀ x y → x + x ≡ y + y → x ≡ y
xxyy zero zero refl = refl
xxyy (suc x) (suc y) p rewrite +-comm x (suc x) | +-comm y (suc y) =
  cong suc (xxyy x y (suc-injective _ _ (suc-injective _ _ p)))


text:
{-# OPTIONS --cubical --safe #-}

open import Prelude
open import Categories

module Categories.Pullback {ℓ₁ ℓ₂} (C : Category ℓ₁ ℓ₂) where

open Category C

record Pullback (f : X ⟶ Z) (g : Y ⟶ Z) : Type (ℓ₁ ℓ⊔ ℓ₂) where
  field
    {P} : Ob
    p₁ : P ⟶ X
    p₂ : P ⟶ Y
    commute : f · p₁ ≡ g · p₂
    ump : ∀ {A : Ob} (h₁ : A ⟶ X) (h₂ : A ⟶ Y) → f · h₁ ≡ g · h₂ →
              ∃![ u ] ((p₁ · u ≡ h₁) × (p₂ · u ≡ h₂))

HasPullbacks : Type (ℓ₁ ℓ⊔ ℓ₂)
HasPullbacks = ∀ {X Y Z} (f : X ⟶ Z) (g : Y ⟶ Z) → Pullback f g

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.Instances.Pointwise where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Algebra.CommRing.Base

private
  variable
    ℓ : Level

pointwiseRing : (X : Type ℓ) (R : CommRing ℓ) → CommRing ℓ
pointwiseRing X R = (X → fst R) , str
    where
      open CommRingStr (snd R)

      isSetX→R = isOfHLevelΠ 2 (λ _ → isSetCommRing R)

      str : CommRingStr (X → fst R)
      CommRingStr.0r str = λ _ → 0r
      CommRingStr.1r str = λ _ → 1r
      CommRingStr._+_ str = λ f g → (λ x → f x + g x)
      CommRingStr._·_ str = λ f g → (λ x → f x · g x)
      CommRingStr.- str = λ f → (λ x → - f x)
      CommRingStr.isCommRing str =
        makeIsCommRing
           isSetX→R
           (λ f g h i x → +Assoc (f x) (g x) (h x) i)
           (λ f i x → +IdR (f x) i)
           (λ f i x → +InvR (f x) i)
           (λ f g i x → +Comm (f x) (g x) i)
           (λ f g h i x → ·Assoc (f x) (g x) (h x) i)
           (λ f i x → ·IdR (f x) i)
           (λ f g h i x → ·DistR+ (f x) (g x) (h x) i)
           λ f g i x → ·Comm (f x) (g x) i

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Issue152 where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ    #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

f : ℕ → ℕ
f 0 with zero
f 0 | n = n
f 1 with zero
f 1 | n = n
f n = n

g : ℕ → ℕ
g 0    with zero
g zero | n = n
g 1    with zero
g (suc zero) | n = n
g n = n

h : ℕ → ℕ
h zero with zero
h 0    | n = n
h (suc zero) with zero
h 1 | n = n
h n = n

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Structure.Operator.Vector where

open import Functional using (swap)
import      Lvl
open import Logic
open import Logic.Propositional
open import Structure.Setoid
open import Structure.Operator.Field
open import Structure.Operator.Group
open import Structure.Operator.Monoid
import      Structure.Operator.Names as Names
open import Structure.Operator.Properties
open import Structure.Operator
open import Type

record VectorSpace {ℓᵥ ℓₛ ℓᵥₑ ℓₛₑ}
                   {V : Type{ℓᵥ}} ⦃ _ : Equiv{ℓᵥₑ}(V) ⦄
                   {S : Type{ℓₛ}} ⦃ _ : Equiv{ℓₛₑ}(S) ⦄
                   (_+ᵥ_ : V → V → V)
                   (_⋅ₛᵥ_ : S → V → V)
                   (_+ₛ_ : S → S → S)
                   (_⋅ₛ_ : S → S → S)
                   : Stmt{ℓₛₑ Lvl.⊔ ℓₛ Lvl.⊔ ℓᵥₑ Lvl.⊔ ℓᵥ} where
  constructor intro
  field
    ⦃ scalarField ⦄            : Field(_+ₛ_)(_⋅ₛ_)
    ⦃ vectorCommutativeGroup ⦄ : CommutativeGroup(_+ᵥ_)

  open Field(scalarField)
    renaming (
      𝟎 to 𝟎ₛ ;
      𝟏 to 𝟏ₛ ;
      _−_ to _−ₛ_ ;
      _/_ to _/ₛ_ ;
      −_ to −ₛ_ ;
      ⅟ to ⅟ₛ ;
      [+]-group              to [+ₛ]-group ;
      [+]-commutativity      to [+ₛ]-commutativity ;
      [+]-monoid             to [+ₛ]-monoid ;
      [+]-binary-operator    to [+ₛ]-binary-operator ;
      [+]-associativity      to [+ₛ]-associativity ;
      [+]-identity-existence to [+ₛ]-identity-existence ;
      [+]-identity           to [+ₛ]-identity ;
      [+]-identityₗ          to [+ₛ]-identityₗ ;
      [+]-identityᵣ          to [+ₛ]-identityᵣ ;
      [+]-inverse-existence  to [+ₛ]-inverse-existence ;
      [+]-inverse            to [+ₛ]-inverse ;
      [+]-inverseₗ           to [+ₛ]-inverseₗ ;
      [+]-inverseᵣ           to [+ₛ]-inverseᵣ ;
      [−]-function           to [−ₛ]-function ;
      [⋅]-binary-operator    to [⋅ₛ]-binary-operator ;
      [⋅]-associativity      to [⋅ₛ]-associativity ;
      [⋅]-identity-existence to [⋅ₛ]-identity-existence ;
      [⋅]-identity           to [⋅ₛ]-identity ;
      [⋅]-identityₗ          to [⋅ₛ]-identityₗ ;
      [⋅]-identityᵣ          to [⋅ₛ]-identityᵣ ;
      [⋅]-inverseₗ           to [⋅ₛ]-inverseₗ ;
      [⋅]-inverseᵣ           to [⋅ₛ]-inverseᵣ ;
      distinct-identities to distinct-identitiesₛ
    ) public
  open CommutativeGroup(vectorCommutativeGroup)
    renaming (
      id to 𝟎ᵥ ;
      inv to −ᵥ_ ;
      inv-op to _−ᵥ_ ;
      group               to [+ᵥ]-group;
      commutativity       to [+ᵥ]-commutativity;
      monoid              to [+ᵥ]-monoid ;
      binary-operator     to [+ᵥ]-binary-operator ;
      associativity       to [+ᵥ]-associativity ;
      identity-existence  to [+ᵥ]-identity-existence ;
      identity            to [+ᵥ]-identity ;
      identityₗ           to [+ᵥ]-identityₗ ;
      identityᵣ           to [+ᵥ]-identityᵣ ;
      inverse-existence   to [+ᵥ]-inverse-existence ;
      inverse             to [+ᵥ]-inverse ;
      inverseₗ            to [+ᵥ]-inverseₗ ;
      inverseᵣ            to [+ᵥ]-inverseᵣ ;
      inv-function        to [−ᵥ]-function
    ) public

  field
    ⦃ [⋅ₛᵥ]-binaryOperator ⦄      : BinaryOperator(_⋅ₛᵥ_)
    [⋅ₛ][⋅ₛᵥ]-compatibility       : Names.Compatibility(_⋅ₛ_)(_⋅ₛᵥ_) -- TODO: This is semigroup action
    ⦃ [⋅ₛᵥ]-identity ⦄            : Identityₗ(_⋅ₛᵥ_)(𝟏ₛ)
    ⦃ [⋅ₛᵥ][+ᵥ]-distributivityₗ ⦄ : Distributivityₗ(_⋅ₛᵥ_)(_+ᵥ_)
    [⋅ₛᵥ][+ₛ][+ᵥ]-distributivityᵣ : Names.DistributivityPatternᵣ(_⋅ₛᵥ_)(_+ₛ_)(_+ᵥ_) -- TODO: This is ∀? → Preserving₂

  _⋅ᵥₛ_ = swap(_⋅ₛᵥ_)

record VectorSpaceVObject {ℓᵥ ℓₛ ℓᵥₑ ℓₛₑ}
  {S : Type{ℓₛ}} ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  (_+ₛ_ : S → S → S)
  (_⋅ₛ_ : S → S → S)
  : Stmt{ℓₛₑ Lvl.⊔ ℓₛ Lvl.⊔ Lvl.𝐒(ℓᵥₑ Lvl.⊔ ℓᵥ)}
  where

  constructor intro
  field
    {Vector} : Type{ℓᵥ}
    ⦃ Vector-equiv ⦄ : Equiv{ℓᵥₑ}(Vector)
    _+ᵥ_ : Vector → Vector → Vector
    _⋅ₛᵥ_ : S → Vector → Vector
    ⦃ vectorSpace ⦄ : VectorSpace(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_)
  open VectorSpace(vectorSpace) public

record VectorSpaceObject {ℓᵥ ℓₛ ℓᵥₑ ℓₛₑ} : Stmt{Lvl.𝐒(ℓₛₑ Lvl.⊔ ℓₛ Lvl.⊔ ℓᵥₑ Lvl.⊔ ℓᵥ)} where
  constructor intro
  field
    {Vector} : Type{ℓᵥ}
    ⦃ equiv-Vector ⦄ : Equiv{ℓᵥₑ}(Vector)
    {Scalar} : Type{ℓₛ}
    ⦃ equiv-Scalar ⦄ : Equiv{ℓₛₑ}(Scalar)
    _+ᵥ_  : Vector → Vector → Vector
    _⋅ₛᵥ_ : Scalar → Vector → Vector
    _+ₛ_  : Scalar → Scalar → Scalar
    _⋅ₛ_  : Scalar → Scalar → Scalar
    ⦃ vectorSpace ⦄ : VectorSpace(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_)
  open VectorSpace(vectorSpace) public

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:
module Data.Char.Ranges where

open import Data.Char
open import Data.List
open import Data.Nat
open import Function

charRange : ℕ -> ℕ -> List Char
charRange start amount = applyUpTo (λ x -> fromℕ $ x + start) amount

UCletters : List Char
UCletters = charRange 65 26

LCletters : List Char
LCletters = charRange 97 26

greekLCletters : List Char
greekLCletters = charRange 945 25

greekUCletters : List Char
greekUCletters = charRange 913 25

symbols : List Char
symbols =
  applyUpTo (λ x -> fromℕ $ x + 33) 15
  ++ applyUpTo (λ x -> fromℕ $ x + 58) 7
  ++ applyUpTo (λ x -> fromℕ $ x + 91) 6
  ++ applyUpTo (λ x -> fromℕ $ x + 123) 4

digits : List Char
digits = charRange 48 10

letters : List Char
letters = UCletters ++ LCletters

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


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

open import Categories.Category

module Categories.Category.Complete.Properties {o ℓ e} (C : Category o ℓ e) where

open import Level
open import Data.Product
open import Relation.Binary

open import Categories.Category.Complete
open import Categories.Category.Complete.Finitely
open import Categories.Category.Construction.Functors
open import Categories.Diagram.Limit as Lim
open import Categories.Diagram.Limit.Properties
open import Categories.Diagram.Equalizer.Limit C
open import Categories.Diagram.Cone.Properties
open import Categories.Object.Product.Limit C
open import Categories.Object.Terminal.Limit C
open import Categories.Functor
open import Categories.Functor.Continuous
open import Categories.Functor.Properties
open import Categories.NaturalTransformation
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_)

import Categories.Category.Construction.Cones as Co
import Categories.Morphism.Reasoning as MR
import Categories.Morphism as Mor
import Categories.Morphism.Properties as Morₚ

private
  variable
    o′ ℓ′ e′ o″ ℓ″ e″ : Level
  module C = Category C

module _ (Com : Complete o′ ℓ′ e′ C) where

  Complete⇒FinitelyComplete : FinitelyComplete C
  Complete⇒FinitelyComplete = record
    { cartesian = record
      { terminal = limit⇒⊥ (Com (⊥⇒limit-F _ _ _))
      ; products = record
        { product = λ {A B} → limit⇒product (Com (product⇒limit-F _ _ _ A B))
        }
      }
    ; equalizer = λ f g → limit⇒equalizer (Com (equalizer⇒limit-F _ _ _ f g))
    }

module _ {D : Category o′ ℓ′ e′} (Com : Complete o″ ℓ″ e″ D) where
  private
    D^C = Functors C D
    module D^C = Category D^C
    module D   = Category D

    module _ {J : Category o″ ℓ″ e″} (F : Functor J D^C) where
      private
        module J = Category J
        module F = Functor F
        open F
        module F₀ j = Functor (F₀ j)
        module F₁ {a b} (f : a J.⇒ b) = NaturalTransformation (F₁ f)

      F[-,_] : C.Obj → Functor J D
      F[-, X ] = record
        { F₀           = λ j → F₀.₀ j X
        ; F₁           = λ f → F₁.η f X
        ; identity     = identity
        ; homomorphism = homomorphism
        ; F-resp-≈     = λ eq → F-resp-≈ eq -- this application cannot be eta reduced
        }

      F[-,-] : Functor C (Functors J D)
      F[-,-] = record
        { F₀           = F[-,_]
        ; F₁           = λ f → ntHelper record
          { η       = λ j → F₀.₁ j f
          ; commute = λ g → F₁.sym-commute g f
          }
        ; identity     = F₀.identity _
        ; homomorphism = F₀.homomorphism _
        ; F-resp-≈     = λ eq → F₀.F-resp-≈ _ eq
        }

      module F[-,-] = Functor F[-,-]

      module LimFX X = Limit (Com F[-, X ])
      open LimFX hiding (commute)

      K⇒lim : ∀ {X Y} (f : X C.⇒ Y) K → Co.Cones F[-, Y ] [ nat-map-Cone (F[-,-].₁ f) K , limit Y ]
      K⇒lim f K = rep-cone _ (nat-map-Cone (F[-,-].₁ f) K)

      lim⇒lim : ∀ {X Y} (f : X C.⇒ Y) → Co.Cones F[-, Y ] [ nat-map-Cone (F[-,-].₁ f) (limit X) , limit Y ]
      lim⇒lim f = K⇒lim f (limit _)

      module lim⇒lim {X Y} (f : X C.⇒ Y) = Co.Cone⇒ F[-, Y ] (lim⇒lim f)

      module FCone (K : Co.Cone F) where
        open Co.Cone F K public
        module N   = Functor N
        module ψ j = NaturalTransformation (ψ j)

      module FCone⇒ {K K′ : Co.Cone F} (K⇒K′ : Co.Cone⇒ F K K′) where
        open Co.Cone⇒ F K⇒K′ public
        module arr = NaturalTransformation arr

      FXcone : ∀ X → (K : Co.Cone F) → Co.Cone F[-, X ]
      FXcone X K = record
        { N    = N.₀ X
        ; apex = record
          { ψ       = λ j → ψ.η j X
          ; commute = λ f → commute f -- this application cannot be eta reduced
          }
        }
        where open FCone K

      ⊤ : Co.Cone F
      ⊤ = record
        { N    = record
          { F₀           = λ X → apex X
          ; F₁           = λ {A B} f → lim⇒lim.arr f
          ; identity     = λ {X} →
            terminal.!-unique X record
            { arr     = D.id
            ; commute = D.identityʳ ○ ⟺ (elimˡ (F₀.identity _))
            }
          ; homomorphism = λ {X Y Z} {f g} →
            terminal.!-unique₂ Z
              {nat-map-Cone (F[-,-].₁ (g C.∘ f)) (limit X)}
              {terminal.! Z}
              {record { commute = λ {j} →
              begin
                proj Z j ∘ lim⇒lim.arr g ∘ lim⇒lim.arr f
                  ≈⟨ pullˡ (lim⇒lim.commute g) ⟩
                (F₀.₁ j g ∘ proj Y j) ∘ lim⇒lim.arr f
                  ≈⟨ pullʳ (lim⇒lim.commute f) ⟩
                F₀.₁ j g ∘ F₀.₁ j f ∘ proj X j
                  ≈˘⟨ pushˡ (F₀.homomorphism j) ⟩
                F₀.₁ j (g C.∘ f) ∘ proj X j
                  ∎ }}
          ; F-resp-≈     = λ {A B} {f g} eq → terminal.!-unique B record
            { commute = lim⇒lim.commute g ○ ∘-resp-≈ˡ (F₀.F-resp-≈ _ (C.Equiv.sym eq)) }
          }
        ; apex = record
          { ψ       = λ j → ntHelper record
            { η       = λ X → proj X j
            ; commute = λ _ → LimFX.commute _
            }
          ; commute = λ f {X} → limit-commute X f
          }
        }
        where open D
              open D.HomReasoning
              open MR D

      K⇒⊤′ : ∀ X {K} → Co.Cones F [ K , ⊤ ] → Co.Cones F[-, X ] [ FXcone X K , LimFX.limit X ]
      K⇒⊤′ X {K} K⇒⊤ = record
        { arr     = arr.η X
        ; commute = comm
        }
        where open FCone⇒ K⇒⊤ renaming (commute to comm)

      complete : Limit F
      complete = record
        { terminal = record
          { ⊤        = ⊤
          ; !        = λ {K} →
            let module K = FCone K
            in record
            { arr     = ntHelper record
              { η       = λ X → rep X (FXcone X K)
              ; commute = λ {X Y} f →
                terminal.!-unique₂ Y
                  {nat-map-Cone (F[-,-].₁ f) (FXcone X K)}
                  {record { commute = λ {j} →
                  begin
                    proj Y j ∘ rep Y (FXcone Y K) ∘ K.N.₁ f ≈⟨ pullˡ (LimFX.commute Y) ⟩
                    K.ψ.η j Y ∘ K.N.F₁ f                    ≈⟨ K.ψ.commute j f ⟩
                    F₀.₁ j f ∘ K.ψ.η j X                    ∎ }}
                  {record { commute = λ {j} →
                  begin
                    proj Y j ∘ lim⇒lim.arr f ∘ rep X (FXcone X K) ≈⟨ pullˡ (lim⇒lim.commute f) ⟩
                    (F₀.₁ j f ∘ proj X j) ∘ rep X (FXcone X K)    ≈⟨ pullʳ (LimFX.commute X) ⟩
                    F₀.₁ j f ∘ K.ψ.η j X                          ∎ }}
              }
            ; commute = λ {_} {X} → LimFX.commute X
            }
          ; !-unique = λ K⇒⊤ {X} → terminal.!-unique X (K⇒⊤′ X K⇒⊤)
          }
        }
        where open D
              open D.HomReasoning
              open MR D

      ev : C.Obj → Functor D^C D
      ev = evalF C D

      module _ (L : Limit F) (X : C.Obj) where
        private
          module ev = Functor (ev X)
          open Mor D^C
          module DM = Mor D
          open Morₚ D
          open D.HomReasoning
          open MR D

        L′ : Limit (ev X ∘F F)
        L′ = Com (ev X ∘F F)

        Fiso : F[-, X ] ≃ ev X ∘F F
        Fiso = record
          { F⇒G = ntHelper record
            { η       = λ _ → D.id
            ; commute = λ _ → id-comm-sym ○ D.∘-resp-≈ˡ (introʳ (F₀.identity _))
            }
          ; F⇐G = ntHelper record
            { η       = λ _ → D.id
            ; commute = λ _ → D.∘-resp-≈ʳ (elimʳ (F₀.identity _)) ○ id-comm-sym
            }
          ; iso = λ _ → record
            { isoˡ = D.identity²
            ; isoʳ = D.identity²
            }
          }

        apex-iso : Limit.apex L ≅ Limit.apex complete
        apex-iso = up-to-iso F L complete

        apex-iso′ : Limit.apex (Com F[-, X ]) DM.≅ Limit.apex L′
        apex-iso′ = ≃⇒lim≅ Fiso (Com F[-, X ]) L′

        project-iso : Functor.F₀ (Limit.apex L) X DM.≅ Limit.apex L′
        project-iso = record
          { from = ai.from D.∘ from.η X
          ; to   = to.η X D.∘ ai.to
          ; iso  = Iso-∘ (record { isoˡ = isoˡ ; isoʳ = isoʳ }) ai.iso
          }
          where open _≅_ apex-iso
                module from = NaturalTransformation from
                module to   = NaturalTransformation to
                module ai   = DM._≅_ apex-iso′

  Functors-Complete : Complete o″ ℓ″ e″ D^C
  Functors-Complete F = complete F

  evalF-Continuous : ∀ X → Continuous o″ ℓ″ e″ (evalF C D X)
  evalF-Continuous X {J} {F} L = Com (evalF C D X ∘F F) , project-iso F L X

max_stars_repo_name: laMudri/agda-categories

max_issues_repo_name: laMudri/agda-categories

max_forks_repo_name: laMudri/agda-categories


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Wedge.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.HITs.Pushout.Base
open import Cubical.Data.Unit

_⋁_ : ∀ {ℓ ℓ'} → Pointed ℓ → Pointed ℓ' → Type (ℓ-max ℓ ℓ')
_⋁_ (A , ptA) (B , ptB) = Pushout {A = Unit} {B = A} {C = B} (λ _ → ptA) (λ _ → ptB)

-- pointed versions

_⋁∙ₗ_ : ∀ {ℓ ℓ'} → Pointed ℓ → Pointed ℓ' → Pointed (ℓ-max ℓ ℓ')
A ⋁∙ₗ B = (A ⋁ B) , (inl (snd A))

_⋁∙ᵣ_ : ∀ {ℓ ℓ'} → Pointed ℓ → Pointed ℓ' → Pointed (ℓ-max ℓ ℓ')
A ⋁∙ᵣ B = (A ⋁ B) , (inr (snd B))

-- Wedge sum of Units is contractible
isContr-Unit⋁Unit : isContr ((Unit , tt) ⋁ (Unit , tt))
fst isContr-Unit⋁Unit = inl tt
snd isContr-Unit⋁Unit (inl tt) = refl
snd isContr-Unit⋁Unit (inr tt) = push tt
snd isContr-Unit⋁Unit (push tt i) j = push tt (i ∧ j)

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:
open import Agda.Builtin.Nat

data Tm : Nat → Set where
  UP : ∀ {n} → Tm n → Tm n

!_ : ∀ {n} → Tm n → Tm (suc n)
! UP t = UP (! t)

data Ty : Nat → Set where
  ⊥ : ∀ {n} → Ty n
  _∶_ : ∀ {n} → Tm n → Ty n → Ty (suc n)

data Cx : Set where
  ∅ : Cx
  _,_ : ∀ {n} → Cx → Ty n → Cx

data _⊇_ : Cx → Cx → Set where
  base : ∅ ⊇ ∅
  weak : ∀ {Γ Γ′ n} {A : Ty n} → Γ′ ⊇ Γ → (Γ′ , A) ⊇ Γ
  lift : ∀ {Γ Γ′ n} {A : Ty n} → Γ′ ⊇ Γ → (Γ′ , A) ⊇ (Γ , A)

data True (Γ : Cx) : ∀ {n} → Ty n → Set where
  up : ∀ {n} {t : Tm n} {A : Ty n} → True Γ (t ∶ A) → True Γ ((! t) ∶ (t ∶ A))

ren-true--pass : ∀ {n Γ Γ′} {A : Ty n} → Γ′ ⊇ Γ → True Γ A → True Γ′ A
ren-true--pass η (up j) = up (ren-true--pass η j)

ren-true--fail : ∀ {Γ Γ′ A} → Γ′ ⊇ Γ → True Γ A → True Γ′ A
ren-true--fail η (up j) = up (ren-true--fail η j)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- {-# OPTIONS --allow-unsolved-metas #-}

module Issue2369.OpenIP where

test : Set
test = {!!}  -- unsolved interaction point

-- postulate A : {!!}


text:
module Generic.Lib.Equality.Coerce where

open import Generic.Lib.Intro
open import Generic.Lib.Equality.Propositional
open import Generic.Lib.Decidable
open import Generic.Lib.Data.Product

Coerce′ : ∀ {α β} -> α ≡ β -> Set α -> Set β
Coerce′ refl = id

coerce′ : ∀ {α β} {A : Set α} -> (q : α ≡ β) -> A -> Coerce′ q A
coerce′ refl = id

uncoerce′ : ∀ {α β} {A : Set α} -> (q : α ≡ β) -> Coerce′ q A -> A
uncoerce′ refl = id

inspectUncoerce′ : ∀ {α β} {A : Set α}
                 -> (q : α ≡ β) -> (p : Coerce′ q A) -> ∃ λ x -> p ≡ coerce′ q x
inspectUncoerce′ refl x = x , refl

split : ∀ {α β γ δ} {A : Set α} {B : A -> Set β} {C : Set γ}
      -> (q : α ⊔ β ≡ δ) -> Coerce′ q (Σ A B) -> (∀ x -> B x -> C) -> C
split q p g = uncurry g (uncoerce′ q p)

decCoerce′ : ∀ {α β} {A : Set α} -> (q : α ≡ β) -> IsSet A -> IsSet (Coerce′ q A)
decCoerce′ refl = id

data Coerce {β} : ∀ {α} -> α ≡ β -> Set α -> Set β where
  coerce : ∀ {A} -> A -> Coerce refl A

qcoerce : ∀ {α β} {A : Set α} {q : α ≡ β} -> A -> Coerce q A
qcoerce {q = refl} = coerce

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
module Function.Equals where

import      Lvl
open import Functional
import      Function.Names as Names
open import Logic
open import Logic.Propositional
open import Structure.Setoid
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Type

module Dependent {ℓ₁ ℓ₂ ℓₑ₂} {A : Type{ℓ₁}} {B : A → Type{ℓ₂}} ⦃ equiv-B : ∀{a} → Equiv{ℓₑ₂}(B(a)) ⦄ where
  infixl 15 _⊜_

  -- Function equivalence. When the types and all their values are shared/equivalent.
  record _⊜_ (f : (a : A) → B(a)) (g : (a : A) → B(a)) : Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓₑ₂} where
    constructor intro
    field
      proof : (f Names.⊜ g)

  instance
    [⊜]-reflexivity : Reflexivity(_⊜_)
    Reflexivity.proof([⊜]-reflexivity) = intro(reflexivity(_≡_) ⦃ Equiv.reflexivity(equiv-B) ⦄)

  instance
    [⊜]-symmetry : Symmetry(_⊜_)
    Symmetry.proof([⊜]-symmetry) (intro fg) = intro(symmetry(_≡_) ⦃ Equiv.symmetry(equiv-B) ⦄ fg)

  instance
    [⊜]-transitivity : Transitivity(_⊜_)
    Transitivity.proof([⊜]-transitivity) (intro fg) (intro gh) = intro(transitivity(_≡_) ⦃ Equiv.transitivity(equiv-B) ⦄ fg gh)

  instance
    [⊜]-equivalence : Equivalence(_⊜_)
    [⊜]-equivalence = record{}

  instance
    [⊜]-equiv : Equiv((a : A) → B(a))
    [⊜]-equiv = intro(_⊜_) ⦃ [⊜]-equivalence ⦄

  instance
    [⊜]-sub : (_≡_) ⊆₂ (_⊜_)
    _⊆₂_.proof [⊜]-sub (intro proof) = intro proof

module _ {ℓ₁ ℓ₂ ℓₑ₂} {A : Type{ℓ₁}} {B : Type{ℓ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ where
  private module D = Dependent {A = A} {B = const B} ⦃ equiv-B ⦄
  open D using (module _⊜_ ; intro) public
  _⊜_              = D._⊜_
  [⊜]-reflexivity  = D.[⊜]-reflexivity
  [⊜]-symmetry     = D.[⊜]-symmetry
  [⊜]-transitivity = D.[⊜]-transitivity
  [⊜]-equivalence  = D.[⊜]-equivalence
  [⊜]-equiv        = D.[⊜]-equiv
  [⊜]-sub          = D.[⊜]-sub


text:
------------------------------------------------------------------------------
-- Proving mirror (mirror t) = t using a list of trees
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOT.FOTC.Program.Mirror.MirrorListSL where

open import Algebra
open import Function
open import Data.List hiding ( reverse )
open import Data.List.Properties
open import Data.Product hiding ( map )

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

module LM {A : Set} = Monoid (++-monoid A)

------------------------------------------------------------------------------
-- Auxiliary functions

reverse : {A : Set} → List A → List A
reverse []       = []
reverse (x ∷ xs) = reverse xs ++ x ∷ []

++-rightIdentity : {A : Set}(xs : List A) → xs ++ [] ≡ xs
++-rightIdentity = proj₂ LM.identity

reverse-++ : {A : Set}(xs ys : List A) →
             reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++ [] ys       = sym (++-rightIdentity (reverse ys))
reverse-++ (x ∷ xs) [] = cong (λ x' → reverse x' ++ x ∷ [])
                              (++-rightIdentity xs)
reverse-++ (x ∷ xs) (y ∷ ys) =
  begin
    reverse (xs ++ y ∷ ys) ++ x ∷ []
      ≡⟨ cong (λ x' → x' ++ x ∷ []) (reverse-++ xs (y ∷ ys)) ⟩
    (reverse (y ∷ ys) ++ reverse xs) ++ x ∷ []
      ≡⟨ LM.assoc (reverse (y ∷ ys)) (reverse xs) (x ∷ []) ⟩
    reverse (y ∷ ys) ++ reverse (x ∷ xs)
  ∎

------------------------------------------------------------------------------
-- The rose tree type.
data Tree (A : Set) : Set where
  tree : A → List (Tree A) → Tree A

------------------------------------------------------------------------------
-- The mirror function.

{-# TERMINATING #-}
mirror : {A : Set} → Tree A → Tree A
mirror (tree a ts) = tree a (reverse (map mirror ts))

-- The proof of the property.
mirror-involutive : {A : Set} → (t : Tree A) → mirror (mirror t) ≡ t
helper            : {A : Set} → (ts : List (Tree A)) →
                    reverse (map mirror (reverse (map mirror ts))) ≡ ts

mirror-involutive (tree a []) = refl
mirror-involutive (tree a (t ∷ ts)) =
  begin
    tree a (reverse (map mirror (reverse (map mirror ts) ++ mirror t ∷ [])))
      ≡⟨ cong (tree a) (helper (t ∷ ts)) ⟩
    tree a (t ∷ ts)
  ∎

helper [] = refl
helper (t ∷ ts) =
  begin
    reverse (map mirror (reverse (map mirror ts) ++ mirror t ∷ []))
     ≡⟨ cong reverse
             (map-++-commute mirror (reverse (map mirror ts)) (mirror t ∷ []))
     ⟩
    reverse (map mirror (reverse (map mirror ts)) ++
            (map mirror (mirror t ∷ [])))
      ≡⟨ subst (λ x → (reverse (map mirror (reverse (map mirror ts)) ++
                                    (map mirror (mirror t ∷ [])))) ≡ x)
               (reverse-++ (map mirror (reverse (map mirror ts)))
                           (map mirror (mirror t ∷ [])))
               refl
      ⟩
    reverse (map mirror (mirror t ∷ [])) ++
    reverse (map mirror (reverse (map mirror ts)))
      ≡⟨ refl ⟩
    mirror (mirror t) ∷ reverse (map mirror (reverse (map mirror ts)))
      ≡⟨ cong (flip _∷_ (reverse (map mirror (reverse (map mirror ts)))))
              (mirror-involutive t)
      ⟩
    t ∷ reverse (map mirror (reverse (map mirror ts)))
      ≡⟨ cong (_∷_ t) (helper ts) ⟩
    t ∷ ts
  ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module NativeIO where

open import Unit public
open import Data.List
open import Data.Nat
open import Data.String.Base using (String) public

{-# FOREIGN GHC import qualified Data.Text #-}
{-# FOREIGN GHC import qualified System.Environment #-}

postulate
  NativeIO     : Set → Set
  nativeReturn : {A : Set} → A → NativeIO A
  _native>>=_  : {A B : Set} → NativeIO A → (A → NativeIO B) → NativeIO B

{-# BUILTIN IO NativeIO #-}
{-# COMPILE GHC NativeIO = type IO #-}
{-# COMPILE GHC nativeReturn = (\_ -> return :: a -> IO a) #-}
{-# COMPILE GHC _native>>=_ = (\_ _ -> (>>=) :: IO a -> (a -> IO b) -> IO b) #-}

postulate
  nativeGetLine   : NativeIO String
  nativePutStrLn  : String → NativeIO Unit

{-# COMPILE GHC nativePutStrLn = (\ s -> putStrLn (Data.Text.unpack s)) #-}
{-# COMPILE GHC nativeGetLine = (fmap Data.Text.pack getLine) #-}

postulate
  getArgs : NativeIO (List String)
  primShowNat : ℕ → String

{-# COMPILE GHC primShowNat = Data.Text.pack . show #-}

{-# COMPILE GHC getArgs =     fmap (map Data.Text.pack) System.Environment.getArgs #-}

--
-- Debug function
--
{-# FOREIGN GHC import qualified Debug.Trace as Trace #-}

{-# FOREIGN GHC

debug = flip Trace.trace

debug' :: c -> Data.Text.Text -> c
debug' c txt = debug c (Data.Text.unpack txt)

#-}

postulate debug : {A : Set} →  A → String → A
--debug {A} a s = a
{-# COMPILE GHC debug = (\x -> debug') #-}

postulate debug₁ : {A : Set₁} →  A → String → A
-- debug₁ {A} a s = a
{-# COMPILE GHC debug₁ = (\x -> debug') #-}

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
-- {-# OPTIONS -v tc.lhs.top:15 #-}
-- {-# OPTIONS -v term:20 #-}

-- Andreas, 2014-11-08, following a complaint by Francesco Mazzoli

open import Common.Prelude

data Subst : (d : Nat) → Set where
  c₁ : ∀ {d}   → Subst d             → Subst d
  c₂ : ∀ d₁ d₂ → Subst d₁ → Subst d₂ → Subst (suc d₁ + d₂)

postulate
  comp : ∀ {d₁ d₂} → Subst d₁ → Subst d₂ → Subst (d₁ + d₂)

lookup : ∀ d → Nat → Subst d → Set₁
lookup d             zero    (c₁ ρ)        = Set
lookup d             (suc v) (c₁ ρ)        = lookup d v ρ
lookup .(suc d₁ + d₂) v       (c₂ d₁ d₂ ρ σ) = lookup (d₁ + d₂) v (comp ρ σ)

-- The dot pattern here is actually normalized, so it is
--
--   suc (d₁ + d₂)
--
-- the recursive call it with (d₁ + d₂).
-- In such simple cases, Agda can now recognize that the pattern is
-- constructor applied to call argument, which is valid descent.

-- This should termination check now.

-- Note however, that Agda only looks for syntactic equality,
-- since it is not allowed to normalize terms on the rhs (yet).

hidden : ∀{d} → Nat → Subst d → Set₁
hidden zero    (c₁ ρ)        = Set
hidden (suc v) (c₁ ρ)        = hidden v ρ
hidden v       (c₂ d₁ d₂ ρ σ) = hidden v (comp ρ σ)

-- This should also termination check, and looks pretty magical... ;-)


text:
-- Evidence producing divmod.
module Numeric.Nat.DivMod where

open import Prelude
open import Control.WellFounded
open import Tactic.Nat
open import Tactic.Nat.Reflect
open import Tactic.Nat.Exp
open import Numeric.Nat.Properties

private
  lemModAux′ : ∀ k m b j → modAux k m (suc j + b) j ≡ modAux 0 m b m
  lemModAux′ k m b  zero   = refl
  lemModAux′ k m b (suc j) = lemModAux′ (suc k) m b j

  lemModAux : ∀ k m b j → modAux k m (suc b + j) j ≡ modAux 0 m b m
  lemModAux k m b j = (λ z → modAux k m (suc z) j) $≡ auto ⟨≡⟩ lemModAux′ k m b j

  lemDivAux′ : ∀ k m b j → divAux k m (suc j + b) j ≡ divAux (suc k) m b m
  lemDivAux′ k m b  zero   = refl
  lemDivAux′ k m b (suc j) = lemDivAux′ k m b j

  lemDivAux : ∀ k m b j → divAux k m (suc b + j) j ≡ divAux (suc k) m b m
  lemDivAux k m b j = (λ z → divAux k m (suc z) j) $≡ auto ⟨≡⟩ lemDivAux′ k m b j

  modLessAux : ∀ k m n j → k + j < suc m → modAux k m n j < suc m
  modLessAux k m  zero    j      lt = by lt
  modLessAux k m (suc n)  zero   _  = modLessAux 0 m n m auto
  modLessAux k m (suc n) (suc j) lt = modLessAux (suc k) m n j (by lt)

  modLess : ∀ a b → a mod suc b < suc b
  modLess a b = fast-diff $ modLessAux 0 b a b auto

  divAuxGt : ∀ k a b j → a ≤ j → divAux k b a j ≡ k
  divAuxGt k  zero   b  j      lt = refl
  divAuxGt k (suc a) b  zero   lt = refute lt
  divAuxGt k (suc a) b (suc j) lt = divAuxGt k a b j (by lt)

  modAuxGt : ∀ k a b j → a ≤ j → modAux k b a j ≡ k + a
  modAuxGt k  zero   b  j      lt = auto
  modAuxGt k (suc a) b  zero   lt = refute lt
  modAuxGt k (suc a) b (suc j) lt = by (modAuxGt (suc k) a b j (by lt))

  qr-mul : (b q r : Nat) → Nat
  qr-mul b q r = q * suc b + r

  divmodAux : ∀ k a b → Acc _<_ a → qr-mul b (divAux k b a b) (modAux 0 b a b) ≡ qr-mul b k a
  divmodAux k a  b wf    with compare b a
  divmodAux k a  b wf       | greater lt =
    let leq : a ≤ b
        leq = by lt in
    qr-mul b $≡ divAuxGt k a b b leq
             *≡ modAuxGt 0 a b b leq
  divmodAux k a .a wf       | equal refl =
    qr-mul a $≡ divAuxGt k a a a (diff! 0)
             *≡ modAuxGt 0 a a a (diff! 0)
  divmodAux k ._ b (acc wf) | less (diff! j) =
    qr-mul b $≡ lemDivAux k b j b *≡ lemModAux 0 b j b ⟨≡⟩
    by (divmodAux (suc k) j b (wf j auto))

  divmod-spec : ∀ a b′ → let b = suc b′ in a div b * b + a mod b ≡ a
  divmod-spec a b = eraseEquality (divmodAux 0 a b (wfNat a))

--- Public definitions ---

data DivMod (a b : Nat) : Set where
  qr : ∀ q r → r < b → q * b + r ≡ a → DivMod a b

quot : ∀ {a b} → DivMod a b → Nat
quot (qr q _ _ _) = q

rem : ∀ {a b} → DivMod a b → Nat
rem (qr _ r _ _) = r

rem-less : ∀ {a b} (d : DivMod a b) → rem d < b
rem-less (qr _ _ lt _) = lt

quot-rem-sound : ∀ {a b} (d : DivMod a b) → quot d * b + rem d ≡ a
quot-rem-sound (qr _ _ _ eq) = eq

syntax divMod b a = a divmod b
divMod : ∀ b {{_ : NonZero b}} a → DivMod a b
divMod zero {{}} a
divMod (suc b) a = qr (a div suc b) (a mod suc b) (modLess a b) (divmod-spec a b)

{-# INLINE divMod #-}

--- Properties ---

mod-less : ∀ b {{_ : NonZero b}} a → a mod b < b
mod-less zero {{}} _
mod-less (suc b) a = rem-less (a divmod suc b)

divmod-sound : ∀ b {{_ : NonZero b}} a → (a div b) * b + a mod b ≡ a
divmod-sound zero {{}} _
divmod-sound (suc b) a = quot-rem-sound (a divmod suc b)

private
  divmod-unique′ : (b q₁ q₂ r₁ r₂ : Nat) → r₁ < b → r₂ < b → q₁ * b + r₁ ≡ q₂ * b + r₂ → q₁ ≡ q₂ × r₁ ≡ r₂
  divmod-unique′ b  zero     zero    r₁ r₂ lt₁ lt₂ eq   = refl , eq
  divmod-unique′ b  zero    (suc q₂) ._ r₂ lt₁ lt₂ refl = refute lt₁
  divmod-unique′ b (suc q₁)  zero    r₁ ._ lt₁ lt₂ refl = refute lt₂
  divmod-unique′ b (suc q₁) (suc q₂) r₁ r₂ lt₁ lt₂ eq   =
    first (cong suc) $ divmod-unique′ b q₁ q₂ r₁ r₂ lt₁ lt₂ (by eq)

divmod-unique : ∀ {a b} (d₁ d₂ : DivMod a b) → quot d₁ ≡ quot d₂ × rem d₁ ≡ rem d₂
divmod-unique (qr q₁ r₁ lt₁ eq₁) (qr q₂ r₂ lt₂ eq₂) =
  case divmod-unique′ _ q₁ q₂ r₁ r₂ lt₁ lt₂ (eq₁ ⟨≡⟩ʳ eq₂) of
  λ p → eraseEquality (fst p) , eraseEquality (snd p)

quot-unique : ∀ {a b} (d₁ d₂ : DivMod a b) → quot d₁ ≡ quot d₂
quot-unique d₁ d₂ = fst (divmod-unique d₁ d₂)

rem-unique : ∀ {a b} (d₁ d₂ : DivMod a b) → rem d₁ ≡ rem d₂
rem-unique d₁ d₂ = snd (divmod-unique d₁ d₂)

instance
  ShowDivMod : ∀ {a b} → Show (DivMod a b)
  showsPrec {{ShowDivMod {a} {b}}} p (qr q r _ _) =
      showParen (p >? 0) $ shows a ∘ showString " == "
                         ∘ shows q ∘ showString " * " ∘ shows b ∘ showString " + " ∘ shows r

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
-- Positivity for functions in instantiated parameterised modules.
module Issue421 where

module Foo (_ : Set₁) where
  Id : Set → Set
  Id n = n

module FooApp = Foo Set

data ⊤ : Set where
  tt : ⊤

⟦_⟧₁ : ⊤ → Set → Set
⟦ tt ⟧₁ x = FooApp.Id x
-- works: ⟦ tt ⟧ x = Foo.Id Set x

data μ₁ x : Set where
  fix : ⟦ x ⟧₁ (μ₁ x) -> μ₁ x

-- Instantiating the module in another parameterised module:

module Matrices (J : Set) where

  Id : (J → Set) → J → Set
  Id m i = m i

data Poly : Set where
  id : (D : Poly) -> Poly

module Dim (I : Set) where
  module M = Matrices I

  ⟦_⟧₂ : Poly → (I → Set) → (I → Set)
  ⟦ id D ⟧₂ x i = M.Id x i

  data μ₂ (p : Poly) (i : I) : Set where
    fix : ⟦ p ⟧₂ (μ₂ p) i -> μ₂ p i

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module ObsEq2 where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

data Fin : Nat -> Set where
  fz : {n : Nat} -> Fin (suc n)
  fs : {n : Nat} -> Fin n -> Fin (suc n)

infixr 40 _::_ _,_

data List (X : Set) : Set where
  ε : List X
  _::_ : X -> List X -> List X

record One : Set where

Π : (S : Set)(T : S -> Set) -> Set
Π S T = (x : S) -> T x

data Σ (S : Set)(T : S -> Set) : Set where
  _,_ : (s : S) -> T s -> Σ S T

split : {S : Set}{T : S -> Set}{P : Σ S T -> Set}
        (p : (s : S)(t : T s) -> P (s , t)) ->
        (x : Σ S T) -> P x
split p (s , t) = p s t

fst : {S : Set}{T : S -> Set}(x : Σ S T) -> S
fst = split \s t -> s

snd : {S : Set}{T : S -> Set}(x : Σ S T) -> T (fst x)
snd = split \s t -> t

mutual

  data ∗ : Set where
    /Π/ : (S : ∗)(T : [ S ] -> ∗) -> ∗
    /Σ/ : (S : ∗)(T : [ S ] -> ∗) -> ∗
    /Fin/ : Nat -> ∗
    /D/ : (I : ∗)(A : [ I ] -> ∗)(R : (i : [ I ]) -> [ A i ] -> List [ I ])
        -> [ I ] -> ∗

  [_] : ∗ -> Set
  [ /Π/ S T ]    = Π [ S ] \s -> [ T s ]
  [ /Σ/ S T ]    = Σ [ S ] \s -> [ T s ]
  [ /Fin/ n ]    = Fin n
  [ /D/ I A R i ]  = Σ [ A i ] \a -> [ Kids I (/D/ I A R) (R i a) ]

  Kids : (I : ∗)(P : [ I ] -> ∗) -> List [ I ] -> ∗
  Kids I P ε = /Fin/ (suc zero)
  Kids I P (i :: is) = /Σ/ (P i) \_ -> Kids I P is

/0/ : ∗
/0/ = /Fin/ zero

/1/ : ∗
/1/ = /Fin/ (suc zero)

/2/ : ∗
/2/ = /Fin/ (suc (suc zero))

Branches : {n : Nat}(P : Fin n -> Set) -> Set
Branches {zero} P = One
Branches {suc n} P = Σ (P fz) \_ -> Branches {n} \x -> P (fs x)

case : {n : Nat}{P : Fin n -> Set} -> Branches P -> (x : Fin n) -> P x
case pps  fz     = fst pps
case pps (fs x)  = case (snd pps) x

infixr 40 _⟶_

infixr 60 _×_

_⟶_ : ∗ -> ∗ -> ∗
S ⟶ T = /Π/ S \_ -> T

_×_ : ∗ -> ∗ -> ∗
S × T = /Σ/ S \_ -> T

NatR : [ /1/ ] -> [ /2/ ] -> List [ /1/ ]
NatR _ fz       = ε
NatR _ (fs fz)  = fz :: ε
NatR _ (fs (fs ()))

/Nat/ : ∗
/Nat/ = /D/ /1/ (\_ -> /2/) NatR fz

/zero/ : [ /Nat/ ]
/zero/ = fz , fz

/suc/ : [ /Nat/ ⟶ /Nat/ ]
/suc/ n = fs fz , n , fz

Hyps : (I : ∗)(K : [ I ] -> ∗)
       (P : (i : [ I ]) -> [ K i ] -> ∗)
       (is : List [ I ]) -> [ Kids I K is ] -> ∗
Hyps I K P  ε          _       = /1/
Hyps I K P  (i :: is) (k , ks) = /Σ/ (P i k) \_ -> Hyps I K P is ks

recs : (I : ∗)(K : [ I ] -> ∗)
       (P : (i : [ I ]) -> [ K i ] -> ∗)
       (e : (i : [ I ])(k : [ K i ]) -> [ P i k ])
       (is : List [ I ])(ks : [ Kids I K is ]) -> [ Hyps I K P is ks ]
recs I K P e  ε          _ = fz
recs I K P e  (i :: is) (k , ks) = ( e i k , recs I K P e is ks )

elim : (I : ∗)(A : [ I ] -> ∗)(R : (i : [ I ]) -> [ A i ] -> List [ I ])
       (P : (i : [ I ]) -> [ /D/ I A R i ] -> ∗) ->
       [( (/Π/ I \i -> /Π/ (A i) \a ->
          /Π/ (Kids I (/D/ I A R) (R i a)) \ks ->
          Hyps I (/D/ I A R) P (R i a) ks ⟶ P i (a , ks)) ⟶
         /Π/ I \i -> /Π/ (/D/ I A R i) \x -> P i x )]
elim I A R P p i (a , ks) =
  p i a ks (recs I (/D/ I A R) P (elim I A R P p) (R i a) ks)

natElim : (P : [ /Nat/ ] -> ∗) ->
          [( P /zero/ ⟶
             (/Π/ /Nat/ \n -> P n ⟶ P (/suc/ n)) ⟶
             /Π/ /Nat/ P )]
natElim P pz ps = elim /1/ (\_ -> /2/) NatR (case (P , _))
  (case ( case (case ((\_ -> pz ) , _ )
  , (split \n -> case (split (\h _ -> ps n h)   , _ ))   , _ )  , _ ))
  fz

plus : [ /Nat/ ⟶ /Nat/ ⟶ /Nat/ ]
plus x y = natElim (\_ -> /Nat/) y (\_ -> /suc/) x

{-
elim /1/ (\_ -> /2/) NatR (\_ _ -> /Nat/)
   (\_ -> case
    ((\_ _ -> y )
    , split (\_ _ -> split (\n _ -> /suc/ n )  )  , _ ) )
   fz x
-}

mutual
  _⇔_ : ∗ -> ∗ -> ∗
  /Π/ S0 T0 ⇔ /Π/ S1 T1 =
    (S1 ⇔ S0) ×
    /Π/ S1 \s1 -> /Π/ S0 \s0 -> (S1 > s1 ≅ S0 > s0) ⟶ (T0 s0 ⇔ T1 s1)
  /Σ/ S0 T0 ⇔ /Σ/ S1 T1 =
    (S0 ⇔ S1) ×
    /Π/ S0 \s0 -> /Π/ S1 \s1 -> (S0 > s0 ≅ S1 > s1) ⟶ (T0 s0 ⇔ T1 s1)
  /Fin/ _ ⇔ /Π/ _ _ = /0/
  /Fin/ _ ⇔ /Σ/ _ _ = /0/
  /Fin/ _ ⇔ /D/ _ _ _ _ = /0/
  /Π/ _ _ ⇔ /Fin/ _ = /0/
  /Σ/ _ _ ⇔ /Fin/ _ = /0/
  /D/ _ _ _ _ ⇔ /Fin/ _ = /0/
  /Fin/ zero ⇔ /Fin/ zero = /1/
  /Fin/ (suc m) ⇔ /Fin/ (suc n) = /Fin/ m ⇔ /Fin/ n
  /D/ I0 A0 R0 i0 ⇔ /D/ I1 A1 R1 i1 =
    (I0 ⇔ I1) ×
    (/Π/ I0 \i0 -> /Π/ I1 \i1 -> (I0 > i0 ≅ I1 > i1) ⟶ (A0 i0 ⇔ A1 i1)) ×
    (/Π/ I0 \i0 -> /Π/ I1 \i1 -> (I0 > i0 ≅ I1 > i1) ⟶
     /Π/ (A0 i0) \a0 -> /Π/ (A1 i1) \a1 -> (A0 i0 > a0 ≅ A1 i1 > a1) ⟶
     Eqs I0 (R0 i0 a0) I1 (R1 i1 a1)) ×
    (I0 > i0 ≅ I1 > i1)
  _ ⇔ _ = /0/

  Eqs : (I0 : ∗) -> List [ I0 ] -> (I1 : ∗) -> List [ I1 ] -> ∗
  Eqs _ ε _ ε = /1/
  Eqs I0 (i0 :: is0) I1 (i1 :: is1) = (I0 > i0 ≅ I1 > i1) × Eqs I0 is0 I1 is1
  Eqs _ _ _ _ = /0/

  _>_≅_>_ : (S : ∗) -> [ S ] -> (T : ∗) -> [ T ] -> ∗
  /Π/ S0 T0 > f0 ≅ /Π/ S1 T1 > f1 =
    /Π/ S0 \s0 -> /Π/ S1 \s1 -> (S0 > s0 ≅ S1 > s1) ⟶
       (T0 s0 > f0 s0 ≅ T1 s1 > f1 s1)
  /Σ/ S0 T0 > p0 ≅ /Σ/ S1 T1 > p1 =
    let s0 : [ S0 ] ; s0 = fst p0
        s1 : [ S1 ] ; s1 = fst p1
    in  (S0 > s0 ≅ S1 > s1) × (T0 s0 > snd p0 ≅ T1 s1 > snd p1)
  /Fin/ (suc n0) > fz    ≅ /Fin/ (suc n1) > fz    = /1/
  /Fin/ (suc n0) > fs x0 ≅ /Fin/ (suc n1) > fs x1 =
    /Fin/ n0 > x0 ≅ /Fin/ n1 > x1
  /D/ I0 A0 R0 i0 > (a0 , ks0) ≅ /D/ I1 A1 R1 i1 > (a1 , ks1) =
    (A0 i0 > a0 ≅ A1 i1 > a1) ×
    (Kids I0 (/D/ I0 A0 R0) (R0 i0 a0) > ks0 ≅
     Kids I1 (/D/ I1 A1 R1) (R1 i1 a1) > ks1)

  _ > _ ≅ _ > _ = /0/

Resp : (S : ∗)(P : [ S ] -> ∗)
       {s0 s1 : [ S ]} -> [ (S > s0 ≅ S > s1) ⟶ (P s0 ⇔ P s1) ]
Resp = {! !}

[_>_] : (S : ∗)(s : [ S ]) -> [ S > s ≅ S > s ]
[_>_] = {! !}

KidsResp : (I0 : ∗)(I1 : ∗) -> [ I0 ⇔ I1 ] ->
           (P0 : [ I0 ] -> ∗)(P1 : [ I1 ] -> ∗) ->
           [( /Π/ I0 \i0 -> /Π/ I1 \i1 -> (I0 > i0 ≅ I1 > i1) ⟶
              (P0 i0 ⇔ P1 i1) )] ->
           (is0 : List [ I0 ])(is1 : List [ I1 ]) ->
           [ Eqs I0 is0 I1 is1 ] ->
           [ Kids I0 P0 is0 ⇔ Kids I1 P1 is1 ]
KidsResp = {! !}

mutual

  _>_<_!_ : (S : ∗) -> [ S ] -> (T : ∗) -> [ S ⇔ T ] -> [ T ]
  /Π/ S0 T0 > f0 < /Π/ S1 T1 ! Q =
    let S1S0 : [ S1 ⇔ S0 ]
        S1S0 = fst Q
        T0T1 : [( /Π/ S1 \s1 -> /Π/ S0 \s0 -> (S1 > s1 ≅ S0 > s0) ⟶
                  (T0 s0 ⇔ T1 s1) )]
        T0T1 = snd Q
    in  \s1 ->
        let s0   : [ S0 ]
            s0   = S1 > s1 < S0 ! S1S0
            s1s0 : [( S1 > s1 ≅ S0 > s0 )]
            s1s0 = [| S1 > s1 < S0 ! S1S0 |]
        in  T0 s0 > f0 s0 < T1 s1 ! T0T1 s1 s0 s1s0

  /Σ/ S0 T0 > p0 < /Σ/ S1 T1 ! Q =
    let S0S1 : [ S0 ⇔ S1 ]
        S0S1 = fst Q
        T0T1 : [( /Π/ S0 \s0 -> /Π/ S1 \s1 -> (S0 > s0 ≅ S1 > s1) ⟶
                      (T0 s0 ⇔ T1 s1) )]
        T0T1 = snd Q
        s0   : [ S0 ]
        s0   = fst p0
        s1   : [ S1 ]
        s1   = S0 > s0 < S1 ! S0S1
        s0s1 : [ S0 > s0 ≅ S1 > s1 ]
        s0s1 = [| S0 > s0 < S1 ! S0S1 |]
        t0   : [ T0 s0 ]
        t0   = snd p0
        t1   : [ T1 s1 ]
        t1   = T0 s0 > t0 < T1 s1 ! T0T1 s0 s1 s0s1
    in  s1 , t1

  /Fin/ (suc n0) > fz   < /Fin/ (suc n1) ! Q = fz
  /Fin/ (suc n0) > fs x < /Fin/ (suc n1) ! Q = fs (/Fin/ n0 > x < /Fin/ n1 ! Q)

  /D/ I0 A0 R0 i0 > (a0 , ks0) < /D/ I1 A1 R1 i1 ! Q =
    let I01 : [ I0 ⇔ I1 ] ; I01 = fst Q
        A01 : [( /Π/ I0 \i0 -> /Π/ I1 \i1 ->
                 (I0 > i0 ≅ I1 > i1) ⟶ (A0 i0 ⇔ A1 i1) )]
        A01 = fst (snd Q)
        R01 : [( /Π/ I0 \i0 -> /Π/ I1 \i1 -> (I0 > i0 ≅ I1 > i1) ⟶
                 /Π/ (A0 i0) \a0 -> /Π/ (A1 i1) \a1 ->
                 (A0 i0 > a0 ≅ A1 i1 > a1) ⟶
                 Eqs I0 (R0 i0 a0) I1 (R1 i1 a1) )]
        R01 = fst (snd (snd Q))
        i01 : [ I0 > i0 ≅ I1 > i1 ] ; i01 = snd (snd (snd Q))
    in  (/Σ/ (A0 i0) \a0 -> Kids I0 (/D/ I0 A0 R0) (R0 i0 a0)) > (a0 , ks0) <
        (/Σ/ (A1 i1) \a1 -> Kids I1 (/D/ I1 A1 R1) (R1 i1 a1)) !
        A01 i0 i1 i01 ,
        \x0 x1 x01 ->
          KidsResp I0 I1 I01
          (/D/ I0 A0 R0) (/D/ I1 A1 R1) (\j0 j1 j01 -> I01 , A01 , R01 , j01 )
          (R0 i0 x0) (R1 i1 x1) (R01 i0 i1 i01 x0 x1 x01)

  /Π/ _ _ > _ < /Σ/ _ _ ! ()
  /Π/ _ _ > _ < /Fin/ _ ! ()
  /Π/ _ _ > _ < /D/ _ _ _ _ ! ()

  /Σ/ _ _ > _ < /Π/ _ _ ! ()
  /Σ/ _ _ > _ < /Fin/ _ ! ()
  /Σ/ _ _ > _ < /D/ _ _ _ _ ! ()

  /D/ _ _ _ _ > _ < /Π/ _ _ ! ()
  /D/ _ _ _ _ > _ < /Σ/ _ _ ! ()
  /D/ _ _ _ _ > _ < /Fin/ _ ! ()

  /Fin/ _ > _ < /Π/ _ _ ! ()
  /Fin/ _ > _ < /Σ/ _ _ ! ()
  /Fin/ zero > () < /Fin/ zero ! _
  /Fin/ zero > _ < /Fin/ (suc n) ! ()
  /Fin/ (suc n) > _ < /Fin/ zero ! ()
  /Fin/ _ > _ < /D/ _ _ _ _ ! ()

  [|_>_<_!_|] : (S : ∗)(s : [ S ])(T : ∗)(q : [ S ⇔ T ]) ->
    [ S > s ≅ T > (S > s < T ! q) ]
  [| S > s < T ! q |] = {! !}

ext : (S : ∗)(T : [ S ] -> ∗)(f g : [ /Π/ S T ]) ->
      [( /Π/ S \x -> T x > f x ≅ T x > g x )] ->
      [ /Π/ S T > f ≅ /Π/ S T > g ]
ext S T f g h s0 s1 s01 =
  (T s0 > f s0 ≅ T s0 > g s0) > h s0 < (T s0 > f s0 ≅ T s1 > g s1) !
  Resp S (\s1 -> T s0 > f s0 ≅ T s1 > g s1) s01

plusZeroLemma : [ (/Nat/ ⟶ /Nat/) > (\x -> plus x /zero/) ≅
                  (/Nat/ ⟶ /Nat/) > (\x -> plus /zero/ x) ]
plusZeroLemma = ext /Nat/ (\_ -> /Nat/)
   (\x -> plus x /zero/) (\x -> plus /zero/ x) (natElim (\x ->
     /Nat/ > plus x /zero/ ≅ /Nat/ > plus /zero/ x) (fz , fz)
    (\n h -> [ (/Nat/ ⟶ /Nat/) > /suc/ ] (plus n /zero/) n h  ))