text:
{-# OPTIONS --without-K --exact-split #-}

module 13-propositional-truncation where

import 12-function-extensionality
open 12-function-extensionality public

-- Section 13 Propositional truncations, the image of a map, and the replacement axiom

--------------------------------------------------------------------------------

-- Section 13.1 Propositional truncations

-- Definition 13.1.1

type-hom-Prop :
  { l1 l2 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) → UU (l1 ⊔ l2)
type-hom-Prop P Q = type-Prop P → type-Prop Q

hom-Prop :
  { l1 l2 : Level} → UU-Prop l1 → UU-Prop l2 → UU-Prop (l1 ⊔ l2)
hom-Prop P Q =
  pair
    ( type-hom-Prop P Q)
    ( is-prop-function-type (is-prop-type-Prop Q))

is-prop-type-hom-Prop :
  { l1 l2 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) → is-prop (type-hom-Prop P Q)
is-prop-type-hom-Prop P Q =
  is-prop-function-type (is-prop-type-Prop Q)

equiv-Prop :
  { l1 l2 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) → UU (l1 ⊔ l2)
equiv-Prop P Q = (type-Prop P) ≃ (type-Prop Q)

precomp-Prop :
  { l1 l2 l3 : Level} {A : UU l1} (P : UU-Prop l2) →
  (A → type-Prop P) → (Q : UU-Prop l3) →
  (type-hom-Prop P Q) → (A → type-Prop Q)
precomp-Prop P f Q g = g ∘ f

is-propositional-truncation :
  ( l : Level) {l1 l2 : Level} {A : UU l1} (P : UU-Prop l2) →
  ( A → type-Prop P) → UU (lsuc l ⊔ l1 ⊔ l2)
is-propositional-truncation l P f =
  (Q : UU-Prop l) → is-equiv (precomp-Prop P f Q)

universal-property-propositional-truncation :
  ( l : Level) {l1 l2 : Level} {A : UU l1}
  (P : UU-Prop l2) (f : A → type-Prop P) → UU (lsuc l ⊔ l1 ⊔ l2)
universal-property-propositional-truncation l {A = A} P f =
  (Q : UU-Prop l) (g : A → type-Prop Q) →
  is-contr (Σ (type-hom-Prop P Q) (λ h → (h ∘ f) ~  g))

-- Some unnumbered remarks after Definition 13.1.3

universal-property-is-propositional-truncation :
  (l : Level) {l1 l2 : Level} {A : UU l1}
  (P : UU-Prop l2) (f : A → type-Prop P) →
  is-propositional-truncation l P f →
  universal-property-propositional-truncation l P f
universal-property-is-propositional-truncation l P f is-ptr-f Q g =
  is-contr-equiv'
    ( Σ (type-hom-Prop P Q) (λ h → Id (h ∘ f) g))
    ( equiv-tot (λ h → equiv-funext))
    ( is-contr-map-is-equiv (is-ptr-f Q) g)

map-is-propositional-truncation :
  {l1 l2 l3 : Level} {A : UU l1} (P : UU-Prop l2) (f : A → type-Prop P) →
  ({l : Level} → is-propositional-truncation l P f) →
  (Q : UU-Prop l3) (g : A → type-Prop Q) → type-hom-Prop P Q
map-is-propositional-truncation P f is-ptr-f Q g =
  pr1
    ( center
      ( universal-property-is-propositional-truncation _ P f is-ptr-f Q g))

htpy-is-propositional-truncation :
  {l1 l2 l3 : Level} {A : UU l1} (P : UU-Prop l2) (f : A → type-Prop P) →
  (is-ptr-f : {l : Level} → is-propositional-truncation l P f) →
  (Q : UU-Prop l3) (g : A → type-Prop Q) →
  ((map-is-propositional-truncation P f is-ptr-f Q g) ∘ f) ~ g
htpy-is-propositional-truncation P f is-ptr-f Q g =
  pr2
    ( center
      ( universal-property-is-propositional-truncation _ P f is-ptr-f Q g))

is-propositional-truncation-universal-property :
  (l : Level) {l1 l2 : Level} {A : UU l1}
  (P : UU-Prop l2) (f : A → type-Prop P) →
  universal-property-propositional-truncation l P f →
  is-propositional-truncation l P f
is-propositional-truncation-universal-property l P f up-f Q =
  is-equiv-is-contr-map
    ( λ g → is-contr-equiv
      ( Σ (type-hom-Prop P Q) (λ h → (h ∘ f) ~ g))
      ( equiv-tot (λ h → equiv-funext))
      ( up-f Q g))

-- Remark 13.1.2

is-propositional-truncation' :
  ( l : Level) {l1 l2 : Level} {A : UU l1} (P : UU-Prop l2) →
  ( A → type-Prop P) → UU (lsuc l ⊔ l1 ⊔ l2)
is-propositional-truncation' l {A = A} P f =
  (Q : UU-Prop l) → (A → type-Prop Q) → (type-hom-Prop P Q)

is-propositional-truncation-simpl :
  { l1 l2 : Level} {A : UU l1} (P : UU-Prop l2)
  ( f : A → type-Prop P) →
  ( (l : Level) → is-propositional-truncation' l P f) →
  ( (l : Level) → is-propositional-truncation l P f)
is-propositional-truncation-simpl P f up-P l Q =
  is-equiv-is-prop
    ( is-prop-Π (λ x → is-prop-type-Prop Q))
    ( is-prop-Π (λ x → is-prop-type-Prop Q))
    ( up-P l Q)

-- Example 13.1.3

--------------------------------------------------------------------------------

-- Section 6.3 Pointed types

-- Definition 6.3.1

UU-pt : (i : Level) → UU (lsuc i)
UU-pt i = Σ (UU i) (λ X → X)

type-UU-pt : {i : Level} → UU-pt i → UU i
type-UU-pt = pr1

pt-UU-pt : {i : Level} (A : UU-pt i) → type-UU-pt A
pt-UU-pt = pr2

-- Definition 6.3.2

_→*_ : {i j : Level} → UU-pt i → UU-pt j → UU-pt (i ⊔ j)
A →* B =
  pair
    ( Σ (type-UU-pt A → type-UU-pt B) (λ f → Id (f (pt-UU-pt A)) (pt-UU-pt B)))
    ( pair
      ( const (type-UU-pt A) (type-UU-pt B) (pt-UU-pt B))
      ( refl))

-- Definition 6.3.3

Ω : {i : Level} → UU-pt i → UU-pt i
Ω A = pair (Id (pt-UU-pt A) (pt-UU-pt A)) refl

-- Definition 6.3.4

iterated-loop-space : {i : Level} → ℕ → UU-pt i → UU-pt i
iterated-loop-space zero-ℕ A = A
iterated-loop-space (succ-ℕ n) A = Ω (iterated-loop-space n A)

--------------------------------------------------------------------------------

is-propositional-truncation-const-star :
  { l1 : Level} (A : UU-pt l1)
  ( l : Level) → is-propositional-truncation l unit-Prop (const (type-UU-pt A) unit star)
is-propositional-truncation-const-star A =
  is-propositional-truncation-simpl
    ( unit-Prop)
    ( const (type-UU-pt A) unit star)
    ( λ l P f → const unit (type-Prop P) (f (pt-UU-pt A)))

-- Example 13.1.4

is-propositional-truncation-id :
  { l1 : Level} (P : UU-Prop l1) →
  ( l : Level) → is-propositional-truncation l P id
is-propositional-truncation-id P l Q =
  is-equiv-id (type-hom-Prop P Q)

-- Proposition 13.1.5

abstract
  is-equiv-is-equiv-precomp-Prop :
    {l1 l2 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) (f : type-hom-Prop P Q) →
    ((l : Level) (R : UU-Prop l) →
    is-equiv (precomp-Prop Q f R)) → is-equiv f
  is-equiv-is-equiv-precomp-Prop P Q f is-equiv-precomp-f =
    is-equiv-is-equiv-precomp-subuniverse id (λ l → is-prop) P Q f
      is-equiv-precomp-f

triangle-3-for-2-is-ptruncation :
  {l1 l2 l3 : Level} {A : UU l1} (P : UU-Prop l2) (P' : UU-Prop l3)
  (f : A → type-Prop P) (f' : A → type-Prop P')
  (h : type-hom-Prop P P') (H : (h ∘ f) ~ f') →
  {l : Level} (Q : UU-Prop l) →
  ( precomp-Prop P' f' Q) ~
  ( (precomp-Prop P f Q) ∘ (precomp h (type-Prop Q)))
triangle-3-for-2-is-ptruncation P P' f f' h H Q g =
  eq-htpy (λ p → inv (ap g (H p)))

is-equiv-is-ptruncation-is-ptruncation :
  {l1 l2 l3 : Level} {A : UU l1} (P : UU-Prop l2) (P' : UU-Prop l3)
  (f : A → type-Prop P) (f' : A → type-Prop P')
  (h : type-hom-Prop P P') (H : (h ∘ f) ~ f') →
  ((l : Level) → is-propositional-truncation l P f) →
  ((l : Level) → is-propositional-truncation l P' f') →
  is-equiv h
is-equiv-is-ptruncation-is-ptruncation P P' f f' h H is-ptr-P is-ptr-P' =
  is-equiv-is-equiv-precomp-Prop P P' h
    ( λ l Q →
      is-equiv-right-factor
        ( precomp-Prop P' f' Q)
        ( precomp-Prop P f Q)
        ( precomp h (type-Prop Q))
        ( triangle-3-for-2-is-ptruncation P P' f f' h H Q)
        ( is-ptr-P l Q)
        ( is-ptr-P' l Q))

is-ptruncation-is-ptruncation-is-equiv :
  {l1 l2 l3 : Level} {A : UU l1} (P : UU-Prop l2) (P' : UU-Prop l3)
  (f : A → type-Prop P) (f' : A → type-Prop P')
  (h : type-hom-Prop P P') (H : (h ∘ f) ~ f') →
  is-equiv h →
  ((l : Level) → is-propositional-truncation l P f) →
  ((l : Level) → is-propositional-truncation l P' f')
is-ptruncation-is-ptruncation-is-equiv P P' f f' h H is-equiv-h is-ptr-f l Q =
  is-equiv-comp
    ( precomp-Prop P' f' Q)
    ( precomp-Prop P f Q)
    ( precomp h (type-Prop Q))
    ( triangle-3-for-2-is-ptruncation P P' f f' h H Q)
    ( is-equiv-precomp-is-equiv h is-equiv-h (type-Prop Q))
    ( is-ptr-f l Q)

is-ptruncation-is-equiv-is-ptruncation :
  {l1 l2 l3 : Level} {A : UU l1} (P : UU-Prop l2) (P' : UU-Prop l3)
  (f : A → type-Prop P) (f' : A → type-Prop P')
  (h : type-hom-Prop P P') (H : (h ∘ f) ~ f') →
  ((l : Level) → is-propositional-truncation l P' f') →
  is-equiv h →
  ((l : Level) → is-propositional-truncation l P f)
is-ptruncation-is-equiv-is-ptruncation P P' f f' h H is-ptr-f' is-equiv-h l Q =
  is-equiv-left-factor
    ( precomp-Prop P' f' Q)
    ( precomp-Prop P f Q)
    ( precomp h (type-Prop Q))
    ( triangle-3-for-2-is-ptruncation P P' f f' h H Q)
    ( is-ptr-f' l Q)
    ( is-equiv-precomp-is-equiv h is-equiv-h (type-Prop Q))

-- Corollary 13.1.6

is-uniquely-unique-propositional-truncation :
  {l1 l2 l3 : Level} {A : UU l1} (P : UU-Prop l2) (P' : UU-Prop l3)
  (f : A → type-Prop P) (f' : A → type-Prop P') →
  ({l : Level} → is-propositional-truncation l P f) →
  ({l : Level} → is-propositional-truncation l P' f') →
  is-contr (Σ (equiv-Prop P P') (λ e → (map-equiv e ∘ f) ~ f'))
is-uniquely-unique-propositional-truncation P P' f f' is-ptr-f is-ptr-f' =
  is-contr-total-Eq-substructure
    ( universal-property-is-propositional-truncation _ P f is-ptr-f P' f')
    ( is-subtype-is-equiv)
    ( map-is-propositional-truncation P f is-ptr-f P' f')
    ( htpy-is-propositional-truncation P f is-ptr-f P' f')
    ( is-equiv-is-ptruncation-is-ptruncation  P P' f f'
      ( map-is-propositional-truncation P f is-ptr-f P' f')
      ( htpy-is-propositional-truncation P f is-ptr-f P' f')
      ( λ l → is-ptr-f)
      ( λ l → is-ptr-f'))

-- Axiom 13.1.8

postulate type-trunc-Prop : {l : Level} → UU l → UU l

postulate is-prop-type-trunc-Prop : {l : Level} (A : UU l) → is-prop (type-trunc-Prop A)

trunc-Prop : {l : Level} → UU l → UU-Prop l
trunc-Prop A = pair (type-trunc-Prop A) (is-prop-type-trunc-Prop A)

postulate unit-trunc-Prop : {l : Level} (A : UU l) → A → type-Prop (trunc-Prop A)

postulate is-propositional-truncation-trunc-Prop : {l1 l2 : Level} (A : UU l1) → is-propositional-truncation l2 (trunc-Prop A) (unit-trunc-Prop A)

universal-property-trunc-Prop : {l1 l2 : Level} (A : UU l1) →
  universal-property-propositional-truncation l2
    ( trunc-Prop A)
    ( unit-trunc-Prop A)
universal-property-trunc-Prop A =
  universal-property-is-propositional-truncation _
    ( trunc-Prop A)
    ( unit-trunc-Prop A)
    ( is-propositional-truncation-trunc-Prop A)

map-universal-property-trunc-Prop :
  {l1 l2 : Level} {A : UU l1} (P : UU-Prop l2) →
  (A → type-Prop P) → type-hom-Prop (trunc-Prop A) P
map-universal-property-trunc-Prop {A = A} P f =
  map-is-propositional-truncation
    ( trunc-Prop A)
    ( unit-trunc-Prop A)
    ( is-propositional-truncation-trunc-Prop A)
    ( P)
    ( f)

-- Proposition 13.1.9

unique-functor-trunc-Prop :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  is-contr
    ( Σ ( type-hom-Prop (trunc-Prop A) (trunc-Prop B))
        ( λ h → (h ∘ (unit-trunc-Prop A)) ~ ((unit-trunc-Prop B) ∘ f)))
unique-functor-trunc-Prop {l1} {l2} {A} {B} f =
  universal-property-trunc-Prop A (trunc-Prop B) ((unit-trunc-Prop B) ∘ f)

functor-trunc-Prop :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  (A → B) → type-hom-Prop (trunc-Prop A) (trunc-Prop B)
functor-trunc-Prop f =
  pr1 (center (unique-functor-trunc-Prop f))

htpy-functor-trunc-Prop :
  { l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  ( (functor-trunc-Prop f) ∘ (unit-trunc-Prop A)) ~ ((unit-trunc-Prop B) ∘ f)
htpy-functor-trunc-Prop f =
  pr2 (center (unique-functor-trunc-Prop f))

htpy-uniqueness-functor-trunc-Prop :
  { l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  ( h : type-hom-Prop (trunc-Prop A) (trunc-Prop B)) →
  ( ( h ∘ (unit-trunc-Prop A)) ~ ((unit-trunc-Prop B) ∘ f)) →
  (functor-trunc-Prop f) ~ h
htpy-uniqueness-functor-trunc-Prop f h H =
  htpy-eq (ap pr1 (contraction (unique-functor-trunc-Prop f) (pair h H)))

id-functor-trunc-Prop :
  { l1 : Level} {A : UU l1} → functor-trunc-Prop (id {A = A}) ~ id
id-functor-trunc-Prop {l1} {A} =
  htpy-uniqueness-functor-trunc-Prop id id refl-htpy

comp-functor-trunc-Prop :
  { l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
  ( g : B → C) (f : A → B) →
  ( functor-trunc-Prop (g ∘ f)) ~
  ( (functor-trunc-Prop g) ∘ (functor-trunc-Prop f))
comp-functor-trunc-Prop g f =
  htpy-uniqueness-functor-trunc-Prop
    ( g ∘ f)
    ( (functor-trunc-Prop g) ∘ (functor-trunc-Prop f))
    ( ( (functor-trunc-Prop g) ·l (htpy-functor-trunc-Prop f)) ∙h
      ( ( htpy-functor-trunc-Prop g) ·r f))

--------------------------------------------------------------------------------

-- Section 13.2 Propositional truncations as higher inductive types

-- Definition 13.2.1

case-paths-induction-principle-propositional-truncation :
  { l : Level} {l1 l2 : Level} {A : UU l1}
  ( P : UU-Prop l2) (α : (p q : type-Prop P) → Id p q) (f : A → type-Prop P) →
  ( B : type-Prop P → UU l) → UU (l ⊔ l2)
case-paths-induction-principle-propositional-truncation P α f B =
  (p q : type-Prop P) (x : B p) (y : B q) → Id (tr B (α p q) x) y

induction-principle-propositional-truncation :
  (l : Level) {l1 l2 : Level} {A : UU l1}
  (P : UU-Prop l2) (α : (p q : type-Prop P) → Id p q) (f : A → type-Prop P) →
  UU (lsuc l ⊔ l1 ⊔ l2)
induction-principle-propositional-truncation l {l1} {l2} {A} P α f =
  ( B : type-Prop P → UU l) →
  ( g : (x : A) → (B (f x))) →
  ( β : case-paths-induction-principle-propositional-truncation P α f B) →
  Σ ((p : type-Prop P) → B p) (λ h → (x : A) → Id (h (f x)) (g x))

-- Lemma 13.2.2

is-prop-case-paths-induction-principle-propositional-truncation :
  { l : Level} {l1 l2 : Level} {A : UU l1}
  ( P : UU-Prop l2) (α : (p q : type-Prop P) → Id p q) (f : A → type-Prop P) →
  ( B : type-Prop P → UU l) →
  case-paths-induction-principle-propositional-truncation P α f B →
  ( p : type-Prop P) → is-prop (B p)
is-prop-case-paths-induction-principle-propositional-truncation P α f B β p =
  is-prop-is-contr-if-inh (λ x → pair (tr B (α p p) x) (β p p x))

case-paths-induction-principle-propositional-truncation-is-prop :
  { l : Level} {l1 l2 : Level} {A : UU l1}
  ( P : UU-Prop l2) (α : (p q : type-Prop P) → Id p q) (f : A → type-Prop P) →
  ( B : type-Prop P → UU l) →
  ( (p : type-Prop P) → is-prop (B p)) →
  case-paths-induction-principle-propositional-truncation P α f B
case-paths-induction-principle-propositional-truncation-is-prop
  P α f B is-prop-B p q x y =
  is-prop'-is-prop (is-prop-B q) (tr B (α p q) x) y

-- Definition 13.2.3

dependent-universal-property-propositional-truncation :
  ( l : Level) {l1 l2 : Level} {A : UU l1}
  ( P : UU-Prop l2) (f : A → type-Prop P) → UU (lsuc l ⊔ l1 ⊔ l2)
dependent-universal-property-propositional-truncation l {l1} {l2} {A} P f =
  ( Q : type-Prop P → UU-Prop l) → is-equiv (precomp-Π f (type-Prop ∘ Q))

-- Theorem 13.2.4

abstract
  dependent-universal-property-is-propositional-truncation :
    { l1 l2 : Level} {A : UU l1} (P : UU-Prop l2) (f : A → type-Prop P) →
    ( {l : Level} → is-propositional-truncation l P f) →
    ( {l : Level} → dependent-universal-property-propositional-truncation l P f)
  dependent-universal-property-is-propositional-truncation
    {l1} {l2} {A} P f is-ptr-f Q =
    is-fiberwise-equiv-is-equiv-toto-is-equiv-base-map
      ( λ (g : A → type-Prop P) → (x : A) → type-Prop (Q (g x)))
      ( precomp f (type-Prop P))
      ( λ h → precomp-Π f (λ p → type-Prop (Q (h p))))
      ( is-ptr-f P)
      ( is-equiv-top-is-equiv-bottom-square
        ( inv-choice-∞
          { C = λ (x : type-Prop P) (p : type-Prop P) → type-Prop (Q p)})
        ( inv-choice-∞
          { C = λ (x : A) (p : type-Prop P) → type-Prop (Q p)})
        ( toto
          ( λ (g : A → type-Prop P) → (x : A) → type-Prop (Q (g x)))
          ( precomp f (type-Prop P))
          ( λ h → precomp-Π f (λ p → type-Prop (Q (h p)))))
        ( precomp f (Σ (type-Prop P) (λ p → type-Prop (Q p))))
        ( ind-Σ (λ h h' → refl))
        ( is-equiv-inv-choice-∞)
        ( is-equiv-inv-choice-∞)
        ( is-ptr-f (Σ-Prop P Q)))
      ( id {A = type-Prop P})

dependent-universal-property-trunc-Prop :
  {l l1 : Level} (A : UU l1) →
  dependent-universal-property-propositional-truncation l
    ( trunc-Prop A)
    ( unit-trunc-Prop A)
dependent-universal-property-trunc-Prop A =
  dependent-universal-property-is-propositional-truncation
    ( trunc-Prop A)
    ( unit-trunc-Prop A)
    ( is-propositional-truncation-trunc-Prop A)

abstract
  is-propositional-truncation-dependent-universal-property :
    { l1 l2 : Level} {A : UU l1} (P : UU-Prop l2) (f : A → type-Prop P) →
    ( {l : Level} →
      dependent-universal-property-propositional-truncation l P f) →
    ( {l : Level} → is-propositional-truncation l P f)
  is-propositional-truncation-dependent-universal-property P f dup-f Q =
    dup-f (λ p → Q)

abstract
  induction-principle-dependent-universal-property-propositional-truncation :
    { l1 l2 : Level} {A : UU l1} (P : UU-Prop l2) (f : A → type-Prop P) →
    ( {l : Level} →
      dependent-universal-property-propositional-truncation l P f) →
    ( {l : Level} → induction-principle-propositional-truncation l P
      ( is-prop'-is-prop (is-prop-type-Prop P)) f)
  induction-principle-dependent-universal-property-propositional-truncation
    P f dup-f B g α =
    tot
      ( λ h → htpy-eq)
      ( center
        ( is-contr-map-is-equiv
          ( dup-f
            ( λ p →
              pair
                ( B p)
                ( is-prop-case-paths-induction-principle-propositional-truncation
                  ( P)
                  ( is-prop'-is-prop (is-prop-type-Prop P))
                  f B α p)))
          ( g)))

abstract
  dependent-universal-property-induction-principle-propositional-truncation :
    { l1 l2 : Level} {A : UU l1} (P : UU-Prop l2) (f : A → type-Prop P) →
    ( {l : Level} → induction-principle-propositional-truncation l P
      ( is-prop'-is-prop (is-prop-type-Prop P)) f) →
    ( {l : Level} → dependent-universal-property-propositional-truncation l P f)
  dependent-universal-property-induction-principle-propositional-truncation
    P f ind-f Q =
    is-equiv-is-prop
      ( is-prop-Π (λ p → is-prop-type-Prop (Q p)))
      ( is-prop-Π (λ a → is-prop-type-Prop (Q (f a))))
      ( λ g →
        pr1
          ( ind-f
            ( λ p → type-Prop (Q p))
            ( g)
            ( case-paths-induction-principle-propositional-truncation-is-prop
              ( P)
              ( is-prop'-is-prop (is-prop-type-Prop P))
              ( f)
              ( λ p → type-Prop (Q p))
              ( λ p → is-prop-type-Prop (Q p)))))

--------------------------------------------------------------------------------

{- We introduce the image inclusion of a map. -}

comp-hom-slice :
  {l1 l2 l3 l4 : Level} {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  (f : A → X) (g : B → X) (h : C → X) →
  hom-slice g h → hom-slice f g → hom-slice f h
comp-hom-slice f g h j i =
  pair ( ( map-hom-slice g h j) ∘
         ( map-hom-slice f g i))
       ( ( triangle-hom-slice f g i) ∙h
         ( (triangle-hom-slice g h j) ·r (map-hom-slice f g i)))

id-hom-slice :
  {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → hom-slice f f
id-hom-slice f = pair id refl-htpy

is-equiv-hom-slice :
  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
  (f : A → X) (g : B → X) → hom-slice f g → UU (l2 ⊔ l3)
is-equiv-hom-slice f g h = is-equiv (map-hom-slice f g h)

precomp-emb :
  { l1 l2 l3 l4 : Level} {X : UU l1} {A : UU l2} (f : A → X)
  {B : UU l3} ( i : B ↪ X) (q : hom-slice f (map-emb i)) →
  {C : UU l4} ( j : C ↪ X) (r : hom-slice (map-emb i) (map-emb j)) →
  hom-slice f (map-emb j)
precomp-emb f i q j r =
  pair
    ( ( map-hom-slice (map-emb i) (map-emb j) r) ∘
      ( map-hom-slice f (map-emb i) q))
    ( ( triangle-hom-slice f (map-emb i) q) ∙h
      ( ( triangle-hom-slice (map-emb i) (map-emb j) r) ·r
        ( map-hom-slice f (map-emb i) q)))

is-prop-hom-slice :
  { l1 l2 l3 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  { B : UU l3} (i : B ↪ X) → is-prop (hom-slice f (map-emb i))
is-prop-hom-slice {X = X} f i =
  is-prop-is-equiv
    ( (x : X) → fib f x → fib (map-emb i) x)
    ( fiberwise-hom-hom-slice f (map-emb i))
    ( is-equiv-fiberwise-hom-hom-slice f (map-emb i))
    ( is-prop-Π
      ( λ x → is-prop-Π
        ( λ p → is-prop-map-is-emb (map-emb i) (is-emb-map-emb i) x)))

universal-property-image :
  ( l : Level) {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  { B : UU l3} (i : B ↪ X) (q : hom-slice f (map-emb i)) →
  UU (lsuc l ⊔ l1 ⊔ l2 ⊔ l3)
universal-property-image l {X = X} f i q =
  ( C : UU l) (j : C ↪ X) → is-equiv (precomp-emb f i q j)

universal-property-image' :
  ( l : Level) {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  { B : UU l3} (i : B ↪ X) (q : hom-slice f (map-emb i)) →
  UU (lsuc l ⊔ l1 ⊔ l2 ⊔ l3)
universal-property-image' l {X = X} f i q =
  ( C : UU l) (j : C ↪ X) →
    hom-slice f (map-emb j) → hom-slice (map-emb i) (map-emb j)

universal-property-image-universal-property-image' :
  ( l : Level) {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  { B : UU l3} (i : B ↪ X) (q : hom-slice f (map-emb i)) →
  universal-property-image' l f i q → universal-property-image l f i q
universal-property-image-universal-property-image' l f i q up' C j =
  is-equiv-is-prop
    ( is-prop-hom-slice (map-emb i) j)
    ( is-prop-hom-slice f j)
    ( up' C j)

{- Remark 14.4.4 -}

universal-property-image-has-section :
  (l : Level) {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  sec f → universal-property-image l f emb-id (pair f refl-htpy)
universal-property-image-has-section l f (pair g H) =
  universal-property-image-universal-property-image'
    l f emb-id (pair f refl-htpy)
    ( λ B m h → pair ((pr1 h) ∘ g) ( λ x → (inv (H x)) ∙ (pr2 h (g x))))

universal-property-image-is-emb :
  (l : Level) {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  (H : is-emb f) → universal-property-image l f (pair f H) (pair id refl-htpy)
universal-property-image-is-emb l f H =
  universal-property-image-universal-property-image'
    l f (pair f H) (pair id refl-htpy)
    ( λ B m h → h)

{- The existence of the image -}

im :
  {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → UU (l1 ⊔ l2)
im {X = X} {A} f = Σ X (λ x → type-trunc-Prop (fib f x))

inclusion-im :
  {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → im f → X
inclusion-im f = pr1

is-emb-inclusion-im :
  {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  is-emb (inclusion-im f)
is-emb-inclusion-im f =
  is-emb-pr1-is-subtype (λ x → is-prop-type-trunc-Prop (fib f x))

emb-im :
  {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → im f ↪ X
emb-im f = pair (inclusion-im f) (is-emb-inclusion-im f)

map-im :
  {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → A → im f
map-im f a = pair (f a) (unit-trunc-Prop (fib f (f a)) (pair a refl))

triangle-im :
  {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  f ~ (inclusion-im f ∘ map-im f)
triangle-im f a = refl

hom-slice-im :
  {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  hom-slice f (inclusion-im f)
hom-slice-im f = pair (map-im f) (triangle-im f)

fiberwise-map-universal-property-im :
  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3} (f : A → X) →
  (m : B ↪ X) (h : hom-slice f (map-emb m)) →
  (x : X) → type-trunc-Prop (fib f x) → fib (map-emb m) x
fiberwise-map-universal-property-im f m h x =
  map-universal-property-trunc-Prop
    { A = (fib f x)}
    ( fib-prop-emb m x)
    ( λ t →
      pair ( map-hom-slice f (map-emb m) h (pr1 t))
           ( ( inv (triangle-hom-slice f (map-emb m) h (pr1 t))) ∙
             ( pr2 t)))

map-universal-property-im :
  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3} (f : A → X) →
  (m : B ↪ X) (h : hom-slice f (map-emb m)) → im f → B
map-universal-property-im f m h (pair x t) =
  pr1 (fiberwise-map-universal-property-im f m h x t)

triangle-universal-property-im :
  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3} (f : A → X) →
  (m : B ↪ X) (h : hom-slice f (map-emb m)) →
  inclusion-im f ~ ((map-emb m) ∘ (map-universal-property-im f m h))
triangle-universal-property-im f m h (pair x t) =
  inv (pr2 (fiberwise-map-universal-property-im f m h x t))

universal-property-im :
  (l : Level) {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  universal-property-image l f (emb-im f) (hom-slice-im f)
universal-property-im l f =
  universal-property-image-universal-property-image'
    l f (emb-im f) (hom-slice-im f)
    ( λ B m h →
      pair ( map-universal-property-im f m h)
           ( triangle-universal-property-im f m h))

{- The uniqueness of the image -}

is-equiv-hom-slice-emb :
  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
  (f : A ↪ X) (g : B ↪ X) (h : hom-slice (map-emb f) (map-emb g)) →
  hom-slice (map-emb g) (map-emb f) →
  is-equiv-hom-slice (map-emb f) (map-emb g) h
is-equiv-hom-slice-emb f g h i =
  is-equiv-has-inverse
    ( map-hom-slice (map-emb g) (map-emb f) i)
    ( λ y →
      eq-emb g
      ( inv
        ( ( triangle-hom-slice
            ( map-emb g)
            ( map-emb f)
            ( i)
            ( y)) ∙
          ( triangle-hom-slice
            ( map-emb f)
            ( map-emb g)
            ( h)
            ( map-hom-slice (map-emb g) (map-emb f) i y)))))
    ( λ x →
      eq-emb f
      ( inv
        ( ( triangle-hom-slice (map-emb f) (map-emb g) h x) ∙
          ( triangle-hom-slice (map-emb g) (map-emb f) i
            ( map-hom-slice
              ( map-emb f)
              ( map-emb g)
              ( h)
              ( x))))))

is-equiv-up-image-up-image :
  {l1 l2 l3 l4 : Level} {X : UU l1} {A : UU l2} (f : A → X)
  {B : UU l3} (i : B ↪ X) (q : hom-slice f (map-emb i))
  {B' : UU l4} (i' : B' ↪ X) (q' : hom-slice f (map-emb i'))
  (h : hom-slice (map-emb i) (map-emb i'))
  (p : Id (comp-hom-slice f (map-emb i) (map-emb i') h q) q') →
  ({l : Level} → universal-property-image l f i q) →
  ({l : Level} → universal-property-image l f i' q') →
  is-equiv (map-hom-slice (map-emb i) (map-emb i') h)
is-equiv-up-image-up-image f i q i' q' h p up-i up-i' =
  is-equiv-hom-slice-emb i i' h (inv-is-equiv (up-i' _ i) q)

up-image-up-image-is-equiv :
  {l1 l2 l3 l4 : Level} {X : UU l1} {A : UU l2} (f : A → X)
  {B : UU l3} (i : B ↪ X) (q : hom-slice f (map-emb i))
  {B' : UU l4} (i' : B' ↪ X) (q' : hom-slice f (map-emb i'))
  (h : hom-slice (map-emb i) (map-emb i'))
  (p : Id (comp-hom-slice f (map-emb i) (map-emb i') h q) q') →
  is-equiv (map-hom-slice (map-emb i) (map-emb i') h) →
  ({l : Level} → universal-property-image l f i q) →
  ({l : Level} → universal-property-image l f i' q')
up-image-up-image-is-equiv f i q i' q' h p is-equiv-h up-i {l} =
  universal-property-image-universal-property-image' l f i' q'
    ( λ C j r →
      comp-hom-slice
        ( map-emb i')
        ( map-emb i)
        ( map-emb j)
        ( inv-is-equiv (up-i C j) r)
        ( pair
          ( inv-is-equiv is-equiv-h)
          ( triangle-section
            ( map-emb i)
            ( map-emb i')
            ( map-hom-slice (map-emb i) (map-emb i') h)
            ( triangle-hom-slice (map-emb i) (map-emb i') h)
            ( pair ( inv-is-equiv is-equiv-h)
                   ( issec-inv-is-equiv is-equiv-h)))))

up-image-is-equiv-up-image :
  {l1 l2 l3 l4 : Level} {X : UU l1} {A : UU l2} (f : A → X)
  {B : UU l3} (i : B ↪ X) (q : hom-slice f (map-emb i))
  {B' : UU l4} (i' : B' ↪ X) (q' : hom-slice f (map-emb i'))
  (h : hom-slice (map-emb i) (map-emb i'))
  (p : Id (comp-hom-slice f (map-emb i) (map-emb i') h q) q') →
  ({l : Level} → universal-property-image l f i' q') →
  is-equiv (map-hom-slice (map-emb i) (map-emb i') h) →
  ({l : Level} → universal-property-image l f i q)
up-image-is-equiv-up-image f i q i' q' h p up-i' is-equiv-h {l} =
  universal-property-image-universal-property-image' l f i q
    ( λ C j r →
      comp-hom-slice
        ( map-emb i)
        ( map-emb i')
        ( map-emb j)
        ( inv-is-equiv (up-i' C j) r)
        ( h))

--------------------------------------------------------------------------------

{- Existential quantification -}

exists-Prop :
  {l1 l2 : Level} {A : UU l1} (P : A → UU-Prop l2) → UU-Prop (l1 ⊔ l2)
exists-Prop {l1} {l2} {A} P = trunc-Prop (Σ A (λ x → type-Prop (P x)))

exists :
  {l1 l2 : Level} {A : UU l1} (P : A → UU-Prop l2) → UU (l1 ⊔ l2)
exists P = type-Prop (exists-Prop P)

is-prop-exists :
  {l1 l2 : Level} {A : UU l1} (P : A → UU-Prop l2) → is-prop (exists P)
is-prop-exists P = is-prop-type-Prop (exists-Prop P)

--------------------------------------------------------------------------------

{- Surjective maps -}

-- Definition 13.5.1

is-surjective :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → UU (l1 ⊔ l2)
is-surjective {B = B} f = (y : B) → type-trunc-Prop (fib f y)

-- Proposition 13.5.3

dependent-universal-property-surj :
  (l : Level) {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  UU ((lsuc l) ⊔ l1 ⊔ l2)
dependent-universal-property-surj l {B = B} f =
  (P : B → UU-Prop l) →
    is-equiv (λ (h : (b : B) → type-Prop (P b)) x → h (f x))

is-surjective-dependent-universal-property-surj :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  ({l : Level} → dependent-universal-property-surj l f) →
  is-surjective f
is-surjective-dependent-universal-property-surj f dup-surj-f =
  inv-is-equiv
    ( dup-surj-f (λ b → trunc-Prop (fib f b)))
    ( λ x → unit-trunc-Prop (fib f (f x)) (pair x refl))

square-dependent-universal-property-surj :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  (P : B → UU-Prop l3) →
  ( λ (h : (y : B) → type-Prop (P y)) x → h (f x)) ~
  ( ( λ h x → h (f x) (pair x refl)) ∘
    ( ( λ h y → (h y) ∘ (unit-trunc-Prop (fib f y))) ∘
      ( λ h y → const (type-trunc-Prop (fib f y)) (type-Prop (P y)) (h y))))
square-dependent-universal-property-surj f P = refl-htpy

dependent-universal-property-surj-is-surjective :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  is-surjective f →
  ({l : Level} → dependent-universal-property-surj l f)
dependent-universal-property-surj-is-surjective f is-surj-f P =
  is-equiv-comp'
    ( λ h x → h (f x) (pair x refl))
    ( ( λ h y → (h y) ∘ (unit-trunc-Prop (fib f y))) ∘
      ( λ h y → const (type-trunc-Prop (fib f y)) (type-Prop (P y)) (h y)))
    ( is-equiv-comp'
      ( λ h y → (h y) ∘ (unit-trunc-Prop (fib f y)))
      ( λ h y → const (type-trunc-Prop (fib f y)) (type-Prop (P y)) (h y))
      ( is-equiv-postcomp-Π
        ( λ y p z → p)
        ( λ y →
          is-equiv-diagonal-is-contr
            ( is-surj-f y)
            ( is-contr-is-prop-inh
              ( is-prop-type-trunc-Prop (fib f y))
              ( is-surj-f y))
            ( type-Prop (P y))))
      ( is-equiv-postcomp-Π
        ( λ b g → g ∘ (unit-trunc-Prop (fib f b)))
        ( λ b → is-propositional-truncation-trunc-Prop (fib f b) (P b))))
    ( is-equiv-map-reduce-Π-fib f ( λ y z → type-Prop (P y)))

-- Theorem 13.5.5

--------------------------------------------------------------------------------

{- Cantor's diagonal argument -}

map-cantor :
  {l1 l2 : Level} (X : UU l1) (f : X → (X → UU-Prop l2)) → (X → UU-Prop l2)
map-cantor X f x = neg-Prop (f x x)

iff-eq :
  {l1 : Level} {P Q : UU-Prop l1} → Id P Q → P ↔ Q
iff-eq refl = pair id id

no-fixed-points-neg-Prop :
  {l1 : Level} (P : UU-Prop l1) → ¬ (P ↔ neg-Prop P)
no-fixed-points-neg-Prop P = no-fixed-points-neg (type-Prop P)

not-in-image-map-cantor :
  {l1 l2 : Level} (X : UU l1) (f : X → (X → UU-Prop l2)) →
  ( t : fib f (map-cantor X f)) → empty
not-in-image-map-cantor X f (pair x α) =
  no-fixed-points-neg-Prop (f x x) (iff-eq (htpy-eq α x))

cantor : {l1 l2 : Level} (X : UU l1) (f : X → (X → UU-Prop l2)) →
  ¬ (is-surjective f)
cantor X f H =
  ( map-universal-property-trunc-Prop empty-Prop
    ( not-in-image-map-cantor X f)
    ( H (map-cantor X f)))

--------------------------------------------------------------------------------

-- Exercises

-- Exercise 13.1

is-propositional-truncation-retract :
  {l l1 l2 : Level} {A : UU l1} (P : UU-Prop l2) →
  (R : (type-Prop P) retract-of A) →
  is-propositional-truncation l P (retraction-retract-of R)
is-propositional-truncation-retract {A = A} P R Q =
  is-equiv-is-prop
    ( is-prop-function-type (is-prop-type-Prop Q))
    ( is-prop-function-type (is-prop-type-Prop Q))
    ( λ g → g ∘ (section-retract-of R))

-- Exercise 13.2

is-propositional-truncation-prod :
  {l1 l2 l3 l4 : Level}
  {A : UU l1} (P : UU-Prop l2) (f : A → type-Prop P)
  {A' : UU l3} (P' : UU-Prop l4) (f' : A' → type-Prop P') →
  ({l : Level} → is-propositional-truncation l P f) →
  ({l : Level} → is-propositional-truncation l P' f') →
  {l : Level} → is-propositional-truncation l (prod-Prop P P') (functor-prod f f')
is-propositional-truncation-prod P f P' f' is-ptr-f is-ptr-f' Q =
  is-equiv-top-is-equiv-bottom-square
    ( ev-pair)
    ( ev-pair)
    ( precomp (functor-prod f f') (type-Prop Q))
    ( λ h a a' → h (f a) (f' a'))
    ( refl-htpy)
    ( is-equiv-ev-pair)
    ( is-equiv-ev-pair)
    ( is-equiv-comp'
      ( λ h a a' → h a (f' a'))
      ( λ h a p' → h (f a) p')
      ( is-ptr-f (pair (type-hom-Prop P' Q) (is-prop-type-hom-Prop P' Q)))
      ( is-equiv-postcomp-Π
        ( λ a g a' → g (f' a'))
        ( λ a → is-ptr-f' Q)))

equiv-prod-trunc-Prop :
  {l1 l2 : Level} (A : UU l1) (A' : UU l2) →
  equiv-Prop (trunc-Prop (A × A')) (prod-Prop (trunc-Prop A) (trunc-Prop A'))
equiv-prod-trunc-Prop A A' =
  pr1
    ( center
      ( is-uniquely-unique-propositional-truncation
        ( trunc-Prop (A × A'))
        ( prod-Prop (trunc-Prop A) (trunc-Prop A'))
        ( unit-trunc-Prop (A × A'))
        ( functor-prod (unit-trunc-Prop A) (unit-trunc-Prop A'))
        ( is-propositional-truncation-trunc-Prop (A × A'))
        ( is-propositional-truncation-prod
          ( trunc-Prop A)
          ( unit-trunc-Prop A)
          ( trunc-Prop A')
          ( unit-trunc-Prop A')
          ( is-propositional-truncation-trunc-Prop A)
          ( is-propositional-truncation-trunc-Prop A'))))

-- Exercise 13.3

-- Exercise 13.3(a)

conj-Prop = prod-Prop

type-conj-Prop :
  {l1 l2 : Level} → UU-Prop l1 → UU-Prop l2 → UU (l1 ⊔ l2)
type-conj-Prop P Q = type-Prop (conj-Prop P Q)

disj-Prop :
  {l1 l2 : Level} → UU-Prop l1 → UU-Prop l2 → UU-Prop (l1 ⊔ l2)
disj-Prop P Q = trunc-Prop (coprod (type-Prop P) (type-Prop Q))

type-disj-Prop :
  {l1 l2 : Level} → UU-Prop l1 → UU-Prop l2 → UU (l1 ⊔ l2)
type-disj-Prop P Q = type-Prop (disj-Prop P Q)

inl-disj-Prop :
  {l1 l2 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) →
  type-hom-Prop P (disj-Prop P Q)
inl-disj-Prop P Q =
  (unit-trunc-Prop (coprod (type-Prop P) (type-Prop Q))) ∘ inl

inr-disj-Prop :
  {l1 l2 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) →
  type-hom-Prop Q (disj-Prop P Q)
inr-disj-Prop P Q =
  (unit-trunc-Prop (coprod (type-Prop P) (type-Prop Q))) ∘ inr

-- Exercise 13.3(b)

ev-disj-Prop :
  {l1 l2 l3 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) (R : UU-Prop l3) →
  type-hom-Prop
    ( hom-Prop (disj-Prop P Q) R)
    ( conj-Prop (hom-Prop P R) (hom-Prop Q R))
ev-disj-Prop P Q R h =
  pair (h ∘ (inl-disj-Prop P Q)) (h ∘ (inr-disj-Prop P Q))

inv-ev-disj-Prop :
  {l1 l2 l3 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) (R : UU-Prop l3) →
  type-hom-Prop
    ( conj-Prop (hom-Prop P R) (hom-Prop Q R))
    ( hom-Prop (disj-Prop P Q) R)
inv-ev-disj-Prop P Q R (pair f g) =
  map-universal-property-trunc-Prop R (ind-coprod (λ t → type-Prop R) f g)

is-equiv-ev-disj-Prop :
  {l1 l2 l3 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) (R : UU-Prop l3) →
  is-equiv (ev-disj-Prop P Q R)
is-equiv-ev-disj-Prop P Q R =
  is-equiv-is-prop
    ( is-prop-type-Prop (hom-Prop (disj-Prop P Q) R))
    ( is-prop-type-Prop (conj-Prop (hom-Prop P R) (hom-Prop Q R)))
    ( inv-ev-disj-Prop P Q R)

-- Exercise 13.9

map-dn-trunc-Prop :
  {l : Level} (A : UU l) → ¬¬ (type-trunc-Prop A) → ¬¬ A
map-dn-trunc-Prop A =
  dn-extend (map-universal-property-trunc-Prop (dn-Prop A) intro-dn)

inv-map-dn-trunc-Prop :
  {l : Level} (A : UU l) → ¬¬ A → ¬¬ (type-trunc-Prop A)
inv-map-dn-trunc-Prop A =
  dn-extend (λ a → intro-dn (unit-trunc-Prop A a))

equiv-dn-trunc-Prop :
  {l : Level} (A : UU l) → ¬¬ (type-trunc-Prop A) ≃ ¬¬ A
equiv-dn-trunc-Prop A =
  equiv-iff
    ( dn-Prop (type-trunc-Prop A))
    ( dn-Prop A)
    ( pair
      ( map-dn-trunc-Prop A)
      ( inv-map-dn-trunc-Prop A))

-- Exercise 13.10

-- The impredicative encoding of the propositional truncation --

impredicative-trunc-Prop :
  {l : Level} → UU l → UU-Prop (lsuc l)
impredicative-trunc-Prop {l} A =
  Π-Prop
    ( UU-Prop l)
    ( λ Q → function-Prop (A → type-Prop Q) Q)

type-impredicative-trunc-Prop :
  {l : Level} → UU l → UU (lsuc l)
type-impredicative-trunc-Prop {l} A =
  type-Prop (impredicative-trunc-Prop A)

map-impredicative-trunc-Prop :
  {l : Level} (A : UU l) →
  type-trunc-Prop A → type-impredicative-trunc-Prop A
map-impredicative-trunc-Prop {l} A =
  map-universal-property-trunc-Prop
    ( impredicative-trunc-Prop A)
    ( λ x Q f → f x)

inv-map-impredicative-trunc-Prop :
  {l : Level} (A : UU l) →
  type-impredicative-trunc-Prop A → type-trunc-Prop A
inv-map-impredicative-trunc-Prop A H =
  H (trunc-Prop A) (unit-trunc-Prop A)

equiv-impredicative-trunc-Prop :
  {l : Level} (A : UU l) →
  type-trunc-Prop A ≃ type-impredicative-trunc-Prop A
equiv-impredicative-trunc-Prop A =
  equiv-iff
    ( trunc-Prop A)
    ( impredicative-trunc-Prop A)
    ( pair
      ( map-impredicative-trunc-Prop A)
      ( inv-map-impredicative-trunc-Prop A))

-- The impredicative encoding of conjunction --

impredicative-conj-Prop :
  {l1 l2 : Level} → UU-Prop l1 → UU-Prop l2 → UU-Prop (lsuc (l1 ⊔ l2))
impredicative-conj-Prop {l1} {l2} P1 P2 =
  Π-Prop
    ( UU-Prop (l1 ⊔ l2))
    ( λ Q → function-Prop (type-Prop P1 → (type-Prop P2 → type-Prop Q)) Q)

type-impredicative-conj-Prop :
  {l1 l2 : Level} → UU-Prop l1 → UU-Prop l2 → UU (lsuc (l1 ⊔ l2))
type-impredicative-conj-Prop P1 P2 =
  type-Prop (impredicative-conj-Prop P1 P2)

map-impredicative-conj-Prop :
  {l1 l2 : Level} (P1 : UU-Prop l1) (P2 : UU-Prop l2) →
  type-conj-Prop P1 P2 → type-impredicative-conj-Prop P1 P2
map-impredicative-conj-Prop {l1} {l2} P1 P2 (pair p1 p2) Q f =
  f p1 p2

inv-map-impredicative-conj-Prop :
  {l1 l2 : Level} (P1 : UU-Prop l1) (P2 : UU-Prop l2) →
  type-impredicative-conj-Prop P1 P2 → type-conj-Prop P1 P2
inv-map-impredicative-conj-Prop P1 P2 H =
  H (conj-Prop P1 P2) (λ p1 p2 → pair p1 p2)

equiv-impredicative-conj-Prop :
  {l1 l2 : Level} (P1 : UU-Prop l1) (P2 : UU-Prop l2) →
  type-conj-Prop P1 P2 ≃ type-impredicative-conj-Prop P1 P2
equiv-impredicative-conj-Prop P1 P2 =
  equiv-iff
    ( conj-Prop P1 P2)
    ( impredicative-conj-Prop P1 P2)
    ( pair
      ( map-impredicative-conj-Prop P1 P2)
      ( inv-map-impredicative-conj-Prop P1 P2))

-- The impredicative encoding of disjunction --

impredicative-disj-Prop :
  {l1 l2 : Level} → UU-Prop l1 → UU-Prop l2 → UU-Prop (lsuc (l1 ⊔ l2))
impredicative-disj-Prop {l1} {l2} P1 P2 =
  Π-Prop
    ( UU-Prop (l1 ⊔ l2))
    ( λ Q →
      function-Prop
        ( type-implication-Prop P1 Q)
        ( function-Prop (type-implication-Prop P2 Q) Q))

type-impredicative-disj-Prop :
  {l1 l2 : Level} → UU-Prop l1 → UU-Prop l2 → UU (lsuc (l1 ⊔ l2))
type-impredicative-disj-Prop P1 P2 =
  type-Prop (impredicative-disj-Prop P1 P2)

map-impredicative-disj-Prop :
  {l1 l2 : Level} (P1 : UU-Prop l1) (P2 : UU-Prop l2) →
  type-disj-Prop P1 P2 → type-impredicative-disj-Prop P1 P2
map-impredicative-disj-Prop {l1} {l2} P1 P2 =
  map-universal-property-trunc-Prop
    ( impredicative-disj-Prop P1 P2)
    ( ind-coprod
      ( λ x → type-impredicative-disj-Prop P1 P2)
      ( λ x Q f1 f2 → f1 x)
      ( λ y Q f1 f2 → f2 y))

inv-map-impredicative-disj-Prop :
  {l1 l2 : Level} (P1 : UU-Prop l1) (P2 : UU-Prop l2) →
  type-impredicative-disj-Prop P1 P2 → type-disj-Prop P1 P2
inv-map-impredicative-disj-Prop P1 P2 H =
  H (disj-Prop P1 P2) (inl-disj-Prop P1 P2) (inr-disj-Prop P1 P2)

equiv-impredicative-disj-Prop :
  {l1 l2 : Level} (P1 : UU-Prop l1) (P2 : UU-Prop l2) →
  type-disj-Prop P1 P2 ≃ type-impredicative-disj-Prop P1 P2
equiv-impredicative-disj-Prop P1 P2 =
  equiv-iff
    ( disj-Prop P1 P2)
    ( impredicative-disj-Prop P1 P2)
    ( pair
      ( map-impredicative-disj-Prop P1 P2)
      ( inv-map-impredicative-disj-Prop P1 P2))

-- The impredicative encoding of negation --

impredicative-neg-Prop :
  {l : Level} → UU l → UU-Prop (lsuc l)
impredicative-neg-Prop {l} A =
  Π-Prop (UU-Prop l) (λ Q → function-Prop A Q)

type-impredicative-neg-Prop :
  {l : Level} → UU l → UU (lsuc l)
type-impredicative-neg-Prop A =
  type-Prop (impredicative-neg-Prop A)

map-impredicative-neg-Prop :
  {l : Level} (A : UU l) →
  ¬ A → type-impredicative-neg-Prop A
map-impredicative-neg-Prop A f Q a = ex-falso (f a)

inv-map-impredicative-neg-Prop :
  {l : Level} (A : UU l) →
  type-impredicative-neg-Prop A → ¬ A
inv-map-impredicative-neg-Prop A H a = H (neg-Prop' A) a a

equiv-impredicative-neg-Prop :
  {l : Level} (A : UU l) →
  ¬ A ≃ type-impredicative-neg-Prop A
equiv-impredicative-neg-Prop A =
  equiv-iff
    ( neg-Prop' A)
    ( impredicative-neg-Prop A)
    ( pair
      ( map-impredicative-neg-Prop A)
      ( inv-map-impredicative-neg-Prop A))

-- The impredicative encoding of existential quantification --

impredicative-exists-Prop :
  {l1 l2 : Level} {A : UU l1} (P : A → UU-Prop l2) → UU-Prop (lsuc (l1 ⊔ l2))
impredicative-exists-Prop {l1} {l2} {A} P =
  Π-Prop
    ( UU-Prop (l1 ⊔ l2))
    ( λ Q → function-Prop ((x : A) → type-Prop (P x) → type-Prop Q) Q)

type-impredicative-exists-Prop :
  {l1 l2 : Level} {A : UU l1} (P : A → UU-Prop l2) → UU (lsuc (l1 ⊔ l2))
type-impredicative-exists-Prop P =
  type-Prop (impredicative-exists-Prop P)

map-impredicative-exists-Prop :
  {l1 l2 : Level} {A : UU l1} (P : A → UU-Prop l2) →
  exists P → type-impredicative-exists-Prop P
map-impredicative-exists-Prop {l1} {l2} {A} P =
  map-universal-property-trunc-Prop
    ( impredicative-exists-Prop P)
    ( ind-Σ (λ x y Q h → h x y))

inv-map-impredicative-exists-Prop :
  {l1 l2 : Level} {A : UU l1} (P : A → UU-Prop l2) →
  type-impredicative-exists-Prop P → exists P
inv-map-impredicative-exists-Prop {A = A} P H =
  H ( exists-Prop P)
    ( λ x y → unit-trunc-Prop (Σ A (λ x → type-Prop (P x))) (pair x y))

equiv-impredicative-exists-Prop :
  {l1 l2 : Level} {A : UU l1} (P : A → UU-Prop l2) →
  exists P ≃ type-impredicative-exists-Prop P
equiv-impredicative-exists-Prop P =
  equiv-iff
    ( exists-Prop P)
    ( impredicative-exists-Prop P)
    ( pair
      ( map-impredicative-exists-Prop P)
      ( inv-map-impredicative-exists-Prop P))

-- The impredicative encoding of the based identity type of a set --

impredicative-based-id-Prop :
  {l : Level} (A : UU-Set l) (a x : type-Set A) → UU-Prop (lsuc l)
impredicative-based-id-Prop {l} A a x =
  Π-Prop (type-Set A → UU-Prop l) (λ Q → hom-Prop (Q a) (Q x))

type-impredicative-based-id-Prop :
  {l : Level} (A : UU-Set l) (a x : type-Set A) → UU (lsuc l)
type-impredicative-based-id-Prop A a x =
  type-Prop (impredicative-based-id-Prop A a x)

map-impredicative-based-id-Prop :
  {l : Level} (A : UU-Set l) (a x : type-Set A) →
  Id a x → type-impredicative-based-id-Prop A a x
map-impredicative-based-id-Prop A a .a refl Q p = p

inv-map-impredicative-based-id-Prop :
  {l : Level} (A : UU-Set l) (a x : type-Set A) →
  type-impredicative-based-id-Prop A a x → Id a x
inv-map-impredicative-based-id-Prop A a x H =
  H (λ x → pair (Id a x) (is-set-type-Set A a x)) refl

equiv-impredicative-based-id-Prop :
  {l : Level} (A : UU-Set l) (a x : type-Set A) →
  Id a x ≃ type-impredicative-based-id-Prop A a x
equiv-impredicative-based-id-Prop A a x =
  equiv-iff
    ( pair (Id a x) (is-set-type-Set A a x))
    ( impredicative-based-id-Prop A a x)
    ( pair
      ( map-impredicative-based-id-Prop A a x)
      ( inv-map-impredicative-based-id-Prop A a x))

-- The impredicative encoding of Martin-Löf's identity type of a set --

impredicative-id-Prop :
  {l : Level} (A : UU-Set l) (x y : type-Set A) → UU-Prop (lsuc l)
impredicative-id-Prop {l} A x y =
  Π-Prop (type-Set A → type-Set A → UU-Prop l)
    (λ Q → function-Prop ((a : type-Set A) → type-Prop (Q a a)) (Q x y))

type-impredicative-id-Prop :
  {l : Level} (A : UU-Set l) (x y : type-Set A) → UU (lsuc l)
type-impredicative-id-Prop A x y =
  type-Prop (impredicative-id-Prop A x y)

map-impredicative-id-Prop :
  {l : Level} (A : UU-Set l) (x y : type-Set A) →
  Id x y → type-impredicative-id-Prop A x y
map-impredicative-id-Prop A x .x refl Q r = r x

inv-map-impredicative-id-Prop :
  {l : Level} (A : UU-Set l ) (x y : type-Set A) →
  type-impredicative-id-Prop A x y → Id x y
inv-map-impredicative-id-Prop A x y H =
  H (λ a b → pair (Id a b) (is-set-type-Set A a b)) (λ a → refl)

equiv-impredicative-id-Prop :
  {l : Level} (A : UU-Set l) (x y : type-Set A) →
  Id x y ≃ type-impredicative-id-Prop A x y
equiv-impredicative-id-Prop A x y =
  equiv-iff
    ( pair (Id x y) (is-set-type-Set A x y))
    ( impredicative-id-Prop A x y)
    ( pair
      ( map-impredicative-id-Prop A x y)
      ( inv-map-impredicative-id-Prop A x y))

-- The impredicative encoding of the based identity type of a 1-type --

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


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

module Cubical.Categories.Structures where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels using (isSetΣ)
open import Cubical.Data.Sigma

open import Cubical.Categories.Category

_∋_ : ∀ {ℓ} → (A : Type ℓ) → A → A
_∋_ A x = x

private
  variable
    ℓ ℓ' ℓ'' ℓ''' : Level
    𝒞 : Precategory ℓ ℓ'

record StructureOver (𝒞 : Precategory ℓ ℓ') ℓ'' ℓ''' : Type (ℓ-suc (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℓ'' ℓ'''))) where
  field
    Struct : 𝒞 .ob → Type ℓ''
    IsHomo : ∀ {x y} → Struct x → Struct y → 𝒞 .hom x y → Type ℓ'''
    isPropIsHomo : ∀ {x y α β f} → isProp (IsHomo {x} {y} α β f)

    idnIsHomo : ∀ {x} (α : Struct x) → IsHomo α α (𝒞 .idn x)
    homoSeq : ∀ {x y z α β γ} {f : 𝒞 .hom x y} {g : 𝒞 .hom y z} →
                IsHomo α β f → IsHomo β γ g → IsHomo α γ (𝒞 .seq f g)

  _⊆_ : ∀ {x} → Struct x → Struct x → Type ℓ'''
  _⊆_ {x} α β = IsHomo α β (𝒞 .idn x)

open StructureOver public renaming (_⊆_ to _[_⊆_])

record StrIsUnivalent {𝒞 : Precategory ℓ ℓ'} (S : StructureOver 𝒞 ℓ'' ℓ''') : Type (ℓ-suc (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℓ'' ℓ'''))) where
  field
    subAntisym : ∀ {x} {α β : S .Struct x} → S [ α ⊆ β ] → S [ β ⊆ α ] → α ≡ β

open StrIsUnivalent public

isPropP : {A : I → Type ℓ} {x : A i0} {y : A i1} → isProp (A i1) → PathP A x y
isPropP Aprop = toPathP (Aprop _ _)

STRUCTURES : (𝒞 : Precategory ℓ ℓ') → StructureOver 𝒞 ℓ'' ℓ''' → Precategory (ℓ-max ℓ ℓ'') (ℓ-max ℓ' ℓ''')
STRUCTURES 𝒞 S .ob = Σ (𝒞 .ob) (S .Struct)
STRUCTURES 𝒞 S .hom (x , α) (y , β) = Σ (𝒞 .hom x y) (S .IsHomo α β)
STRUCTURES 𝒞 S .idn (x , α) = 𝒞 .idn x , S .idnIsHomo α
STRUCTURES 𝒞 S .seq (f , hᶠ) (g , hᵍ) = 𝒞 .seq f g , S .homoSeq hᶠ hᵍ
STRUCTURES 𝒞 S .seq-λ (f , hᶠ) = cong₂ _,_ (𝒞 .seq-λ f) (toPathP (S .isPropIsHomo _ _))
STRUCTURES 𝒞 S .seq-ρ (f , hᶠ) = cong₂ _,_ (𝒞 .seq-ρ f) (toPathP (S .isPropIsHomo _ _))
STRUCTURES 𝒞 S .seq-α (f , hᶠ) (g , hᵍ) (h , hʰ) = cong₂ _,_ (𝒞 .seq-α f g h) (toPathP (S .isPropIsHomo _ _))

STRUCTURESisCat : ⦃ 𝒞-cat : isCategory 𝒞 ⦄ {S : StructureOver 𝒞 ℓ'' ℓ'''} → isCategory (STRUCTURES 𝒞 S)
STRUCTURESisCat {{𝒞-cat}} {S = S} .homIsSet {x = x , α} {y = y , β} = isSetΣ (𝒞-cat .homIsSet) (λ _ → isProp→isSet (S .isPropIsHomo))

SIP : ∀ ⦃ 𝒞-cat : isCategory 𝒞 ⦄ ⦃ 𝒞-univ : isUnivalent 𝒞 ⦄ → (S : StructureOver 𝒞 ℓ'' ℓ''') → ⦃ S-univ : StrIsUnivalent S ⦄ → isUnivalent (STRUCTURES 𝒞 S)
SIP {𝒞 = 𝒞} {{𝒞-cat}} {{𝒞-univ}} S {{S-univ}} .univ (x , α) (y , β) = isoToIsEquiv (iso (pathToIso (x , α) (y , β)) catisoToPath sect ret)
  where
    catisoToPath : ∀ {x y : 𝒞 .ob} {α : S .Struct x} {β : S .Struct y} → CatIso (STRUCTURES 𝒞 S) (x , α) (y , β) → (x , α) ≡ (y , β)
    catisoToPath {x = x} {y} {α} {β} (catiso (f , hᶠ) (g , hᵍ) sec ret) = ΣPathTransport→PathΣ _ _ (x≡y , α≡β x≡y α β (subst (S .IsHomo α β) f≡h hᶠ) (subst (S .IsHomo β α) g≡h⁻¹ hᵍ))
      where
        x≅y : CatIso 𝒞 x y
        x≅y = catiso f g (cong fst sec) (cong fst ret)

        x≡y : x ≡ y
        x≡y = uva 𝒞-univ x≅y

        f≡h : f ≡ pathMor 𝒞 x≡y
        f≡h = sym (uvaPathMor 𝒞-univ x≅y)

        g≡h⁻¹ : g ≡ pathMor⁻ 𝒞 x≡y
        g≡h⁻¹ = sym (uvaPathMor⁻ 𝒞-univ x≅y)

        α≡β : ∀ {x y : 𝒞 .ob} (p : x ≡ y)
                (α : S .Struct x) (β : S .Struct y)
                (h⇒ : S .IsHomo α β (pathMor 𝒞 p)) (h⇐ : S .IsHomo β α (pathMor⁻ 𝒞 p))
                → subst (S .Struct) p α ≡ β
        α≡β {x} {y} =
          J (λ z q → ∀ (α : S .Struct x) (β : S .Struct z) (h⇒ : S .IsHomo α β (pathMor 𝒞 q)) (h⇐ : S .IsHomo β α (pathMor⁻ 𝒞 q)) → subst (S .Struct) q α ≡ β)
          (λ α β h⇒ h⇐ → transportRefl α ∙ subAntisym S-univ (subst (S .IsHomo α β) (pathMorRefl {𝒞 = 𝒞}) h⇒) (subst (S .IsHomo β α) (pathMor⁻Refl {𝒞 = 𝒞}) h⇐))

    sect : section (pathToIso (x , α) (y , β)) catisoToPath
    sect (catiso h h⁻¹ sec ret) = {!   !}

    ret : retract (pathToIso (x , α) (y , β)) catisoToPath
    ret = J (λ z q → catisoToPath (pathToIso (x , α) z q) ≡ q)
      (subst {y = (pathToIso (x , α) (x , α) refl)} (λ x → catisoToPath x ≡ refl) (sym (JRefl (λ z _ → (x , α) ≅ z) ?)))

ext: agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The reader monad
------------------------------------------------------------------------

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

open import Level

module Category.Monad.Reader {r} (R : Set r) (a : Level) where

open import Function
open import Function.Identity.Categorical as Id using (Identity)
open import Category.Applicative.Indexed
open import Category.Monad.Indexed
open import Category.Monad
open import Data.Unit

private
  variable
    ℓ : Level
    A B I : Set ℓ

------------------------------------------------------------------------
-- Indexed reader

IReaderT : IFun I (r ⊔ a) → IFun I (r ⊔ a)
IReaderT M i j A = R → M i j A

module _ {M : IFun I (r ⊔ a)} where

  ------------------------------------------------------------------------
  -- Indexed reader applicative

  ReaderTIApplicative : RawIApplicative M → RawIApplicative (IReaderT M)
  ReaderTIApplicative App = record
    { pure = λ x r → pure x
    ; _⊛_ = λ m n r → m r ⊛ n r
    } where open RawIApplicative App

  ReaderTIApplicativeZero : RawIApplicativeZero M →
                            RawIApplicativeZero (IReaderT M)
  ReaderTIApplicativeZero App = record
    { applicative = ReaderTIApplicative applicative
    ; ∅ = const ∅
    } where open RawIApplicativeZero App

  ReaderTIAlternative : RawIAlternative M → RawIAlternative (IReaderT M)
  ReaderTIAlternative Alt = record
    { applicativeZero = ReaderTIApplicativeZero applicativeZero
    ; _∣_ = λ m n r → m r ∣ n r
    } where open RawIAlternative Alt

  ------------------------------------------------------------------------
  -- Indexed reader monad

  ReaderTIMonad : RawIMonad M → RawIMonad (IReaderT M)
  ReaderTIMonad Mon = record
    { return = λ x r → return x
    ; _>>=_ = λ m f r → m r >>= flip f r
    } where open RawIMonad Mon

  ReaderTIMonadZero : RawIMonadZero M → RawIMonadZero (IReaderT M)
  ReaderTIMonadZero Mon = record
    { monad = ReaderTIMonad monad
    ; applicativeZero = ReaderTIApplicativeZero applicativeZero
    } where open RawIMonadZero Mon

  ReaderTIMonadPlus : RawIMonadPlus M → RawIMonadPlus (IReaderT M)
  ReaderTIMonadPlus Mon = record
    { monad = ReaderTIMonad monad
    ; alternative = ReaderTIAlternative alternative
    } where open RawIMonadPlus Mon

------------------------------------------------------------------------
-- Reader monad operations

record RawIMonadReader {I : Set ℓ} (M : IFun I (r ⊔ a))
                       : Set (ℓ ⊔ suc (r ⊔ a)) where
  field
    monad  : RawIMonad M
    reader : ∀ {i} → (R → A) → M i i A
    local  : ∀ {i j} → (R → R) → M i j A → M i j A

  open RawIMonad monad public

  ask : ∀ {i} → M i i (Lift (r ⊔ a) R)
  ask = reader lift

  asks : ∀ {i} → (R → A) → M i i A
  asks = reader

ReaderTIMonadReader : {I : Set ℓ} {M : IFun I (r ⊔ a)} →
                      RawIMonad M → RawIMonadReader (IReaderT M)
ReaderTIMonadReader Mon = record
  { monad = ReaderTIMonad Mon
  ; reader = λ f r → return (f r)
  ; local = λ f m → m ∘ f
  } where open RawIMonad Mon

------------------------------------------------------------------------
-- Ordinary reader monads

RawMonadReader : (M : Set (r ⊔ a) → Set (r ⊔ a)) → Set _
RawMonadReader M = RawIMonadReader {I = ⊤} (λ _ _ → M)

module RawMonadReader {M} (Mon : RawMonadReader M) where
  open RawIMonadReader Mon public

ReaderT : (M : Set (r ⊔ a) → Set (r ⊔ a)) → Set _ → Set _
ReaderT M = IReaderT {I = ⊤} (λ _ _ → M) _ _

ReaderTMonad : ∀ {M} → RawMonad M → RawMonad (ReaderT M)
ReaderTMonad = ReaderTIMonad

ReaderTMonadReader : ∀ {M} → RawMonad M → RawMonadReader (ReaderT M)
ReaderTMonadReader = ReaderTIMonadReader

ReaderTMonadZero : ∀ {M} → RawMonadZero M → RawMonadZero (ReaderT M)
ReaderTMonadZero = ReaderTIMonadZero

ReaderTMonadPlus : ∀ {M} → RawMonadPlus M → RawMonadPlus (ReaderT M)
ReaderTMonadPlus = ReaderTIMonadPlus

Reader : Set (r ⊔ a) → Set (r ⊔ a)
Reader = ReaderT Identity

ReaderMonad : RawMonad Reader
ReaderMonad = ReaderTIMonad Id.monad

ReaderMonadReader : RawMonadReader Reader
ReaderMonadReader = ReaderTIMonadReader Id.monad


text:
module Data.Real.Diff where

open import Level using (0ℓ)
import Data.Real as ℝ
open ℝ using (ℝ)
open import Data.Real.Properties

import Data.Nat as ℕ
open ℕ using (ℕ; suc; zero; _⊓_; _⊔_)

open import Data.Unit.Polymorphic using (tt; ⊤)
open import Data.Product using (_×_; _,_; proj₁; proj₂)

open import Function using (_∘_; id)

-- TODO should move to _≈_ at some point
open import Relation.Binary.PropositionalEquality hiding ([_])
open ≡-Reasoning

import Data.Vec as V
open V using (Vec; []; _∷_)

import Data.Vec.Recursive as VR
open VR using (_^_; 2+_)

open import Data.Fin using (Fin; zero; suc)

Tower : ℕ → Set
Tower = Vec ℝ

Diff : Set
Diff = ∀ {d n} → Tower d ^ n → Tower d ^ n

Diff2 : Set
Diff2 = ∀ {d n} → Tower d ^ n → Tower d ^ n → Tower d ^ n

-- utility function
infix 2 _!_
_!_ : ∀ {n} → (∀ {d'} → Tower d' ^ n) → ∀ d → Tower d ^ n
x ! d = x {d}

lift : ∀ {n a} {A : Set a} → A → A ^ n
lift {n} x = VR.replicate n x

const' : ∀ {d} → ℝ → Tower d
const' {zero} x = []
const' {suc d} x = x ∷ (const' 0.0)

const : ∀ {n d} → ℝ ^ n → Tower d ^ n
const {n} = VR.map const' n

return' : ∀ {d} → ℝ → Tower (suc d)
return' x = x ∷ const' 1.0

return : ∀ {n d} → ℝ ^ n → Tower (suc d) ^ n
return {n} = VR.map return' n

extract : ∀ {d n} → Tower (suc d) ^ n → ℝ ^ n
extract {n = n} = VR.map V.head n

lop : ∀ {d} → Tower (suc d) → Tower d
lop {zero} _ = []
lop {suc d} (x ∷ xs) = x ∷ lop xs

run : ∀ {m n} (f : Tower 1 ^ m → Tower 1 ^ n) (x : ℝ ^ m) → ℝ ^ n
run f = extract ∘ f ∘ const

-_ : Diff
-_ {n = n} = VR.map (V.map λ x → ℝ.- x) n

infixl 6 _+_ _-_
infixr 9 -_
_+_ _-_ : Diff2
_+_ {n = n} = VR.zipWith (V.zipWith ℝ._+_) n
x - y = x + (- y)

*T : ∀ {d} (x y : Tower d) → Tower d
*T [] _ = []
*T xx@(x ∷ xs) yy@(y ∷ ys) = x ℝ.* y ∷ *T (lop xx) ys + *T (lop yy) xs

infixl 7 _*_
_*_ : Diff2
_*_ {zero} {n} x _ = x
_*_ {suc d} {n} = VR.zipWith *T n

-- directional derivative
du
  : ∀ {m n} (f : Tower 2 ^ m → Tower 2 ^ n)
  → Tower 2 ^ m → Tower 1 ^ n
du {n = n} f xs = VR.map V.tail n (f xs)

fins : ∀ n → Fin n ^ n
fins n = VR.tabulate n id

directions : ∀ {d n} → ℝ ^ n → (Tower (suc d) ^ n) ^ n
directions {d} {n} x = VR.map (λ i → go i x) n (fins n)
  where
    go : ∀ {m} → Fin m → ℝ ^ m → Tower (suc d) ^ m
    go {1} zero y = return y
    go {2+ m} zero (y , ys) = return y , const ys
    go {2+ m} (suc i) (y , ys) = const y , go i ys

outerWith
  : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
  → (f : A → B → C) → ∀ m n → A ^ m → B ^ n → (C ^ n) ^ m
outerWith f m n rm rn = VR.map (λ x → VR.map (f x) n rn) m rm

-- this is all very likely very slow
-- it's running `du` `m` times...
jacobian grad : ∀ {m n} (f : Tower 2 ^ m → Tower 2 ^ n) → ℝ ^ m → (ℝ ^ n) ^ m
jacobian {m = m} f x = VR.map (extract ∘ du f) m (directions x)
grad = jacobian

-- TODO
-- The second derivative cross terms are not currently clear to me.
-- directions2d : ∀ {d n} → ℝ ^ n → ((Tower (suc d) ^ n) ^ n) ^ n
-- directions2d {d} {n} x = rotations n dirs
--   -- VR.zipWith (λ y ys → {!   !}) n (dirs) (rotations dirs)
--   where
--     dirs : (Tower (suc d) ^ n) ^ n
--     dirs = directions x

--     rotations : ∀ m → (Tower (suc d) ^ m) ^ m → ((Tower (suc d) ^ m) ^ m) ^ m
--     rotations = {!   !}

-- d2u
--   : ∀ {m n} (f : Tower 3 ^ m → Tower 3 ^ n)
--   → Tower 3 ^ m → Tower 1 ^ n
-- d2u {n = n} f xs = VR.map (V.tail ∘ V.tail) n (f xs)

-- hessian
--   : ∀ {m n} (f : Tower 3 ^ m  → Tower 3 ^ n)
--   → ℝ ^ m → ((ℝ ^ n) ^ m) ^ m
-- hessian {m} {n} f x =
--   VR.map (λ dir → VR.map (extract ∘ d2u f) m dir) m (directions2d x)
  -- outerWith (λ y z → extract (du (du f) y)) m m (directions x) (directions x)

_>-<_ : (ℝ → ℝ) → (∀ {d'} → Tower d' → Tower d') → ∀ {d} → Tower d → Tower d
(f >-< g) {zero} [] = []
(f >-< g) {suc d} xx@(x ∷ xs) = f x ∷ xs * g (lop xx)

liftF : ∀ {d} (f : Tower d → Tower d) → ∀ {n} → Tower d ^ n → Tower d ^ n
liftF f {n} = VR.map f n

infixl 8 _^^_
_^^_ : ∀ {d n} → Tower d ^ n → (m : ℕ) → Tower d ^ n
x ^^ zero = lift (const 1.0)
x ^^ (suc d) = x * x ^^ d

module Single where
  infixr 9 e^_
  e^_ log recip sin cos sinh cosh abs sgn : ∀ {d} → Tower d → Tower d

  e^ [] = []
  e^_ {suc d} xx@(x ∷ xs) = ℝ.e^ x ∷ xs * (e^ lop xx)

  log = ℝ.log >-< recip

  recip [] = []
  recip xx@(x ∷ xs) = 1/x ∷ 1/xx
    where
      1/x = 1.0 ℝ.÷ x
      1/xx = recip (lop xx)

  abs = ℝ.abs >-< sgn

  sgn [] = []
  sgn (x ∷ xs) = if does (0.0 ≤? x) then const 1.0 else const (ℝ.- 1.0)
    where
      open import Data.Bool using (if_then_else_)
      open import Data.Real.Order
      open import Relation.Nullary

  -- I'm not sure why I have to write these by hand.
  sin [] = []
  sin xx@(x ∷ xs) = ℝ.sin x ∷ xs * cos (lop xx)

  cos [] = []
  cos xx@(x ∷ xs) = ℝ.cos x ∷ - xs * sin (lop xx)

  sinh [] = []
  sinh xx@(x ∷ xs) = ℝ.sinh x ∷ xs * cosh (lop xx)

  cosh [] = []
  cosh xx@(x ∷ xs) = ℝ.cosh x ∷ xs * sinh (lop xx)

infixr 9 e^_
e^_ log recip sin cos sinh cosh abs sgn : Diff
e^_ = liftF Single.e^_
log = liftF Single.log
recip = liftF Single.recip
abs = liftF Single.abs
sgn = liftF Single.sgn
sin = liftF Single.sin
cos = liftF Single.cos
sinh = liftF Single.sinh
cosh = liftF Single.cosh

infix 8 _**_
_**_ : Diff2
x ** y = e^ (y * log x)

ascend descend
  : ∀ {n} (f : Tower 2 ^ n → Tower 2) (δ : ℝ ^ n) (m : ℕ) (x : ℝ ^ n) → ℝ ^ n
ascend f δ zero x = x
ascend {n = n} f δ (suc m) x = ascend f δ m (add x (mul δ (grad f x)))
  where
    add mul : (x y : ℝ ^ n) → ℝ ^ n
    add = VR.zipWith ℝ._+_ n
    mul = VR.zipWith ℝ._*_ n

descend f = ascend λ x → - f x

ascend_f=_δ=_steps=_start=_
  : ∀ {n} (_ : ⊤ {0ℓ}) (f : Tower 2 ^ n → Tower 2) (δ : ℝ ^ n) (m : ℕ) (x : ℝ ^ n) → ℝ ^ n
ascend_f=_δ=_steps=_start=_ _ = ascend

∶ : ⊤ {0ℓ}
∶ = _

sterling : ℕ → ℝ
sterling n = n' ℝ.* ℝ.log n' ℝ.- n'
  where
    n' = ℝ.fromℕ n

logPoisson' logPoisson : ∀ {n} → ℕ ^ n → ∀ {d} → Tower d ^ n → Tower d ^ n

-- neglecting the normalization term
logPoisson' {n} k α = const k' * log α - α
  where
    k' = VR.map ℝ.fromℕ n k

logPoisson {n} k α = logPoisson' k α - const (VR.map sterling n k)

sum : ∀ {d n} → Tower d ^ n → Tower d
sum {d} {n} = VR.foldl (λ _ → Tower d) (const 0.0) id (λ _ x y → x + y) n
  where open import Function using (id)

binned : ∀ {d n} → ℕ ^ n → Tower d ^ n → Tower d
binned n = sum ∘ logPoisson' n

test : ∀ {n} → ℝ ^ n → ℝ ^ n
test x =
  ascend ∶
    f= binned (lift 10)
    δ= lift 1.0
    steps= 1000
    start= x

testgrad : ∀ {n} → ℝ ^ n → ℝ ^ n
testgrad = grad (binned (lift 10))

max_stars_repo_name: cspollard/diff

max_issues_repo_name: cspollard/diff

max_forks_repo_name: cspollard/diff


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Sets of variables
------------------------------------------------------------------------

module Base.Syntax.Vars
     (Type : Set)
  where

-- The notion of sets of variables
--
-- This module is calculus-independent.

open import Base.Syntax.Context Type

open import Relation.Binary.PropositionalEquality
open import Data.Unit
open import Data.Sum
open import Data.Bool

-- Sets of variables

open import Base.Data.DependentList

Free : Type → Set
Free _ = Bool

Vars : Context → Set
Vars = DependentList Free

none : {Γ : Context} → Vars Γ
none = tabulate (λ _ → false)

singleton : ∀ {τ Γ} → Var Γ τ → Vars Γ
singleton {Γ = τ • Γ₀} this = true • none
singleton (that x) = false • singleton x

-- Union of variable sets
infixl 6 _∪_ -- just like _+_
_∪_ : ∀ {Γ} → Vars Γ → Vars Γ → Vars Γ
_∪_ = zipWith _∨_

-- Test if a set of variables is empty
empty? : ∀ {Γ} → (vs : Vars Γ) → (vs ≡ none) ⊎ ⊤
empty? ∅ = inj₁ refl
empty? (true • vs) = inj₂ tt
empty? (false • vs) with empty? vs
... | inj₁ vs=∅ = inj₁ (cong₂ _•_ refl vs=∅)
... | inj₂ _ = inj₂ tt

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

module Inspect where

open import Level
open import Path

record Reveal_·_is_ {A : Type a} {B : A → Type b} (f : (x : A) → B x) (x : A) (y : B x) : Type b where
  constructor 〖_〗
  field eq : f x ≡ y

inspect : {A : Type a} {B : A → Type b} (f : (x : A) → B x) (x : A) → Reveal f · x is f x
inspect f x = 〖 refl 〗

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
open import Prelude

module Implicits.Resolution.Deterministic.Expressiveness where

open import Data.Fin.Substitution
open import Implicits.Syntax
open import Implicits.Syntax.Type.Unification
open import Implicits.Resolution.Ambiguous.Resolution as A
open import Implicits.Resolution.Deterministic.Resolution as D
open import Extensions.ListFirst

module Deterministic⊆Ambiguous where
  open FirstLemmas
  open import Relation.Unary

  soundness : ∀ {ν} {Δ : ICtx ν} {r} → Δ D.⊢ᵣ r → Δ A.⊢ᵣ r
  soundness (r-simp r x) = lem x (r-ivar (proj₁ $ first⟶∈ r))
    where
      lem : ∀ {ν} {a τ} {Δ : ICtx ν} → Δ ⊢ a ↓ τ → Δ A.⊢ᵣ a → Δ A.⊢ᵣ simpl τ
      lem (i-simp τ) hyp = hyp
      lem (i-iabs ih₁ ih₂) hyp = lem ih₂ (r-iapp hyp (soundness ih₁))
      lem (i-tabs b ih) hyp = lem ih (r-tapp b hyp)
  soundness (r-iabs _ ih) = r-iabs (soundness ih)
  soundness (r-tabs ih) = r-tabs (soundness ih)


text:
{-# OPTIONS --universe-polymorphism #-}
open import Common.Prelude
  renaming (Nat to ℕ; module Nat to ℕ)
   using (zero; suc; _+_; _∸_; List; []; _∷_; Bool; true; false)
open import Common.Level
open import Common.Reflect

module TermSplicing where

module Library where
  data Box {a} (A : Set a) : Set a where
    box : A → Box A

  record ⊤ : Set where
    constructor tt

  infixr 5 _×_
  record _×_ (A B : Set) : Set where
    constructor _,_
    field
      proj₁ : A
      proj₂ : B

  [_] : ∀ {A : Set} → A → List A
  [ x ] = x ∷ []

  replicate : ∀ {A : Set} → ℕ → A → List A
  replicate zero x = []
  replicate (suc n) x = x ∷ replicate n x

  foldr : ∀ {A B : Set} → (A → B → B) → B → List A → B
  foldr c n []       = n
  foldr c n (x ∷ xs) = c x (foldr c n xs)

  foldl : ∀ {A B : Set} → (A → B → A) → A → List B → A
  foldl c n []       = n
  foldl c n (x ∷ xs) = foldl c (c n x) xs

  reverse : ∀ {A : Set} → List A → List A
  reverse = foldl (λ rev x → x ∷ rev) []

  length : ∀ {A : Set} → List A → ℕ
  length = foldr (λ _ → suc) 0

  data Maybe (A : Set) : Set where
    nothing : Maybe A
    just    : A → Maybe A

  mapMaybe : ∀ {A B : Set} → (A → B) → Maybe A → Maybe B
  mapMaybe f (just x) = just (f x)
  mapMaybe f nothing  = nothing

  when : ∀ {A} → Bool → Maybe A → Maybe A
  when true  x = x
  when false _ = nothing

  data _≡_ {a} {A : Set a} (x : A) : A -> Set where
    refl : x ≡ x

  _→⟨_⟩_ : ∀ (A : Set) (n : ℕ) (B : Set) → Set
  A →⟨ zero  ⟩ B = B
  A →⟨ suc n ⟩ B = A → A →⟨ n ⟩ B

open Library

module ReflectLibrary where
  lamᵛ : Term → Term
  lamᵛ = lam visible

  lamʰ : Term → Term
  lamʰ = lam hidden

  argᵛʳ : ∀{A} → A → Arg A
  argᵛʳ = arg (arginfo visible relevant)

  argʰʳ : ∀{A} → A → Arg A
  argʰʳ = arg (arginfo hidden relevant)

  app` : (Args → Term) → (hrs : List ArgInfo) → Term →⟨ length hrs ⟩ Term
  app` f = go [] where
    go : List (Arg Term) → (hrs : List ArgInfo) → Term →⟨ length hrs ⟩ Term
    go args []             = f (reverse args)
    go args (i ∷ hs) = λ t → go (arg i t ∷ args) hs

  con` : QName → (hrs : List ArgInfo) → Term →⟨ length hrs ⟩ Term
  con` x = app` (con x)

  def` : QName → (hrs : List ArgInfo) → Term →⟨ length hrs ⟩ Term
  def` x = app` (def x)

  var` : ℕ → (hrs : List ArgInfo) → Term →⟨ length hrs ⟩ Term
  var` x = app` (var x)

  coe : ∀ {A : Set} {z : A} n → (Term →⟨ length (replicate n z) ⟩ Term) → Term →⟨ n ⟩ Term
  coe zero    t = t
  coe (suc n) f = λ t → coe n (f t)

  con`ⁿʳ : QName → (n : ℕ) → Term →⟨ n ⟩ Term
  con`ⁿʳ x n = coe n (app` (con x) (replicate n (arginfo visible relevant)))

  def`ⁿʳ : QName → (n : ℕ) → Term →⟨ n ⟩ Term
  def`ⁿʳ x n = coe n (app` (def x) (replicate n (arginfo visible relevant)))

  var`ⁿʳ : ℕ → (n : ℕ) → Term →⟨ n ⟩ Term
  var`ⁿʳ x n = coe n (app` (var x) (replicate n (arginfo visible relevant)))

  sort₀ : Sort
  sort₀ = lit 0

  sort₁ : Sort
  sort₁ = lit 1

  `Set₀ : Term
  `Set₀ = sort sort₀

  el₀ : Term → Type
  el₀ = el sort₀

  -- Builds a type variable (of type Set₀)
  ``var₀ : ℕ → Args → Type
  ``var₀ n args = el₀ (var n args)

  ``Set₀ : Type
  ``Set₀ = el sort₁ `Set₀

  unEl : Type → Term
  unEl (el _ tm) = tm

  getSort : Type → Sort
  getSort (el s _) = s

  unArg : ∀ {A} → Arg A → A
  unArg (arg _ a) = a

  `Level : Term
  `Level = def (quote Level) []

  ``Level : Type
  ``Level = el₀ `Level

  `sucLevel : Term → Term
  `sucLevel = def`ⁿʳ (quote lsuc) 1

  sucSort : Sort → Sort
  sucSort s = set (`sucLevel (sort s))

  ℕ→Level : ℕ → Level
  ℕ→Level zero    = lzero
  ℕ→Level (suc n) = lsuc (ℕ→Level n)

  -- Can't match on Levels anymore
--   Level→ℕ : Level → ℕ
--   Level→ℕ zero    = zero
--   Level→ℕ (suc n) = suc (Level→ℕ n)

  setLevel : Level → Sort
  setLevel ℓ = lit 0 -- (Level→ℕ ℓ)

  _==_ : QName → QName → Bool
  _==_ = primQNameEquality

  decodeSort : Sort → Maybe Level
  decodeSort (set (con c [])) = when (quote lzero == c) (just lzero)
  decodeSort (set (con c (arg (arginfo visible relevant) s ∷ [])))
    = when (quote lsuc == c) (mapMaybe lsuc (decodeSort (set s)))
  decodeSort (set (sort s)) = decodeSort s
  decodeSort (set _) = nothing
  decodeSort (lit n) = just (ℕ→Level n)
  decodeSort unknown = nothing

  _`⊔`_ : Sort → Sort → Sort
  s₁ `⊔` s₂ with decodeSort s₁ | decodeSort s₂
  ...          | just n₁       | just n₂        = setLevel (n₁ ⊔ n₂)
  ...          | _             | _              = set (def (quote _⊔_) (argᵛʳ (sort s₁) ∷ argᵛʳ (sort s₂) ∷ []))

  Π : Arg Type → Type → Type
  Π t u = el (getSort (unArg t) `⊔` getSort u) (pi t u)

  Πᵛʳ : Type → Type → Type
  Πᵛʳ t u = el (getSort t `⊔` getSort u) (pi (arg (arginfo visible relevant) t) u)

  Πʰʳ : Type → Type → Type
  Πʰʳ t u = el (getSort t `⊔` getSort u) (pi (arg (arginfo hidden relevant) t) u)

open ReflectLibrary

`ℕ : Term
`ℕ = def (quote ℕ) []

`ℕOk : (unquote `ℕ) ≡ ℕ
`ℕOk = refl

``ℕ : Type
``ℕ = el₀ `ℕ

idℕ : ℕ → ℕ
idℕ = unquote (lamᵛ (var 0 []))

id : (A : Set) → A → A
id = unquote (lamᵛ (lamᵛ (var 0 [])))

idBox : Box ({A : Set} → A → A)
idBox = box (unquote (lamᵛ (var 0 [])))

-- builds a pair
_`,_ : Term → Term → Term
_`,_ = con`ⁿʳ (quote _,_) 2

`tt : Term
`tt = con (quote tt) []

tuple : List Term → Term
tuple = foldr _`,_ `tt

`refl : Term
`refl = con (quote refl) []

`zero : Term
`zero = con (quote ℕ.zero) []

`[] : Term
`[] = con (quote []) []

_`∷_ : (`x `xs : Term) → Term
_`∷_ = con`ⁿʳ (quote _∷_) 2

`var : (`n `args : Term) → Term
`var = con`ⁿʳ (quote var) 2

`lam : (`hiding `args : Term) → Term
`lam = con`ⁿʳ (quote lam) 2

`visible : Term
`visible = con (quote visible) []

`hidden : Term
`hidden = con (quote hidden) []

`[_`] : Term → Term
`[ x `] = x `∷ `[]

quotedTwice : Term
quotedTwice = `lam `visible (`var `zero `[])

unquoteTwice₂ : ℕ → ℕ
unquoteTwice₂ = unquote (unquote quotedTwice)

unquoteTwice : ℕ → ℕ
unquoteTwice x = unquote (unquote (`var `zero `[]))

id₂ : {A : Set} → A → A
id₂ = unquote (lamᵛ (var 0 []))

id₃ : {A : Set} → A → A
id₃ x = unquote (var 0 [])

module Id {A : Set} (x : A) where
  x′ : A
  x′ = unquote (var 0 [])

k`ℕ : ℕ → Term
k`ℕ zero    = `ℕ
k`ℕ (suc n) = unquote (def (quote k`ℕ) [ argᵛʳ (var 0 []) ]) -- k`ℕ n

test : id ≡ (λ A (x : A) → x)
     × unquote `Set₀                      ≡ Set
     × unquote `ℕ                         ≡ ℕ
     × unquote (lamᵛ (var 0 []))          ≡ (λ (x : Set) → x)
     × id                                 ≡ (λ A (x : A) → x)
     × unquote `tt                        ≡ tt
     × (λ {A} → Id.x′ {A})                ≡ (λ {A : Set} (x : A) → x)
     × unquote (pi (argᵛʳ ``Set₀) ``Set₀)  ≡ (Set → Set)
     × unquoteTwice                        ≡ (λ (x : ℕ) → x)
     × unquote (k`ℕ 42)                    ≡ ℕ
     × ⊤
test = unquote (tuple (replicate n `refl)) where n = 10

Πⁿ : ℕ → Type → Type
Πⁿ zero    t = t
Πⁿ (suc n) t = Π (argʰʳ ``Set₀) (Πⁿ n t)

ƛⁿ : Hiding → ℕ → Term → Term
ƛⁿ h zero    t = t
ƛⁿ h (suc n) t = lam h (ƛⁿ h n t)

-- projᵢ : Proj i n
-- projᵢ = proj i n
-- Projᵢ = {A₁ ... Ai ... An : Set} → A₁ → ... → Aᵢ → ... → An → Aᵢ
-- projᵢ = λ {A₁ ... Ai ... An} x₁ ... xᵢ ... xn → xᵢ

Proj : (i n : ℕ) → Term
Proj i n = unEl (Πⁿ n (go n)) where
  n∸1 = n ∸ 1
  go : ℕ → Type
  go zero    = ``var₀ ((n + n) ∸ i) []
  go (suc m) = Π (argᵛʳ (``var₀ n∸1 [])) (go m)

proj : (i n : ℕ) → Term
proj i n = ƛⁿ visible n (var (n ∸ i) [])

projFull : (i n : ℕ) → Term
projFull i n = ƛⁿ hidden n (proj i n)

ℕ→ℕ : Set
ℕ→ℕ = unquote (unEl (Π (argᵛʳ ``ℕ) ``ℕ))

ℕ→ℕOk : ℕ→ℕ ≡ (ℕ → ℕ)
ℕ→ℕOk = refl

``∀A→A : Type
``∀A→A = Π (argᵛʳ ``Set₀) (``var₀ 0 [])

∀A→A : Set₁
∀A→A = unquote (unEl ``∀A→A)

Proj₁¹ : Set₁
Proj₁¹ = unquote (Proj 1 1)

Proj₁² : Set₁
Proj₁² = unquote (Proj 1 2)

Proj₂² : Set₁
Proj₂² = unquote (Proj 2 2)

proj₃⁵ : unquote (Proj 3 5)
proj₃⁵ _ _ x _ _ = x

proj₃⁵′ : Box (unquote (Proj 3 5))
proj₃⁵′ = box (unquote (proj 3 5))

proj₂⁷ : unquote (Proj 2 7)
proj₂⁷ = unquote (proj 2 7)

test-proj : proj₃⁵′                ≡ box (λ _ _ x _ _ → x)
          × Proj₁¹                 ≡ ({A : Set} → A → A)
          × Proj₁²                 ≡ ({A₁ A₂ : Set} → A₁ → A₂ → A₁)
          × Proj₂²                 ≡ ({A₁ A₂ : Set} → A₁ → A₂ → A₂)
          × unquote (Proj 3 5)     ≡ ({A₁ A₂ A₃ A₄ A₅ : Set} → A₁ → A₂ → A₃ → A₄ → A₅ → A₃)
          × unquote (projFull 1 1) ≡ (λ {A : Set} (x : A) → x)
          × unquote (projFull 1 2) ≡ (λ {A₁ A₂ : Set} (x₁ : A₁) (x₂ : A₂) → x₁)
          × unquote (projFull 2 2) ≡ (λ {A₁ A₂ : Set} (x₁ : A₁) (x₂ : A₂) → x₂)
          × ∀A→A                   ≡ (∀ (A : Set) → A)
          × ⊤
test-proj = unquote (tuple (replicate n `refl)) where n = 9

module Test where
  data Squash (A : Set) : Set where
    squash : unquote (unEl (Π (arg (arginfo visible irrelevant) (``var₀ 0 [])) (el₀ (def (quote Squash) (argᵛʳ (var 1 []) ∷ [])))))

data Squash (A : Set) : Set where
  squash : .A → Squash A

`Squash : Term → Term
`Squash = def`ⁿʳ (quote Squash) 1

squash-type : Type
squash-type = Π (arg (arginfo visible irrelevant) (``var₀ 0 [])) (el₀ (`Squash (var 1 [])))

test-squash : ∀ {A} → (.A → Squash A) ≡ unquote (unEl squash-type)
test-squash = refl

`∀ℓ→Setℓ : Type
`∀ℓ→Setℓ = Πᵛʳ ``Level (el₀ (sort (set (var 0 []))))

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module BHeap {A : Set}(_≤_ : A → A → Set) where

open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import BTree {A} hiding (flatten)
open import Data.Nat hiding (_≤_)
open import Data.List
open import Data.Sum renaming (_⊎_ to _∨_)
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality hiding (trans)

open DecTotalOrder decTotalOrder hiding (refl ; _≤_)

data BHeap : Bound → Set where
  lf : {b : Bound}
                   → BHeap b
  nd : {b : Bound}{x : A}
                   → LeB b (val x)
                   → (l r : BHeap (val x))
                   → BHeap b

forget : {b : Bound} → BHeap b → BTree
forget lf = leaf
forget (nd {x = x} _ l r) = node x (forget l) (forget r)

# : {b : Bound} → BHeap b → ℕ
# lf = zero
# (nd _ l r) = suc (# l + # r)

height : {b : Bound} → BHeap b → ℕ
height lf = zero
height (nd _ l r)
    with total (height l) (height r)
... | inj₁ hl≤hr = suc (height r)
... | inj₂ hr≤hl = suc (height l)

merge : {b : Bound} → Total _≤_ → (l r : BHeap b) → BHeap b
merge _ lf r = r
merge _ l lf = l
merge tot≤ (nd {x = x} b≤x l r) (nd {x = x'} b≤x' l' r')
    with tot≤ x x'
... | inj₁ x≤x' = nd b≤x (merge tot≤ l r) (nd (lexy x≤x') l' r')
... | inj₂ x'≤x = nd b≤x' (nd (lexy x'≤x) l r) (merge tot≤ l' r')

flatten : {b : Bound}(h : BHeap b) → List A
flatten lf = []
flatten (nd {x = x} b≤x l r) = x ∷ (flatten l ++ flatten r)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
open import SingleSorted.AlgebraicTheory

import SingleSorted.Interpretation as Interpretation
import SingleSorted.SyntacticCategory as SyntacticCategory
import SingleSorted.Substitution as Substitution

module SingleSorted.UniversalInterpretation
  {ℓt}
  {Σ : Signature}
  (T : Theory ℓt Σ) where

  open Theory T
  open Substitution T
  open SyntacticCategory T

  -- The universal interpretation in the syntactic category
  ℐ : Interpretation.Interpretation Σ cartesian-𝒮
  ℐ =
    record
     { interp-carrier = ctx-slot
     ; interp-pow = power-𝒮
     ; interp-oper = λ f var-var → tm-oper f (λ i → tm-var i)
     }

  open Interpretation.Interpretation ℐ

  -- A term is essentially interpreted by itself
  interp-term-self : ∀ {Γ} (t : Term Γ) y → Γ ⊢ interp-term t y ≈ t
  interp-term-self (tm-var x) _ = eq-refl
  interp-term-self (tm-oper f xs) y = eq-congr (λ i → interp-term-self (xs i) var-var)

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.Equality

macro
  macro₁ : Term -> TC ⊤
  macro₁ goal = do
    u   ← quoteTC ((1 + 2) - 3)
    u'  ← onlyReduceDefs (quote _+_ ∷ []) (normalise u)
    qu' ← quoteTC u'
    unify qu' goal

test₁ : macro₁ ≡ def (quote _-_)
                   (arg (arg-info visible relevant) (lit (nat 3)) ∷
                    arg (arg-info visible relevant) (lit (nat 3)) ∷ [])
test₁ = refl

macro
  macro₂ : Term -> TC ⊤
  macro₂ goal = do
    u   ← quoteTC ((1 - 2) + 3)
    u'  ← dontReduceDefs (quote _+_ ∷ []) (normalise u)
    qu' ← quoteTC u'
    unify qu' goal

test₂ : macro₂ ≡ def (quote _+_)
                   (arg (arg-info visible relevant) (lit (nat 0)) ∷
                    arg (arg-info visible relevant) (lit (nat 3)) ∷ [])
test₂ = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Homomorphism proofs for variables and constants over polynomials
------------------------------------------------------------------------

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

open import Tactic.RingSolver.Core.Polynomial.Parameters

module Tactic.RingSolver.Core.Polynomial.Homomorphism.Variables
  {r₁ r₂ r₃ r₄}
  (homo : Homomorphism r₁ r₂ r₃ r₄)
  where

open import Data.Product        using (_,_)
open import Data.Vec.Base as Vec     using (Vec)
open import Data.Fin            using (Fin)
open import Data.List.Kleene

open Homomorphism homo

open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas homo
open import Tactic.RingSolver.Core.Polynomial.Base (Homomorphism.from homo)
open import Tactic.RingSolver.Core.Polynomial.Reasoning (Homomorphism.to homo)
open import Tactic.RingSolver.Core.Polynomial.Semantics homo

open import Algebra.Operations.Ring rawRing

ι-hom : ∀ {n} (i : Fin n) (Ρ : Vec Carrier n) → ⟦ ι i ⟧ Ρ ≈ Vec.lookup Ρ i
ι-hom i Ρ′ = let (ρ , Ρ) = drop-1 (space≤′n i) Ρ′ in begin
  ⟦ (κ Raw.1# Δ 1 ∷↓ []) ⊐↓ space≤′n i ⟧ Ρ′  ≈⟨ ⊐↓-hom (κ Raw.1# Δ 1 ∷↓ []) (space≤′n i) Ρ′ ⟩
  ⅀?⟦ κ Raw.1# Δ 1 ∷↓ [] ⟧ (ρ , Ρ)           ≈⟨ ∷↓-hom-s (κ Raw.1#) 0 [] ρ Ρ  ⟩
  ρ * ⟦ κ Raw.1# ⟧ Ρ                         ≈⟨ *≫ 1-homo ⟩
  ρ * 1#                                     ≈⟨ *-identityʳ ρ ⟩
  ρ                                          ≡⟨ drop-1⇒lookup i Ρ′ ⟩
  Vec.lookup Ρ′ i                            ∎


text:
{-

Holey congruence for propositional equality.

-}

module Holes.Cong.Propositional where

open import Holes.Prelude
open PropEq using (_≡_; refl; cong; sym; trans)

import Holes.Cong.General as Cong

open Cong (quote cong) (quote sym) public
  using (cong!)


text:
data N : Set where
  suc : N → N

data Val : N → Set where
  valSuc : ∀ n → Val (suc n)

record R : Set where
  constructor wrap
  field unwrap : N

data W (ft : R) : Set where
  immed : (v : Val (R.unwrap ft)) → W ft

test : (fa : R) → W fa → R
test fa (immed (valSuc a)) = fa

postulate
  Evaluate : ∀ (ft : R) (P : (w : W ft) → Set) → Set

test₂ : ∀ (fa : R) → Set
test₂ fa = Evaluate fa testw
  where
  testw : W fa → Set
  testw (immed (valSuc a)) = W fa

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Operations.Combinatorial where

open import Data.Bool using (true; false)
import      Data.Bool as B
import      Data.Fin  as F
open import Data.Nat  using (ℕ; suc)
open import Data.Vec  using ([]; _∷_)
import      Data.Vec  as V
open import Relation.Binary.PropositionalEquality

open import Types
open import Eval

not : Closed (𝔹 ⇒ 𝔹)
not = lam (var F.zero refl nand var F.zero refl)

not-prf : ∀ {n} {ctx : Ctx n} {Γ : Env ctx} b → (Γ ⟦ not ⟧) b ≡ B.not b
not-prf true = refl
not-prf false = refl

not⁺ : ∀ n → Closed (𝔹⁺ n ⇒ 𝔹⁺ n)
not⁺ 0 = lam []
not⁺ (suc n) = lam (not ∙ head (var F.zero refl) ∷ not⁺ n ∙ tail (var F.zero refl))

not⁺-prf : ∀ {n m} {ctx : Ctx m} {Γ : Env ctx} bs → (Γ ⟦ not⁺ n ⟧) bs ≡ V.map B.not bs
not⁺-prf [] = refl
not⁺-prf (true ∷ bs) = cong₂ _∷_ refl (not⁺-prf bs)
not⁺-prf (false ∷ bs) = cong₂ _∷_ refl (not⁺-prf bs)

and : Closed (𝔹 ⇒ (𝔹 ⇒ 𝔹))
and = lam (lam (not ∙ ((var (F.suc F.zero) refl) nand (var F.zero refl))))

and-prf : ∀ a b → ([] ⟦ and ⟧) a b ≡ B._∧_ a b
and-prf  true  true = refl
and-prf  true false = refl
and-prf false  true = refl
and-prf false false = refl

and⁺ : ∀ n → Closed (𝔹⁺ n ⇒ (𝔹⁺ n ⇒ 𝔹⁺ n))
and⁺ 0 = lam (lam [])
and⁺ (suc n) = lam (lam (x ∷ xs))
  where
  x  = and    ∙ head (var (F.suc F.zero) refl) ∙ head (var F.zero refl)
  xs = and⁺ n ∙ tail (var (F.suc F.zero) refl) ∙ tail (var F.zero refl)

and⁺-prf : ∀ {n m} {ctx : Ctx m} {Γ : Env ctx} as bs → (Γ ⟦ and⁺ n ⟧) as bs ≡ V.zipWith B._∧_ as bs
and⁺-prf [] [] = refl
and⁺-prf ( true ∷ as) ( true ∷ bs) = cong₂ _∷_ refl (and⁺-prf as bs)
and⁺-prf ( true ∷ as) (false ∷ bs) = cong₂ _∷_ refl (and⁺-prf as bs)
and⁺-prf (false ∷ as) ( true ∷ bs) = cong₂ _∷_ refl (and⁺-prf as bs)
and⁺-prf (false ∷ as) (false ∷ bs) = cong₂ _∷_ refl (and⁺-prf as bs)

or : Closed (𝔹 ⇒ (𝔹 ⇒ 𝔹))
or = lam (lam (l nand r))
  where
  l = ((var (F.suc F.zero) refl) nand (var (F.suc F.zero) refl))
  r = ((var F.zero refl) nand (var F.zero refl))

or-prf : ∀ a b → ([] ⟦ or ⟧) a b ≡ B._∨_ a b
or-prf  true  true = refl
or-prf  true false = refl
or-prf false  true = refl
or-prf false false = refl

or⁺ : ∀ n → Closed (𝔹⁺ n ⇒ (𝔹⁺ n ⇒ 𝔹⁺ n))
or⁺ 0 = lam (lam [])
or⁺ (suc n) = lam (lam (x ∷ xs))
  where
  x  = or    ∙ head (var (F.suc F.zero) refl) ∙ head (var F.zero refl)
  xs = or⁺ n ∙ tail (var (F.suc F.zero) refl) ∙ tail (var F.zero refl)

or⁺-prf : ∀ {n m} {ctx : Ctx m} {Γ : Env ctx} as bs → (Γ ⟦ or⁺ n ⟧) as bs ≡ V.zipWith B._∨_ as bs
or⁺-prf [] [] = refl
or⁺-prf ( true ∷ as) ( true ∷ bs) = cong₂ _∷_ refl (or⁺-prf as bs)
or⁺-prf ( true ∷ as) (false ∷ bs) = cong₂ _∷_ refl (or⁺-prf as bs)
or⁺-prf (false ∷ as) ( true ∷ bs) = cong₂ _∷_ refl (or⁺-prf as bs)
or⁺-prf (false ∷ as) (false ∷ bs) = cong₂ _∷_ refl (or⁺-prf as bs)

xor : Closed (𝔹 ⇒ (𝔹 ⇒ 𝔹))
xor = lam (lam (lam (l nand r) ∙ x))
  where
  x = (var (F.suc F.zero) refl) nand (var F.zero refl)
  l = ((var (F.suc (F.suc F.zero)) refl) nand (var F.zero refl))
  r = ((var F.zero refl) nand (var (F.suc F.zero) refl))

xor-prf : ∀ a b → ([] ⟦ xor ⟧) a b ≡ B._xor_ a b
xor-prf  true  true = refl
xor-prf  true false = refl
xor-prf false  true = refl
xor-prf false false = refl

xor⁺ : ∀ n → Closed (𝔹⁺ n ⇒ (𝔹⁺ n ⇒ 𝔹⁺ n))
xor⁺ 0 = lam (lam [])
xor⁺ (suc n) = lam (lam (x ∷ xs))
  where
  x  = xor    ∙ head (var (F.suc F.zero) refl) ∙ head (var F.zero refl)
  xs = xor⁺ n ∙ tail (var (F.suc F.zero) refl) ∙ tail (var F.zero refl)

xor⁺-prf : ∀ {n m} {ctx : Ctx m} {Γ : Env ctx} as bs → (Γ ⟦ xor⁺ n ⟧) as bs ≡ V.zipWith B._xor_ as bs
xor⁺-prf [] [] = refl
xor⁺-prf ( true ∷ as) ( true ∷ bs) = cong₂ _∷_ refl (xor⁺-prf as bs)
xor⁺-prf ( true ∷ as) (false ∷ bs) = cong₂ _∷_ refl (xor⁺-prf as bs)
xor⁺-prf (false ∷ as) ( true ∷ bs) = cong₂ _∷_ refl (xor⁺-prf as bs)
xor⁺-prf (false ∷ as) (false ∷ bs) = cong₂ _∷_ refl (xor⁺-prf as bs)

max_stars_repo_name: bens/hwlc

max_issues_repo_name: bens/hwlc

max_forks_repo_name: bens/hwlc