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

module Definition.Conversion.Symmetry where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Conversion
open import Definition.Conversion.Stability
open import Definition.Conversion.Soundness
open import Definition.Conversion.Conversion
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Equality
open import Definition.Typed.Consequences.Reduction
open import Definition.Typed.Consequences.Injectivity
open import Definition.Typed.Consequences.Substitution
open import Definition.Typed.Consequences.SucCong

open import Tools.Product
import Tools.PropositionalEquality as PE

mutual
  -- Symmetry of algorithmic equality of neutrals
  sym~↑! : ∀ {t u A Γ Δ l} → ⊢ Γ ≡ Δ
        → Γ ⊢ t ~ u ↑! A ^ l
        → ∃ λ B → Γ ⊢ A ≡ B ^ [ ! , l ]  × Δ ⊢ u ~ t ↑! B ^ l
  sym~↑! Γ≡Δ (var-refl x x≡y) =
    let ⊢A = syntacticTerm x
    in  _ , refl ⊢A
     ,  var-refl (PE.subst (λ y → _ ⊢ var y ∷ _ ^ _) x≡y (stabilityTerm Γ≡Δ x))
                 (PE.sym x≡y)
  sym~↑! Γ≡Δ (app-cong {rF = !} t~u x) =
    let ⊢Γ , ⊢Δ , _ = contextConvSubst Γ≡Δ
        B , whnfB , A≡B , u~t = sym~↓! Γ≡Δ t~u
        F′ , G′ , ΠF′G′≡B = Π≡A A≡B whnfB
        F≡F′ , rF≡rF′ , lF≡lF' , lG≡lG' , G≡G′ = injectivity (PE.subst (λ x → _ ⊢ _ ≡ x ^ _) ΠF′G′≡B A≡B)
    in  _ , substTypeEq G≡G′ (soundnessConv↑Term x)
    ,   app-cong (PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) ΠF′G′≡B u~t)
                 (convConvTerm (symConv↑Term Γ≡Δ x) (stabilityEq Γ≡Δ F≡F′))
  sym~↑! Γ≡Δ (app-cong {rF = %} t~u x) =
    let ⊢Γ , ⊢Δ , _ = contextConvSubst Γ≡Δ
        B , whnfB , A≡B , u~t = sym~↓! Γ≡Δ t~u
        F′ , G′ , ΠF′G′≡B = Π≡A A≡B whnfB
        F≡F′ , rF≡rF′ , lF≡lF' , lG≡lG' , G≡G′ = injectivity (PE.subst (λ x → _ ⊢ _ ≡ x ^ _) ΠF′G′≡B A≡B)
    in  _ , substTypeEq G≡G′ (proj₂ (proj₂ (soundness~↑% x)))
    ,   app-cong (PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) ΠF′G′≡B u~t)
                 (sym~↑% Γ≡Δ (conv~↑% x (stabilityEq (reflConEq ⊢Γ) F≡F′)))
  sym~↑! Γ≡Δ (natrec-cong x x₁ x₂ t~u) =
    let ⊢Γ , ⊢Δ , _ = contextConvSubst Γ≡Δ
        B , whnfB , A≡B , u~t = sym~↓! Γ≡Δ t~u
        B≡ℕ = ℕ≡A A≡B whnfB
        F≡G = stabilityEq (Γ≡Δ ∙ refl (univ (ℕⱼ ⊢Γ))) (soundnessConv↑ x)
        F[0]≡G[0] = substTypeEq F≡G (refl (zeroⱼ ⊢Δ))
    in  _ , substTypeEq (soundnessConv↑ x) (soundness~↓! t~u)
    ,   natrec-cong (symConv↑ (Γ≡Δ ∙ (refl (univ (ℕⱼ ⊢Γ)))) x)
                    (convConvTerm (symConv↑Term Γ≡Δ x₁) F[0]≡G[0])
                    (convConvTerm (symConv↑Term Γ≡Δ x₂) (sucCong F≡G))
                    (PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) B≡ℕ u~t)
  sym~↑! Γ≡Δ (Emptyrec-cong x t~u) =
    let ⊢Γ , ⊢Δ , _ = contextConvSubst Γ≡Δ
        u~t = sym~↑% Γ≡Δ t~u
        -- F≡G = stabilityEq Γ≡Δ (soundnessConv↑ x)
    in  _ , soundnessConv↑ x
    , Emptyrec-cong (symConv↑ Γ≡Δ x) u~t
  sym~↑! Γ≡Δ (Id-cong X x x₁) =
    let ⊢Γ , ⊢Δ , _ = contextConvSubst Γ≡Δ
        B , whnfB , A≡B , u~t = sym~↓! Γ≡Δ X
        U≡B = U≡A-whnf A≡B whnfB
        A'≡A = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) U≡B u~t
    in _ , refl (Ugenⱼ ⊢Γ) , Id-cong A'≡A
                                     (convConvTerm (symConv↑Term Γ≡Δ x) (univ (soundness~↓! (stability~↓! Γ≡Δ X))))
                                     (convConvTerm (symConv↑Term Γ≡Δ x₁) (univ (soundness~↓! (stability~↓! Γ≡Δ X))))
  sym~↑! Γ≡Δ (Id-ℕ X x) =
    let ⊢Γ , ⊢Δ , _ = contextConvSubst Γ≡Δ
        B , whnfB , A≡B , u~t = sym~↓! Γ≡Δ X
        U≡B = ℕ≡A A≡B whnfB
        A'≡A = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) U≡B u~t
    in _ , refl (Ugenⱼ ⊢Γ) , Id-ℕ A'≡A (symConv↑Term Γ≡Δ x)
  sym~↑! Γ≡Δ (Id-ℕ0 X) =
    let ⊢Γ , ⊢Δ , _ = contextConvSubst Γ≡Δ
        B , whnfB , A≡B , u~t = sym~↓! Γ≡Δ X
        U≡B = ℕ≡A A≡B whnfB
        A'≡A = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) U≡B u~t
    in _ , refl (Ugenⱼ ⊢Γ) , Id-ℕ0 A'≡A
  sym~↑! Γ≡Δ (Id-ℕS x X) =
    let ⊢Γ , ⊢Δ , _ = contextConvSubst Γ≡Δ
        B , whnfB , A≡B , u~t = sym~↓! Γ≡Δ X
        U≡B = ℕ≡A A≡B whnfB
        A'≡A = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) U≡B u~t
    in _ , refl (Ugenⱼ ⊢Γ) , Id-ℕS (symConv↑Term Γ≡Δ x) A'≡A
  sym~↑! Γ≡Δ (Id-U X x) =
    let ⊢Γ , ⊢Δ , _ = contextConvSubst Γ≡Δ
        B , whnfB , A≡B , u~t = sym~↓! Γ≡Δ X
        U≡B = U≡A-whnf A≡B whnfB
        A'≡A = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) U≡B u~t
    in _ , refl (Ugenⱼ ⊢Γ) , Id-U A'≡A (symConv↑Term Γ≡Δ x)
  sym~↑! Γ≡Δ (Id-Uℕ X) =
    let ⊢Γ , ⊢Δ , _ = contextConvSubst Γ≡Δ
        B , whnfB , A≡B , u~t = sym~↓! Γ≡Δ X
        U≡B = U≡A-whnf A≡B whnfB
        A'≡A = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) U≡B u~t
    in _ , refl (Ugenⱼ ⊢Γ) , Id-Uℕ A'≡A
  sym~↑! Γ≡Δ (Id-UΠ x X) =
    let ⊢Γ , ⊢Δ , _ = contextConvSubst Γ≡Δ
        B , whnfB , A≡B , u~t = sym~↓! Γ≡Δ X
        U≡B = U≡A-whnf A≡B whnfB
        A'≡A = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) U≡B u~t
    in _ , refl (Ugenⱼ ⊢Γ) , Id-UΠ (symConv↑Term Γ≡Δ x) A'≡A
  sym~↑! Γ≡Δ (cast-cong X x x₁ x₂ x₃) =
      let U , whnfU , U≡U' , A'~A = sym~↓! Γ≡Δ X
          B'~B = symConv↑Term Γ≡Δ x
          U≡B = U≡A-whnf U≡U' whnfU
          A'≡A = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) U≡B A'~A
      in
          _ , univ (soundnessConv↑Term x), cast-cong A'≡A B'~B
                                                     (convConvTerm (symConv↑Term Γ≡Δ x₁) (univ (soundness~↓! (stability~↓! Γ≡Δ X))))
                                                     (stabilityTerm Γ≡Δ x₃) (stabilityTerm Γ≡Δ x₂)
  sym~↑! Γ≡Δ (cast-ℕ X x x₁ x₂) =
      let U , whnfU , U≡U' , A'~A = sym~↓! Γ≡Δ X
          B'~B = symConv↑Term Γ≡Δ x
          U≡B = U≡A-whnf U≡U' whnfU
          A'≡A = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) U≡B A'~A
      in _ , univ (soundness~↓! X) , cast-ℕ A'≡A (symConv↑Term Γ≡Δ x) (stabilityTerm Γ≡Δ x₂) (stabilityTerm Γ≡Δ x₁)
  sym~↑! Γ≡Δ (cast-ℕℕ X x x₁) =
      let ⊢Γ , ⊢Δ , _ = contextConvSubst Γ≡Δ
          N , whnfN , N≡N' , t'~t = sym~↓! Γ≡Δ X
          ℕ≡B = ℕ≡A N≡N' whnfN
          t'≡t = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) ℕ≡B t'~t
      in _ , refl (univ (ℕⱼ ⊢Γ)) , cast-ℕℕ t'≡t (stabilityTerm Γ≡Δ x₁) (stabilityTerm Γ≡Δ x)
  sym~↑! Γ≡Δ (cast-Π x X x₁ x₂ x₃) =
      let U , whnfU , U≡U' , A'~A = sym~↓! Γ≡Δ X
          B'~B = symConv↑Term Γ≡Δ x
          U≡B = U≡A-whnf U≡U' whnfU
          A'≡A = PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) U≡B A'~A
      in _ , univ (soundness~↓! X) , cast-Π B'~B A'≡A
                                            (convConvTerm (symConv↑Term Γ≡Δ x₁) (univ (soundnessConv↑Term (stabilityConv↑Term Γ≡Δ x))))
                                            (stabilityTerm Γ≡Δ x₃) (stabilityTerm Γ≡Δ x₂)
  sym~↑! Γ≡Δ (cast-Πℕ x x₁ x₂ x₃) =
      let ⊢Γ , ⊢Δ , _ = contextConvSubst Γ≡Δ
      in _ , refl (univ (ℕⱼ ⊢Γ)) , cast-Πℕ (symConv↑Term Γ≡Δ x)
                                           (convConvTerm (symConv↑Term Γ≡Δ x₁) (univ (soundnessConv↑Term (stabilityConv↑Term Γ≡Δ x))))
                                           (stabilityTerm Γ≡Δ x₃) (stabilityTerm Γ≡Δ x₂)
  sym~↑! Γ≡Δ (cast-ℕΠ x x₁ x₂ x₃) = _ , univ (soundnessConv↑Term x) , cast-ℕΠ (symConv↑Term Γ≡Δ x) (symConv↑Term Γ≡Δ x₁)
                                                                              (stabilityTerm Γ≡Δ x₃) (stabilityTerm Γ≡Δ x₂)
  sym~↑! Γ≡Δ (cast-ΠΠ%! x x₁ x₂ x₃ x₄) = _ , univ (soundnessConv↑Term x₁) ,
                                         cast-ΠΠ%! (symConv↑Term Γ≡Δ x) (symConv↑Term Γ≡Δ x₁)
                                                   (convConvTerm (symConv↑Term Γ≡Δ x₂) (univ (soundnessConv↑Term (stabilityConv↑Term Γ≡Δ x))))
                                                   (stabilityTerm Γ≡Δ x₄) (stabilityTerm Γ≡Δ x₃)
  sym~↑! Γ≡Δ (cast-ΠΠ!% x x₁ x₂ x₃ x₄) = _ , univ (soundnessConv↑Term x₁) ,
                                         cast-ΠΠ!% (symConv↑Term Γ≡Δ x) (symConv↑Term Γ≡Δ x₁)
                                                   (convConvTerm (symConv↑Term Γ≡Δ x₂) (univ (soundnessConv↑Term (stabilityConv↑Term Γ≡Δ x))))
                                                   (stabilityTerm Γ≡Δ x₄) (stabilityTerm Γ≡Δ x₃)

  sym~↑% : ∀ {t u A Γ Δ l} → ⊢ Γ ≡ Δ
         → Γ ⊢ t ~ u ↑% A ^ l
         → Δ ⊢ u ~ t ↑% A ^ l
  sym~↑% Γ≡Δ (%~↑ ⊢k ⊢l) = %~↑ (stabilityTerm Γ≡Δ ⊢l) (stabilityTerm Γ≡Δ ⊢k)

  sym~↑ : ∀ {t u A rA Γ Δ l} → ⊢ Γ ≡ Δ
        → Γ ⊢ t ~ u ↑ A ^ [ rA , l ]
        → ∃ λ B → Γ ⊢ A ≡ B ^ [ rA , l ] × Δ ⊢ u ~ t ↑ B ^ [ rA , l ]
  sym~↑ Γ≡Δ (~↑! x) =
    let B , A≡B , x′ = sym~↑! Γ≡Δ x
    in B , A≡B , ~↑! x′
  sym~↑ {A = A} Γ≡Δ (~↑% x) =
    let x′ = sym~↑% Γ≡Δ x
        ⊢A , _ , _ = syntacticEqTerm (proj₂ (proj₂ (soundness~↑% x)))
    in A , refl ⊢A , ~↑% x′

  -- Symmetry of algorithmic equality of neutrals of types in WHNF.
  sym~↓! : ∀ {t u A Γ Δ l} → ⊢ Γ ≡ Δ → Γ ⊢ t ~ u ↓! A ^ l
         → ∃ λ B → Whnf B × Γ ⊢ A ≡ B ^ [ ! , l ] × Δ ⊢ u ~ t ↓! B ^ l
  sym~↓! Γ≡Δ ([~] A₁ D whnfA k~l) =
    let B , A≡B , k~l′ = sym~↑! Γ≡Δ k~l
        _ , ⊢B = syntacticEq A≡B
        B′ , whnfB′ , D′ = whNorm ⊢B
        A≡B′ = trans (sym (subset* D)) (trans A≡B (subset* (red D′)))
    in  B′ , whnfB′ , A≡B′ , [~] B (stabilityRed* Γ≡Δ (red D′)) whnfB′ k~l′

  -- Symmetry of algorithmic equality of types.
  symConv↑ : ∀ {A B r Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ A [conv↑] B ^ r → Δ ⊢ B [conv↑] A ^ r
  symConv↑ Γ≡Δ ([↑] A′ B′ D D′ whnfA′ whnfB′ A′<>B′) =
    [↑] B′ A′ (stabilityRed* Γ≡Δ D′) (stabilityRed* Γ≡Δ D) whnfB′ whnfA′
        (symConv↓ Γ≡Δ A′<>B′)

  -- Symmetry of algorithmic equality of types in WHNF.
  symConv↓ : ∀ {A B r Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ A [conv↓] B ^ r → Δ ⊢ B [conv↓] A ^ r
  symConv↓ Γ≡Δ (U-refl PE.refl x) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  U-refl PE.refl ⊢Δ
  symConv↓ Γ≡Δ (univ x) = univ (symConv↓Term Γ≡Δ x)

  -- Symmetry of algorithmic equality of terms.
  symConv↑Term : ∀ {t u A Γ Δ l} → ⊢ Γ ≡ Δ → Γ ⊢ t [conv↑] u ∷ A ^ l → Δ ⊢ u [conv↑] t ∷ A ^ l
  symConv↑Term Γ≡Δ ([↑]ₜ B t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u) =
    [↑]ₜ B u′ t′ (stabilityRed* Γ≡Δ D) (stabilityRed*Term Γ≡Δ d′)
         (stabilityRed*Term Γ≡Δ d) whnfB whnfu′ whnft′ (symConv↓Term Γ≡Δ t<>u)

  -- Symmetry of algorithmic equality of terms in WHNF.
  symConv↓Term : ∀ {t u A Γ Δ l} → ⊢ Γ ≡ Δ → Γ ⊢ t [conv↓] u ∷ A ^ l  → Δ ⊢ u [conv↓] t ∷ A ^ l
  symConv↓Term Γ≡Δ (U-refl x x₁) =
      let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ in U-refl (PE.sym x) ⊢Δ
  symConv↓Term Γ≡Δ (ne t~u) =
    let ⊢Γ , ⊢Δ , _ = contextConvSubst Γ≡Δ
        B , whnfB , A≡B , u~t = sym~↓! Γ≡Δ t~u
        U≡B = U≡A-whnf A≡B whnfB
    in ne (PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) U≡B (proj₂ (proj₂ (proj₂ (sym~↓! Γ≡Δ t~u)))))
  symConv↓Term Γ≡Δ (ℕ-refl x) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  ℕ-refl ⊢Δ
  symConv↓Term Γ≡Δ (Empty-refl x _) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  Empty-refl x ⊢Δ
  symConv↓Term Γ≡Δ (∃-cong PE.refl x A<>B A<>B₁) =
    let F≡H = soundnessConv↑Term A<>B
        _ , ⊢H = syntacticEq (stabilityEq Γ≡Δ (univ F≡H))
    in ∃-cong PE.refl ⊢H (symConv↑Term Γ≡Δ A<>B)
                 (symConv↑Term (Γ≡Δ ∙ univ F≡H) A<>B₁)
  symConv↓Term Γ≡Δ (Π-cong PE.refl PE.refl PE.refl PE.refl l< l<' x A<>B A<>B₁) =
    let F≡H = soundnessConv↑Term A<>B
        _ , ⊢H = syntacticEq (stabilityEq Γ≡Δ (univ F≡H))
    in  Π-cong PE.refl PE.refl PE.refl PE.refl l< l<' ⊢H (symConv↑Term Γ≡Δ A<>B)
                  (symConv↑Term (Γ≡Δ ∙ univ F≡H) A<>B₁)
  symConv↓Term Γ≡Δ (ℕ-ins t~u) =
    let B , whnfB , A≡B , u~t = sym~↓! Γ≡Δ t~u
        B≡ℕ = ℕ≡A A≡B whnfB
    in  ℕ-ins (PE.subst (λ x → _ ⊢ _ ~ _ ↓! x ^ _) B≡ℕ u~t)
  symConv↓Term Γ≡Δ (ne-ins t u x t~u) =
    let B , whnfB , A≡B , u~t = sym~↓! Γ≡Δ t~u
    in  ne-ins (stabilityTerm Γ≡Δ u) (stabilityTerm Γ≡Δ t) x u~t
  symConv↓Term Γ≡Δ (zero-refl x) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  zero-refl ⊢Δ
  symConv↓Term Γ≡Δ (suc-cong t<>u) = suc-cong (symConv↑Term Γ≡Δ t<>u)
  symConv↓Term Γ≡Δ (η-eq l< l<' x x₁ x₂ y y₁ t<>u) =
    η-eq l<  l<' (stability Γ≡Δ x) (stabilityTerm Γ≡Δ x₂) (stabilityTerm Γ≡Δ x₁)
         y₁ y (symConv↑Term (Γ≡Δ ∙ refl x) t<>u)

-- Symmetry of algorithmic equality of types with preserved context.
symConv : ∀ {A B r Γ} → Γ ⊢ A [conv↑] B ^ r → Γ ⊢ B [conv↑] A ^ r
symConv A<>B =
  let ⊢Γ = wfEq (soundnessConv↑ A<>B)
  in  symConv↑ (reflConEq ⊢Γ) A<>B

-- Symmetry of algorithmic equality of terms with preserved context.
symConvTerm : ∀ {t u A Γ l} → Γ ⊢ t [conv↑] u ∷ A ^ l → Γ ⊢ u [conv↑] t ∷ A ^ l
symConvTerm t<>u =
  let ⊢Γ = wfEqTerm (soundnessConv↑Term t<>u)
  in  symConv↑Term (reflConEq ⊢Γ) t<>u

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Functions.Definition
open import Functions.Lemmas
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.Lemmas
open import Sets.Cardinality.Finite.Definition
open import Semirings.Definition
open import Sets.CantorBijection.CantorBijection
open import Orders.Total.Definition

module Sets.Cardinality where

open import Semirings.Lemmas ℕSemiring

record CountablyInfiniteSet {a : _} (A : Set a) : Set a where
  field
    counting : A → ℕ
    countingIsBij : Bijection counting

data Countable {a : _} (A : Set a) : Set a where
  finite : FiniteSet A → Countable A
  infinite : CountablyInfiniteSet A → Countable A

ℕCountable : CountablyInfiniteSet ℕ
ℕCountable = record { counting = id ; countingIsBij = invertibleImpliesBijection (record { inverse = id ; isLeft = λ b → refl ; isRight = λ a → refl}) }

doubleLemma : (a b : ℕ) → 2 *N a ≡ 2 *N b → a ≡ b
doubleLemma a b pr = productCancelsLeft 2 a b (le 1 refl) pr

evenCannotBeOdd : (a b : ℕ) → 2 *N a ≡ succ (2 *N b) → False
evenCannotBeOdd zero b ()
evenCannotBeOdd (succ a) zero pr rewrite Semiring.commutative ℕSemiring a 0 | Semiring.commutative ℕSemiring a (succ a) = naughtE (equalityCommutative (succInjective pr))
evenCannotBeOdd (succ a) (succ b) pr = evenCannotBeOdd a b pr''
  where
    pr' : a +N a ≡ (b +N succ b)
    pr' rewrite Semiring.commutative ℕSemiring a 0 | Semiring.commutative ℕSemiring b 0 | Semiring.commutative ℕSemiring a (succ a) = succInjective (succInjective pr)
    pr'' : 2 *N a ≡ succ (2 *N b)
    pr'' rewrite Semiring.commutative ℕSemiring a 0 | Semiring.commutative ℕSemiring b 0 | Semiring.commutative ℕSemiring (succ b) b = pr'

aMod2 : (a : ℕ) → Sg ℕ (λ i → (2 *N i ≡ a) || (succ (2 *N i) ≡ a))
aMod2 zero = (0 , inl refl)
aMod2 (succ a) with aMod2 a
aMod2 (succ a) | b , inl x = b , inr (applyEquality succ x)
aMod2 (succ a) | b , inr x = (succ b) , inl pr
  where
    pr : succ (b +N succ (b +N 0)) ≡ succ a
    pr rewrite Semiring.commutative ℕSemiring b (succ (b +N 0)) | Semiring.commutative ℕSemiring (b +N 0) b = applyEquality succ x

sqrtFloor : (a : ℕ) → Sg (ℕ && ℕ) (λ pair → ((_&&_.fst pair) *N (_&&_.fst pair) +N (_&&_.snd pair) ≡ a) && ((_&&_.snd pair) <N 2 *N (_&&_.fst pair) +N 1))
sqrtFloor zero = (0 ,, 0) , (refl ,, le zero refl)
sqrtFloor (succ n) with sqrtFloor n
sqrtFloor (succ n) | (a ,, b) , pr with TotalOrder.totality ℕTotalOrder b (2 *N a)
sqrtFloor (succ n) | (a ,, b) , pr | inl (inl x) = (a ,, succ b) , (p ,, q)
  where
    p : a *N a +N succ b ≡ succ n
    p rewrite Semiring.commutative ℕSemiring (a *N a) (succ b) | Semiring.commutative ℕSemiring b (a *N a) = applyEquality succ (_&&_.fst pr)
    q : succ b <N (a +N (a +N 0)) +N 1
    q rewrite Semiring.commutative ℕSemiring (a +N (a +N 0)) (succ 0) | Semiring.commutative ℕSemiring a 0 = succPreservesInequality x
sqrtFloor (succ n) | (a ,, b) , (_ ,, pr) | inl (inr x) rewrite Semiring.commutative ℕSemiring (a +N (a +N 0)) (succ 0) = exFalso (noIntegersBetweenXAndSuccX (a +N (a +N 0)) x pr)
sqrtFloor (succ n) | (a ,, b) , pr | inr x = (succ a ,, 0) , (q ,, succIsPositive _)
  where
    p : a +N a *N succ a ≡ n
    p rewrite x | Semiring.commutative ℕSemiring a 0 | Semiring.commutative ℕSemiring (a +N a) (succ 0) | Semiring.commutative ℕSemiring (a *N a) (succ a +N a) | multiplicationNIsCommutative a (succ a) | Semiring.commutative ℕSemiring (a *N a) (a +N a) | Semiring.+Associative ℕSemiring a a (a *N a) = _&&_.fst pr
    q : succ ((a +N a *N succ a) +N 0) ≡ succ n
    q rewrite Semiring.commutative ℕSemiring (a +N a *N succ a) 0 = applyEquality succ p

pairUnionIsCountable : {a b : _} {A : Set a} {B : Set b} → (X : CountablyInfiniteSet A) → (Y : CountablyInfiniteSet B) → CountablyInfiniteSet (A || B)
CountablyInfiniteSet.counting (pairUnionIsCountable X Y) (inl r) = 2 *N (CountablyInfiniteSet.counting X r)
CountablyInfiniteSet.counting (pairUnionIsCountable X Y) (inr s) = succ (2 *N (CountablyInfiniteSet.counting Y s))
Bijection.inj (CountablyInfiniteSet.countingIsBij (pairUnionIsCountable X Y)) {inl x} {inl y} pr rewrite Semiring.commutative ℕSemiring (CountablyInfiniteSet.counting X x) 0 | Semiring.commutative ℕSemiring (CountablyInfiniteSet.counting X y) 0 | doubleIsAddTwo (CountablyInfiniteSet.counting X x) | doubleIsAddTwo (CountablyInfiniteSet.counting X y) = applyEquality inl (Bijection.inj (CountablyInfiniteSet.countingIsBij X) inter)
  where
    inter : CountablyInfiniteSet.counting X x ≡ CountablyInfiniteSet.counting X y
    inter = doubleLemma (CountablyInfiniteSet.counting X x) (CountablyInfiniteSet.counting X y) pr
Bijection.inj (CountablyInfiniteSet.countingIsBij (pairUnionIsCountable X Y)) {inl x} {inr y} pr = exFalso (evenCannotBeOdd (CountablyInfiniteSet.counting X x) (CountablyInfiniteSet.counting Y y) pr)
Bijection.inj (CountablyInfiniteSet.countingIsBij (pairUnionIsCountable X Y)) {inr x} {inl y} pr = exFalso (evenCannotBeOdd (CountablyInfiniteSet.counting X y) (CountablyInfiniteSet.counting Y x) (equalityCommutative pr))
Bijection.inj (CountablyInfiniteSet.countingIsBij (pairUnionIsCountable X Y)) {inr x} {inr y} pr = applyEquality inr (Bijection.inj (CountablyInfiniteSet.countingIsBij Y) (doubleLemma (CountablyInfiniteSet.counting Y x) (CountablyInfiniteSet.counting Y y) (succInjective pr) ))
Bijection.surj (CountablyInfiniteSet.countingIsBij (pairUnionIsCountable X Y)) b with aMod2 b
Bijection.surj (CountablyInfiniteSet.countingIsBij (pairUnionIsCountable X Y)) b | a , inl x with Bijection.surj (CountablyInfiniteSet.countingIsBij X) a
Bijection.surj (CountablyInfiniteSet.countingIsBij (pairUnionIsCountable X Y)) b | a , inl x | r , pr = inl r , ans
  where
    ans : 2 *N CountablyInfiniteSet.counting X r ≡ b
    ans rewrite pr = x
Bijection.surj (CountablyInfiniteSet.countingIsBij (pairUnionIsCountable X Y)) b | a , inr x with Bijection.surj (CountablyInfiniteSet.countingIsBij Y) a
Bijection.surj (CountablyInfiniteSet.countingIsBij (pairUnionIsCountable X Y)) b | a , inr x | r , pr = inr r , ans
  where
    ans : succ (2 *N CountablyInfiniteSet.counting Y r) ≡ b
    ans rewrite pr = x

firstEqualityOfPair : {a b : _} {A : Set a} {B : Set b} → {x1 x2 : A} → {y1 y2 : B} → (x1 ,, y1) ≡ (x2 ,, y2) → x1 ≡ x2
firstEqualityOfPair {x1} {x2} {y1} {y2} refl = refl

secondEqualityOfPair : {a b : _} {A : Set a} {B : Set b} → {x1 x2 : A} → {y1 y2 : B} → (x1 ,, y1) ≡ (x2 ,, y2) → y1 ≡ y2
secondEqualityOfPair {x1} {x2} {y1} {y2} refl = refl

reflPair : {a b : _} {A : Set a} {B : Set b} {x1 x2 : A} {y1 y2 : B} → (x1 ≡ x2) → (y1 ≡ y2) → (x1 ,, y1) ≡ x2 ,, y2
reflPair refl refl = refl

bijectionOfCountableSetIsCountable : {a b : _} {A : Set a} {B : Set b} → (X : CountablyInfiniteSet A) {f : A → B} → (bij : Bijection f) → CountablyInfiniteSet B
CountablyInfiniteSet.counting (bijectionOfCountableSetIsCountable X {f} record { inj = inj ; surj = surj }) b with surj b
CountablyInfiniteSet.counting (bijectionOfCountableSetIsCountable record { counting = counting ; countingIsBij = countingIsBij } {f} record { inj = inj ; surj = surj }) b | a , pr = counting a
Bijection.inj (CountablyInfiniteSet.countingIsBij (bijectionOfCountableSetIsCountable X {f} record { inj = inj ; surj = surj })) {m} {n} m=n with surj m
Bijection.inj (CountablyInfiniteSet.countingIsBij (bijectionOfCountableSetIsCountable X {f} record { inj = inj ; surj = surj })) {m} {n} m=n | a , b with surj n
... | c , d = transitivity (equalityCommutative b) (transitivity (applyEquality f (Bijection.inj (CountablyInfiniteSet.countingIsBij X) m=n)) d)
Bijection.surj (CountablyInfiniteSet.countingIsBij (bijectionOfCountableSetIsCountable X {f} record { inj = inj ; surj = surj })) b with Bijection.surj (CountablyInfiniteSet.countingIsBij X) b
Bijection.surj (CountablyInfiniteSet.countingIsBij (bijectionOfCountableSetIsCountable X {f} record { inj = inj ; surj = surj })) b | a , pr = f a , s
  where
    s : CountablyInfiniteSet.counting (bijectionOfCountableSetIsCountable X {f} record { inj = inj ; surj = surj }) (f a) ≡ b
    s with surj (f a)
    s | t , u = transitivity (applyEquality (CountablyInfiniteSet.counting X) (inj u)) pr

N^2Countable : CountablyInfiniteSet (ℕ && ℕ)
CountablyInfiniteSet.counting N^2Countable x = Invertible.inverse (bijectionImpliesInvertible (cantorBijection)) x
CountablyInfiniteSet.countingIsBij N^2Countable = invertibleImpliesBijection (inverseIsInvertible (bijectionImpliesInvertible cantorBijection))

tupleRmap : {a b c : _} {A : Set a} {B : Set b} {C : Set c} → (f : B → C) → (A && B) → (A && C)
tupleRmap f (a ,, b) = (a ,, f b)

tupleLmap : {a b c : _} {A : Set a} {B : Set b} {C : Set c} → (f : A → C) → (A && B) → (C && B)
tupleLmap f (a ,, b) = (f a ,, b)

bijectionOnRightOfProduct : {a b c : _} {A : Set a} {B : Set b} {C : Set c} → {f : B → C} → Bijection f → Bijection (tupleRmap {A = A} f)
Bijection.inj (bijectionOnRightOfProduct {A = A} {B} {C} {f} bij) {fst ,, snd} {fst₁ ,, snd₁} gx=gy rewrite firstEqualityOfPair gx=gy | Bijection.inj bij (secondEqualityOfPair gx=gy) = refl
Bijection.surj (bijectionOnRightOfProduct {A = A} {B} {C} {f} bij) (fst ,, snd) with Bijection.surj bij snd
Bijection.surj (bijectionOnRightOfProduct {A = A} {B} {C} {f} bij) (fst ,, snd) | b , pr = (fst ,, b) , reflPair refl pr

bijectionOnLeftOfProduct : {a b c : _} {A : Set a} {B : Set b} {C : Set c} → {f : A → C} → Bijection f → Bijection (tupleLmap {B = B} f)
Bijection.inj (bijectionOnLeftOfProduct {A = A} {B} {C} {f} bij) {a ,, b} {c ,, d} gx=gy rewrite secondEqualityOfPair gx=gy | Bijection.inj bij (firstEqualityOfPair gx=gy) = refl
Bijection.surj (bijectionOnLeftOfProduct {A = A} {B} {C} {f} bij) (fst ,, snd) with Bijection.surj bij fst
Bijection.surj (bijectionOnLeftOfProduct {A = A} {B} {C} {f} bij) (fst ,, snd) | a , b = (a ,, snd) , reflPair b refl

pairProductIsCountable : {a b : _} {A : Set a} {B : Set b} → (X : CountablyInfiniteSet A) → (Y : CountablyInfiniteSet B) → CountablyInfiniteSet (A && B)
pairProductIsCountable {A = A} {B = B} X Y = bijectionOfCountableSetIsCountable N^2Countable {(tupleLmap m) ∘ (tupleRmap n)} bijF
  where
    bijM = (bijectionImpliesInvertible (CountablyInfiniteSet.countingIsBij X))
    bijN = (bijectionImpliesInvertible (CountablyInfiniteSet.countingIsBij Y))
    m : ℕ → A
    m = Invertible.inverse bijM
    n : ℕ → B
    n = Invertible.inverse bijN
    bM : Bijection m
    bM = invertibleImpliesBijection (record { inverse = CountablyInfiniteSet.counting X ; isLeft = Invertible.isRight bijM ; isRight = Invertible.isLeft bijM })
    bN : Bijection n
    bN = invertibleImpliesBijection (record { inverse = CountablyInfiniteSet.counting Y ; isLeft = Invertible.isRight bijN ; isRight = Invertible.isLeft bijN })
    bijF : Bijection ((tupleLmap {A = ℕ} {B = B} {C = A} m) ∘ (tupleRmap {A = ℕ} {B = ℕ} {C = B} n))
    bijF = bijectionComp {f = tupleRmap {A = ℕ} {B = ℕ} {C = B} n} {g = tupleLmap {A = ℕ} {B = B} {C = A} m} (bijectionOnRightOfProduct (invertibleImpliesBijection (bijectionImpliesInvertible bN))) (bijectionOnLeftOfProduct bM)

--  injectionToNMeansCountable : {a : _} {A : Set a} {f : A → ℕ} → Injection f → InfiniteSet A → Countable A
--  injectionToNMeansCountable {f = f} inj record { isInfinite = isInfinite } = {!!}

ext: agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Ring.DirectProd where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.Algebra.Ring.Base

private
  variable
    ℓ ℓ' ℓ'' ℓ''' : Level

module _
  (A'@(A , Ar) : Ring ℓ)
  (B'@(B , Br) : Ring ℓ')
  where

  open RingStr Ar using ()
    renaming
    ( 0r        to 0A
    ; 1r        to 1A
    ; _+_       to _+A_
    ; -_        to -A_
    ; _·_       to _·A_
    ; +Assoc    to +AAssoc
    ; +Identity to +AIdentity
    ; +Lid      to +ALid
    ; +Rid      to +ARid
    ; +Inv      to +AInv
    ; +Linv     to +ALinv
    ; +Rinv     to +ARinv
    ; +Comm     to +AComm
    ; ·Assoc    to ·AAssoc
    ; ·Identity to ·AIdentity
    ; ·Lid      to ·ALid
    ; ·Rid      to ·ARid
    ; ·Rdist+   to ·ARdist+
    ; ·Ldist+   to ·ALdist+
    ; is-set    to isSetA     )

  open RingStr Br using ()
    renaming
    ( 0r        to 0B
    ; 1r        to 1B
    ; _+_       to _+B_
    ; -_        to -B_
    ; _·_       to _·B_
    ; +Assoc    to +BAssoc
    ; +Identity to +BIdentity
    ; +Lid      to +BLid
    ; +Rid      to +BRid
    ; +Inv      to +BInv
    ; +Linv     to +BLinv
    ; +Rinv     to +BRinv
    ; +Comm     to +BComm
    ; ·Assoc    to ·BAssoc
    ; ·Identity to ·BIdentity
    ; ·Lid      to ·BLid
    ; ·Rid      to ·BRid
    ; ·Rdist+   to ·BRdist+
    ; ·Ldist+   to ·BLdist+
    ; is-set    to isSetB     )

  DirectProd-Ring : Ring (ℓ-max ℓ ℓ')
  fst DirectProd-Ring = A × B
  RingStr.0r (snd DirectProd-Ring) = 0A , 0B
  RingStr.1r (snd DirectProd-Ring) = 1A , 1B
  (snd DirectProd-Ring RingStr.+ (a , b)) (a' , b') = (a +A a') , (b +B b')
  (snd DirectProd-Ring RingStr.· (a , b)) (a' , b') = (a ·A a') , (b ·B b')
  (RingStr.- snd DirectProd-Ring) (a , b) = (-A a) , (-B b)
  RingStr.isRing (snd DirectProd-Ring) =
    makeIsRing (isSet× isSetA isSetB)
    (λ x y z i → +AAssoc (fst x) (fst y) (fst z) i , +BAssoc (snd x) (snd y) (snd z) i)
    (λ x i → (+ARid (fst x) i) , (+BRid (snd x) i))
    (λ x i → (+ARinv (fst x) i) , +BRinv (snd x) i)
    (λ x y i → (+AComm (fst x) (fst y) i) , (+BComm (snd x) (snd y) i))
    (λ x y z i → (·AAssoc (fst x) (fst y) (fst z) i) , (·BAssoc (snd x) (snd y) (snd z) i))
    (λ x i → (·ARid (fst x) i) , (·BRid (snd x) i))
    (λ x i → (·ALid (fst x) i) , (·BLid (snd x) i))
    (λ x y z i → (·ARdist+ (fst x) (fst y) (fst z) i) , (·BRdist+ (snd x) (snd y) (snd z) i))
    (λ x y z i → (·ALdist+ (fst x) (fst y) (fst z) i) , (·BLdist+ (snd x) (snd y) (snd z) i))

module Coproduct-Equiv
  {Xr@(X , Xstr) : Ring ℓ}
  {Yr@(Y , Ystr) : Ring ℓ'}
  {X'r@(X' , X'str) : Ring ℓ''}
  {Y'r@(Y' , Y'str) : Ring ℓ'''}
  where

  open Iso
  open IsRingHom
  open RingStr

  _+X×X'_ : X × X' → X × X' → X × X'
  _+X×X'_ = _+_ (snd (DirectProd-Ring Xr X'r))

  _+Y×Y'_ : Y × Y' → Y × Y' → Y × Y'
  _+Y×Y'_ = _+_ (snd (DirectProd-Ring Yr Y'r))

  _·X×X'_ : X × X' → X × X' → X × X'
  _·X×X'_ = _·_ (snd (DirectProd-Ring Xr X'r))

  _·Y×Y'_ : Y × Y' → Y × Y' → Y × Y'
  _·Y×Y'_ = _·_ (snd (DirectProd-Ring Yr Y'r))

  re×re' : (re : RingEquiv Xr Yr) → (re' : RingEquiv X'r Y'r) → (X × X') ≃ (Y × Y')
  re×re' re re' = ≃-× (fst re) (fst re')

  Coproduct-Equiv-12 : (re : RingEquiv Xr Yr) → (re' : RingEquiv X'r Y'r) →
                        RingEquiv (DirectProd-Ring Xr X'r) (DirectProd-Ring Yr Y'r)
  fst (Coproduct-Equiv-12 re re') = re×re' re re'
  snd (Coproduct-Equiv-12 re re') = makeIsRingHom fun-pres1 fun-pres+ fun-pres·
    where
    fun-pres1 : (fst (re×re' re re')) (1r Xstr , 1r X'str) ≡ (1r (Yr .snd) , 1r (Y'r .snd))
    fun-pres1 = ≡-× (pres1 (snd re)) (pres1 (snd re'))

    fun-pres+ : (x1 x2 : X × X') → (fst (re×re' re re')) (x1 +X×X' x2) ≡ (( (fst (re×re' re re')) x1) +Y×Y' ( (fst (re×re' re re')) x2))
    fun-pres+ (x1 , x'1) (x2 , x'2) = ≡-× (pres+ (snd re) x1 x2) (pres+ (snd re') x'1 x'2)

    fun-pres· : (x1 x2 : X × X') → (fst (re×re' re re')) (x1 ·X×X' x2) ≡ (( (fst (re×re' re re')) x1) ·Y×Y' ( (fst (re×re' re re')) x2))
    fun-pres· (x1 , x'1) (x2 , x'2) = ≡-× (pres· (snd re) x1 x2) (pres· (snd re') x'1 x'2)

max_stars_repo_name: guilhermehas/cubical

max_issues_repo_name: guilhermehas/cubical

max_forks_repo_name: guilhermehas/cubical


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Sets.EquivalenceRelations
open import Setoids.Setoids

module Setoids.Union.Definition {a b : _} {A : Set a} (S : Setoid {a} {b} A) where

open Setoid S
open Equivalence eq
open import Setoids.Subset S

unionPredicate : {c d : _} {pred1 : A → Set c} {pred2 : A → Set d} (s1 : subset pred1) (s2 : subset pred2) → A → Set (c ⊔ d)
unionPredicate {pred1 = pred1} {pred2} s1 s2 a = pred1 a || pred2 a

union : {c d : _} {pred1 : A → Set c} {pred2 : A → Set d} (s1 : subset pred1) (s2 : subset pred2) → subset (unionPredicate s1 s2)
union s1 s2 {x1} {x2} x1=x2 (inl x) = inl (s1 x1=x2 x)
union s1 s2 {x1} {x2} x1=x2 (inr x) = inr (s2 x1=x2 x)


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Everything where

import Cubical.HITs.Cylinder
import Cubical.HITs.Hopf
import Cubical.HITs.Interval
import Cubical.HITs.Ints.BiInvInt
import Cubical.HITs.Ints.DeltaInt
import Cubical.HITs.Ints.HAEquivInt
import Cubical.HITs.Ints.IsoInt
import Cubical.HITs.Ints.QuoInt
import Cubical.HITs.Join
import Cubical.HITs.ListedFiniteSet
import Cubical.HITs.Pushout
import Cubical.HITs.Modulo
import Cubical.HITs.S1
import Cubical.HITs.S2
import Cubical.HITs.S3
import Cubical.HITs.Rational
import Cubical.HITs.Susp
import Cubical.HITs.SmashProduct
import Cubical.HITs.Torus
import Cubical.HITs.PropositionalTruncation
import Cubical.HITs.SetTruncation
import Cubical.HITs.GroupoidTruncation
import Cubical.HITs.2GroupoidTruncation
import Cubical.HITs.SetQuotients
import Cubical.HITs.FiniteMultiset
import Cubical.HITs.Sn
import Cubical.HITs.RPn
import Cubical.HITs.Truncation
import Cubical.HITs.Colimit
import Cubical.HITs.MappingCones
import Cubical.HITs.InfNat
import Cubical.HITs.KleinBottle
import Cubical.HITs.DunceCap
import Cubical.HITs.Localization
import Cubical.HITs.Nullification
import Cubical.HITs.AssocList

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


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

module FOT.Common.FOL.Existential.RequiredWitness where

-- We need to use the existential witness in some proofs based on the
-- non-empty domain hypothesis.

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

postulate
  D   : Set
  D≢∅ : D  -- Non-empty domain.

-- The existential quantifier type on D.
data ∃ (P : D → Set) : Set where
  ∃-intro : ∀ {x} → P x → ∃ P

-- Theorem: Let A be a formula. If x is not free in A then ⊢ (∃x)A ↔ A
-- (Mendelson, 1997, proposition 2.18 (b), p. 70).

-- A version of the right-to-left implication.
l→r : {A : Set} → A → ∃ (λ _ → A)
l→r a = ∃-intro {x = D≢∅} a

------------------------------------------------------------------------------
-- References
--
-- Mendelson, Elliott (1997). Introduction to Mathematical Logic. 4th
-- ed. Chapman & Hall.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Andreas, 2019-03-27
-- Do not run checkIApplyConfluence unless --cubical

-- The following verbosity options triggers a crash
-- in case checkIApplyConfluence_ runs.

-- {-# OPTIONS --cubical #-}  -- Trigges the crash.

{-# OPTIONS -v tc.cover.iapply.confluence.crash:666 #-}  -- Activate crashing program point.

open import Agda.Builtin.Nat

-- A harmless definition.

id : Nat → Nat
id zero    = zero
id (suc x) = suc (id x)

-- Should succeed.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K --safe #-}
module Util.Data.Product where

open import Data.Product public hiding (map₂)

map₂ : ∀ {α β γ} {A : Set α} {B : A → Set β} {C : A → Set γ}
  → (∀ a → B a → C a)
  → Σ A B → Σ A C
map₂ f (a , b) = a , f a b

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:
{-# OPTIONS --cubical --safe #-}

module Cubical.Data.Strict2Group.Explicit.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Group.Base
open import Cubical.Data.Strict2Group.Explicit.Notation

record Strict2GroupExp ℓ : Type (ℓ-suc ℓ) where
  constructor strict2groupexp
  field
    -- a group of objects and a group of morphisms
    C₀ : Group ℓ
    C₁ : Group ℓ

    -- source and target morphisms
    s : morph C₁ C₀
    t : morph C₁ C₀

    -- identity morphism
    i : morph C₀ C₁
    -- the composition map C₁×₀C₁→C₁
    ∘ : (g f : Group.type C₁) → (s .fst) g ≡ (t .fst f) → Group.type C₁

  open S2GBaseNotation C₀ C₁ s t i ∘

  field
    si : (x : TC₀) → src (id x) ≡ x
    ti : (x : TC₀) → tar (id x) ≡ x

    s∘ : (g f : TC₁) → (c : CohCond g f) → src (∘ g f c) ≡ src f
    t∘ : (g f : TC₁) → (c : CohCond g f) → tar (∘ g f c) ≡ tar g

    -- composition operation defines a homomorphism that is associative and unital w.r.t. i
    isMorph∘ : ∀ {g f g' f' : TC₁} (c : CohCond g f) (c' : CohCond g' f')
      → ∘ (g ∙₁ g') (f ∙₁ f') (∙c c c') ≡ (∘ g f c) ∙₁ (∘ g' f' c')

    assoc∘ : ∀ {h g f : TC₁} → (c1 : CohCond g f) → (c2 : CohCond h g)
      → ∘ (∘ h g c2) f ((s∘ h g c2) ∙ c1) ≡  ∘ h (∘ g f c1) (c2 ∙ (sym (t∘ g f c1)))

    lUnit∘ : (f : TC₁) → ∘ (id (tar f)) f (si (tar f)) ≡ f
    rUnit∘ : (f : TC₁) → ∘ f (id (src f)) (sym (ti (src f))) ≡ f

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
------------------------------------------------------------------------
-- An example showing that transitivity-like proofs that are not
-- size-preserving can sometimes be used in a compositional way
------------------------------------------------------------------------

-- One can use the technique from "Beating the Productivity Checker
-- Using Embedded Languages" to make it possible to use
-- transitivity-like proofs that are not size-preserving in
-- corecursive definitions. However, it is unclear if this is ever
-- useful: the example presented below is rather contrived.

{-# OPTIONS --sized-types #-}

open import Prelude

module Delay-monad.Bisimilarity.Transitivity-constructor
  {a} {A : Type a} where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude.Size

open import Function-universe equality-with-J hiding (Kind)

open import Delay-monad
open import Delay-monad.Bisimilarity hiding (never≉now)
open import Delay-monad.Bisimilarity.Negative

------------------------------------------------------------------------
-- Proof programs

-- There are two kinds of proof "programs", corresponding to strong
-- and weak bisimilarity.

data Kind : Type where
  strong weak : Kind

mutual

  -- Proof "programs".

  data Prog (i : Size) : Kind → Delay A ∞ → Delay A ∞ → Type a where

    -- Congruences.

    now   : ∀ {k x} → Prog i k (now x) (now x)
    later : ∀ {k x y} →
            Prog′ i k (force x) (force y) →
            Prog i k (later x) (later y)

    -- Weak bisimilarity.

    laterʳ : ∀ {x y} → Prog i weak x (force y) → Prog i weak x (later y)
    laterˡ : ∀ {x y} → Prog i weak (force x) y → Prog i weak (later x) y

    -- Equational reasoning.
    --
    -- Note that if A is inhabited, then there is no size-preserving
    -- transitivity-like proof taking strong bisimilarity and weak
    -- bisimilarity to weak bisimilarity (see
    -- Delay-monad.Bisimilarity.Negative.size-preserving-transitivity-∼≈ˡ⇔uninhabited).

    reflP  : ∀ {k} x → Prog i k x x
    symP   : ∀ {k x y} → Prog i k x y → Prog i k y x
    transP : ∀ {k x y z} →
             Prog i strong x y → Prog i k y z → Prog i k x z

  record Prog′ (i : Size) (k : Kind) (x y : Delay A ∞) : Type a where
    coinductive
    field
      force : {j : Size< i} → Prog j k x y

open Prog′ public

------------------------------------------------------------------------
-- Completeness

-- Proof programs are complete with respect to strong and weak
-- bisimilarity. Note that these proofs are size-preserving.

complete-strong : ∀ {i x y} →
                  [ i ] x ∼ y → Prog i strong x y
complete-strong now       = now
complete-strong (later p) =
  later λ { .force → complete-strong (force p) }

complete-weak : ∀ {i x y} → [ i ] x ≈ y → Prog i weak x y
complete-weak now        = now
complete-weak (laterʳ p) = laterʳ (complete-weak p)
complete-weak (laterˡ p) = laterˡ (complete-weak p)
complete-weak (later  p) =
  later λ { .force → complete-weak (force p) }

------------------------------------------------------------------------
-- Soundness

-- Proof WHNFs.

data WHNF (i : Size) : Kind → Delay A ∞ → Delay A ∞ → Type a where
  now    : ∀ {k x} → WHNF i k (now x) (now x)
  later  : ∀ {k x y} →
           Prog′ i k (force x) (force y) →
           WHNF i k (later x) (later y)
  laterʳ : ∀ {x y} →
           WHNF i weak x (force y) → WHNF i weak x (later y)
  laterˡ : ∀ {x y} →
           WHNF i weak (force x) y → WHNF i weak (later x) y

-- Reflexivity.

reflW : ∀ {i k} x → WHNF i k x x
reflW (now   x) = now
reflW (later x) = later λ { .force → reflP (force x) }

-- Symmetry.

symW : ∀ {i k x y} → WHNF i k x y → WHNF i k y x
symW now        = now
symW (later  p) = later λ { .force → symP (force p) }
symW (laterʳ p) = laterˡ (symW p)
symW (laterˡ p) = laterʳ (symW p)

-- Transitivity for strong WHNFs.

trans∼∼W : ∀ {i x y z} →
           WHNF i strong x y → WHNF i strong y z → WHNF i strong x z
trans∼∼W now       q         = q
trans∼∼W (later p) (later q) =
  later λ { .force → transP (force p) (force q) }

-- Strong equality programs can be turned into WHNFs.

whnf∼ : ∀ {i x y} → Prog i strong x y → WHNF i strong x y
whnf∼ now          = now
whnf∼ (later p)    = later p
whnf∼ (reflP x)    = reflW x
whnf∼ (symP p)     = symW (whnf∼ p)
whnf∼ (transP p q) = trans∼∼W (whnf∼ p) (whnf∼ q)

-- Strong proof programs are sound with respect to strong
-- bisimilarity. Note that these proofs are size-preserving.

mutual

  sound-strong : ∀ {i x y} →
                 Prog i strong x y → [ i ] x ∼ y
  sound-strong p = soundW-strong (whnf∼ p)

  soundW-strong : ∀ {i x y} →
                  WHNF i strong x y → [ i ] x ∼ y
  soundW-strong now       = now
  soundW-strong (later p) =
    later λ { .force → sound-strong (force p) }

-- Another transitivity lemma. This lemma cannot, in general, be made
-- fully size-preserving (see not-fully-size-preserving below).

trans∼-W : ∀ {i k x y z} →
           WHNF ∞ strong x y → WHNF i k y z → WHNF i k x z
trans∼-W now       q          = q
trans∼-W p         (laterʳ q) = laterʳ (trans∼-W p q)
trans∼-W (later p) (laterˡ q) = laterˡ (trans∼-W (whnf∼ (force p)) q)
trans∼-W (later p) (later  q) =
  later λ { .force → transP (force p) (force q) }

-- All fully defined programs can be turned into WHNFs.

whnf : ∀ {i k x y} → Prog ∞ k x y → WHNF i k x y
whnf now          = now
whnf (later p)    = later p
whnf (laterʳ p)   = laterʳ (whnf p)
whnf (laterˡ p)   = laterˡ (whnf p)
whnf (reflP x)    = reflW x
whnf (symP p)     = symW (whnf p)
whnf (transP p q) = trans∼-W (whnf p) (whnf q)

-- Weak proof programs are sound with respect to weak bisimilarity.
-- Note that these proofs are /not/ guaranteed to be size-preserving.

mutual

  sound-weak : ∀ {i x y} → Prog ∞ weak x y → [ i ] x ≈ y
  sound-weak p = soundW-weak (whnf p)

  soundW-weak : ∀ {i x y} → WHNF ∞ weak x y → [ i ] x ≈ y
  soundW-weak now        = now
  soundW-weak (laterʳ p) = laterʳ  (soundW-weak p)
  soundW-weak (laterˡ p) = laterˡ  (soundW-weak p)
  soundW-weak (later  p) =
    later λ { .force → sound-weak (force p) }

------------------------------------------------------------------------
-- Some negative results

-- The soundness proof for weak proof programs can be made
-- size-preserving iff A is uninhabited.

size-preserving⇔uninhabited :
  (∀ {i x y} → Prog i weak x y → [ i ] x ≈ y) ⇔ ¬ A
size-preserving⇔uninhabited = record
  { to   = (∀ {i x y} → Prog i weak x y → [ i ] x ≈ y)  ↝⟨ (λ sound p q → sound (transP (complete-strong p) (complete-weak q))) ⟩
           Transitivity-∼≈ˡ                             ↝⟨ _⇔_.to size-preserving-transitivity-∼≈ˡ⇔uninhabited ⟩□
           ¬ A                                          □
  ; from = ¬ A                                          ↝⟨ uninhabited→trivial ⟩
           (∀ x y → x ≈ y)                              ↝⟨ (λ trivial {_ _ _} _ → trivial _ _) ⟩□
           (∀ {i x y} → Prog i weak x y → [ i ] x ≈ y)  □
  }

-- The lemma trans∼-W cannot be made fully size-preserving (assuming
-- that A is inhabited).

not-fully-size-preserving :
  (∀ {i k x y z} →
   WHNF i strong x y → WHNF i k y z → WHNF i k x z) →
  ¬ A
not-fully-size-preserving trans x = contradiction ∞
  where

  never≉now : ∀ {i} → ¬ WHNF i weak never (now x)
  never≉now (laterˡ p) = never≉now p

  mutual

    never≈now : ∀ {i} → WHNF i weak never (now x)
    never≈now =
      trans (later {y = record { force = now x }} never∼now)
            (laterˡ now)

    never∼now : ∀ {i} → Prog′ i strong never (now x)
    force never∼now {j = j} = ⊥-elim (contradiction j)

    contradiction : Size → ⊥
    contradiction i = never≉now (never≈now {i = i})

-- One might wonder why the counterexample above cannot be adapted so
-- that it also applies to programs, for which a size-preserving
-- transitivity constructor exists. The following lemma documents one
-- attempt at adapting the counterexample. Note that the new
-- counterexample is based on the assumption that one can convert a
-- strong bisimilarity program /of any size/ relating never and x to a
-- proof that x is /equal/ to never.

partially-adapted-counterexample :
  (∀ {i x} → Prog i strong never x → x ≡ never) →
  ¬ A
partially-adapted-counterexample convert x = contradiction ∞
  where
  mutual

    now∼→≡now : ∀ {i x y} → Prog i strong (now x) y → y ≡ now x
    now∼→≡now now          = refl
    now∼→≡now (reflP _)    = refl
    now∼→≡now (symP p)     = ∼now→≡now p
    now∼→≡now (transP p q) rewrite now∼→≡now p = now∼→≡now q

    ∼now→≡now : ∀ {i x y} → Prog i strong x (now y) → x ≡ now y
    ∼now→≡now now          = refl
    ∼now→≡now (reflP _)    = refl
    ∼now→≡now (symP p)     = now∼→≡now p
    ∼now→≡now (transP p q) rewrite ∼now→≡now q = ∼now→≡now p

  mutual

    now≉Pnever : ∀ {i} → ¬ Prog i weak (now x) never
    now≉Pnever (laterʳ p)   = now≉Pnever p
    now≉Pnever (symP p)     = never≉Pnow p
    now≉Pnever (transP p q) rewrite now∼→≡now p = now≉Pnever q

    never≉Pnow : ∀ {i} → ¬ Prog i weak never (now x)
    never≉Pnow (laterˡ p)   = never≉Pnow p
    never≉Pnow (symP p)     = now≉Pnever p
    never≉Pnow (transP p q) rewrite convert p = never≉Pnow q

  mutual

    never≈Pnow : ∀ {i} → Prog i weak never (now x)
    never≈Pnow =
      transP (later {y = record { force = now x }} never∼Pnow)
             (laterˡ now)

    never∼Pnow : ∀ {i} → Prog′ i strong never (now x)
    force never∼Pnow {j = j} = ⊥-elim (contradiction j)

    contradiction : Size → ⊥
    contradiction i = never≉Pnow (never≈Pnow {i = i})

------------------------------------------------------------------------
-- A contrived example

-- Note the use of a strong bisimilarity program of size i as the
-- first argument to transitivity in the following example; this is
-- not supported by transitive-∼ˡ, which requires the first argument
-- to have size ∞.

exampleP : ∀ {i} → Prog i weak never never
exampleP {i} =
  transP (reflP {i = i} never) (later λ { .force → exampleP })

example : ∀ {i} → [ i ] never ≈ never
example = sound-weak exampleP

-- However, note that the first argument could just as well have been
-- given the size ∞, in which case transitive-∼ˡ works:

counterargument : ∀ {i} → [ i ] never ≈ never {A = A}
counterargument =
  transitive-∼ˡ (reflexive never)
                (later λ { .force → counterargument })

-- Are there any applications in which strong and weak bisimilarities
-- are proved simultaneously? One can observe that, if the first
-- argument is never, then weak bisimilarity is contained in strong
-- (in a size-preserving way), as witnessed by →∼-neverˡ. Perhaps one
-- can find some compelling application of the technique presented
-- above if it can be combined with a lemma like →∼-neverˡ. However,
-- it is unclear if such a combination is possible: the soundness
-- proof above relies on the fact that strong bisimilarity programs
-- contain no weak bisimilarity programs (in particular, no
-- transitivity proofs with a weak bisimilarity as the second
-- argument).

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


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

module 10-truncation-levels where

import 09-fundamental-theorem
open 09-fundamental-theorem public

-- Section 8.1 Propositions

is-prop :
  {i : Level} (A : UU i) → UU i
is-prop A = (x y : A) → is-contr (Id x y)

{- We introduce the universe of all propositions. -}
UU-Prop :
  (l : Level) → UU (lsuc l)
UU-Prop l = Σ (UU l) is-prop

type-Prop :
  {l : Level} → UU-Prop l → UU l
type-Prop P = pr1 P

is-prop-type-Prop :
  {l : Level} (P : UU-Prop l) → is-prop (type-Prop P)
is-prop-type-Prop P = pr2 P

{- The empty type is a proposition. -}

abstract
  is-prop-empty : is-prop empty
  is-prop-empty ()

abstract
  is-prop-unit : is-prop unit
  is-prop-unit = is-prop-is-contr is-contr-unit

unit-Prop : UU-Prop lzero
unit-Prop = pair unit is-prop-unit

is-prop' :
  {i : Level} (A : UU i) → UU i
is-prop' A = (x y : A) → Id x y

abstract
  is-prop-is-prop' :
    {i : Level} {A : UU i} → is-prop' A → is-prop A
  is-prop-is-prop' {i} {A} H x y =
    pair
      ( (inv (H x x)) ∙ (H x y))
      ( ind-Id x
        ( λ z p → Id ((inv (H x x)) ∙ (H x z)) p)
        ( left-inv (H x x)) y)

abstract
  is-prop'-is-prop :
    {i : Level} {A : UU i} → is-prop A → is-prop' A
  is-prop'-is-prop H x y = pr1 (H x y)

abstract
  is-contr-is-prop-inh :
    {i : Level} {A : UU i} → is-prop A → A → is-contr A
  is-contr-is-prop-inh H a = pair a (is-prop'-is-prop H a)

abstract
  is-prop-is-contr-if-inh :
    {i : Level} {A : UU i} → (A → is-contr A) → is-prop A
  is-prop-is-contr-if-inh H x y = is-prop-is-contr (H x) x y

is-subtype :
  {i j : Level} {A : UU i} (B : A → UU j) → UU (i ⊔ j)
is-subtype B = (x : _) → is-prop (B x)

double-structure-swap :
  {l1 l2 l3 : Level} (A : UU l1) (B : A → UU l2) (C : A → UU l3) →
  Σ (Σ A B) (λ t → C (pr1 t)) → Σ (Σ A C) (λ t → B (pr1 t))
double-structure-swap A B C (pair (pair a b) c) = (pair (pair a c) b)

htpy-double-structure-swap :
  {l1 l2 l3 : Level} (A : UU l1) (B : A → UU l2) (C : A → UU l3) →
  ((double-structure-swap A C B) ∘ (double-structure-swap A B C)) ~ id
htpy-double-structure-swap A B C (pair (pair a b) c) =
  eq-pair (eq-pair refl refl) refl

is-equiv-double-structure-swap :
  {l1 l2 l3 : Level} (A : UU l1) (B : A → UU l2) (C : A → UU l3) →
  is-equiv (double-structure-swap A B C)
is-equiv-double-structure-swap A B C =
  is-equiv-has-inverse
    ( double-structure-swap A C B)
    ( htpy-double-structure-swap A C B)
    ( htpy-double-structure-swap A B C)

{- The following is a general construction that will help us show that
   the identity type of a subtype agrees with the identity type of the
   original type. We already know that the first projection of a family of
   propositions is an embedding, but the following lemma still has its uses. -}

abstract
  is-contr-total-Eq-substructure :
    {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {P : A → UU l3} →
    is-contr (Σ A B) → (is-subtype P) → (a : A) (b : B a) (p : P a) →
    is-contr (Σ (Σ A P) (λ t → B (pr1 t)))
  is-contr-total-Eq-substructure {A = A} {B} {P}
    is-contr-AB is-subtype-P a b p =
    is-contr-is-equiv
      ( Σ (Σ A B) (λ t → P (pr1 t)))
      ( double-structure-swap A P B)
      ( is-equiv-double-structure-swap A P B)
      ( is-contr-is-equiv'
        ( P a)
        ( left-unit-law-Σ-map-gen (λ t → P (pr1 t)) is-contr-AB (pair a b))
        ( is-equiv-left-unit-law-Σ-map-gen _ is-contr-AB (pair a b))
        ( is-contr-is-prop-inh (is-subtype-P a) p))

Eq-total-subtype :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} → is-subtype B →
  (Σ A B) → (Σ A B) → UU l1
Eq-total-subtype is-subtype-B p p' = Id (pr1 p) (pr1 p')

reflexive-Eq-total-subtype :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (is-subtype-B : is-subtype B) →
  (p : Σ A B) → Eq-total-subtype is-subtype-B p p
reflexive-Eq-total-subtype is-subtype-B (pair x y) = refl

Eq-total-subtype-eq :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (is-subtype-B : is-subtype B) →
  (p p' : Σ A B) → Id p p' → Eq-total-subtype is-subtype-B p p'
Eq-total-subtype-eq is-subtype-B p .p refl =
  reflexive-Eq-total-subtype is-subtype-B p

is-contr-total-Eq-total-subtype :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (is-subtype-B : is-subtype B) →
  (p : Σ A B) → is-contr (Σ (Σ A B) (Eq-total-subtype is-subtype-B p))
is-contr-total-Eq-total-subtype is-subtype-B (pair x y) =
  is-contr-total-Eq-substructure
    ( is-contr-total-path x)
    ( is-subtype-B)
    x refl y

is-equiv-Eq-total-subtype-eq :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (is-subtype-B : is-subtype B) →
  (p p' : Σ A B) → is-equiv (Eq-total-subtype-eq is-subtype-B p p')
is-equiv-Eq-total-subtype-eq is-subtype-B p =
  fundamental-theorem-id p
    ( reflexive-Eq-total-subtype is-subtype-B p)
    ( is-contr-total-Eq-total-subtype is-subtype-B p)
    ( Eq-total-subtype-eq is-subtype-B p)

eq-subtype :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (is-subtype-B : is-subtype B) →
  {p p' : Σ A B} → Eq-total-subtype is-subtype-B p p' → Id p p'
eq-subtype is-subtype-B {p} {p'} =
  inv-is-equiv (is-equiv-Eq-total-subtype-eq is-subtype-B p p')

-- Section 8.2 Sets

is-set :
  {i : Level} → UU i → UU i
is-set A = (x y : A) → is-prop (Id x y)

UU-Set :
  (i : Level) → UU (lsuc i)
UU-Set i = Σ (UU i) is-set

type-Set :
  {l : Level} → UU-Set l → UU l
type-Set X = pr1 X

is-set-type-Set :
  {l : Level} (X : UU-Set l) → is-set (type-Set X)
is-set-type-Set X = pr2 X

axiom-K :
  {i : Level} → UU i → UU i
axiom-K A = (x : A) (p : Id x x) → Id refl p

abstract
  is-set-axiom-K :
    {i : Level} (A : UU i) → axiom-K A → is-set A
  is-set-axiom-K A H x y =
    is-prop-is-prop' (ind-Id x (λ z p → (q : Id x z) → Id p q) (H x) y)

abstract
  axiom-K-is-set :
    {i : Level} (A : UU i) → is-set A → axiom-K A
  axiom-K-is-set A H x p =
    ( inv (contraction (is-contr-is-prop-inh (H x x) refl) refl)) ∙
    ( contraction (is-contr-is-prop-inh (H x x) refl) p)

abstract
  is-equiv-prop-in-id :
    {i j : Level} {A : UU i}
    (R : A → A → UU j)
    (p : (x y : A) → is-prop (R x y))
    (ρ : (x : A) → R x x)
    (i : (x y : A) → R x y → Id x y) →
    (x y : A) → is-equiv (i x y)
  is-equiv-prop-in-id R p ρ i x =
    fundamental-theorem-id-retr x (i x)
      (λ y → pair
        (ind-Id x (λ z p → R x z) (ρ x) y)
        ((λ r → is-prop'-is-prop (p x y) _ r)))

abstract
  is-prop-is-equiv :
    {i j : Level} {A : UU i} (B : UU j) (f : A → B) (E : is-equiv f) →
    is-prop B → is-prop A
  is-prop-is-equiv B f E H x y =
    is-contr-is-equiv _ (ap f {x} {y}) (is-emb-is-equiv f E x y) (H (f x) (f y))

abstract
  is-prop-is-equiv' :
    {i j : Level} (A : UU i) {B : UU j} (f : A → B) (E : is-equiv f) →
    is-prop A → is-prop B
  is-prop-is-equiv' A f E H =
    is-prop-is-equiv _ (inv-is-equiv E) (is-equiv-inv-is-equiv E) H

abstract
  is-set-prop-in-id :
    {i j : Level} {A : UU i} (R : A → A → UU j)
    (p : (x y : A) → is-prop (R x y))
    (ρ : (x : A) → R x x)
    (i : (x y : A) → R x y → Id x y) →
    is-set A
  is-set-prop-in-id R p ρ i x y =
    is-prop-is-equiv'
      ( R x y)
      ( i x y)
      ( is-equiv-prop-in-id R p ρ i x y) (p x y)

abstract
  is-prop-Eq-ℕ :
    (n m : ℕ) → is-prop (Eq-ℕ n m)
  is-prop-Eq-ℕ zero-ℕ zero-ℕ = is-prop-unit
  is-prop-Eq-ℕ zero-ℕ (succ-ℕ m) = is-prop-empty
  is-prop-Eq-ℕ (succ-ℕ n) zero-ℕ = is-prop-empty
  is-prop-Eq-ℕ (succ-ℕ n) (succ-ℕ m) = is-prop-Eq-ℕ n m

abstract
  eq-Eq-ℕ : (n m : ℕ) → Eq-ℕ n m → Id n m
  eq-Eq-ℕ = least-reflexive-Eq-ℕ Id (λ n → refl)

abstract
  is-set-ℕ : is-set ℕ
  is-set-ℕ =
    is-set-prop-in-id
      Eq-ℕ
      is-prop-Eq-ℕ
      refl-Eq-ℕ
      eq-Eq-ℕ

set-ℕ : UU-Set lzero
set-ℕ = pair ℕ is-set-ℕ

-- Section 8.3 General truncation levels

data 𝕋 : UU lzero where
  neg-two-𝕋 : 𝕋
  succ-𝕋 : 𝕋 → 𝕋

neg-one-𝕋 : 𝕋
neg-one-𝕋 = succ-𝕋 (neg-two-𝕋)

zero-𝕋 : 𝕋
zero-𝕋 = succ-𝕋 (neg-one-𝕋)

one-𝕋 : 𝕋
one-𝕋 = succ-𝕋 (zero-𝕋)

ℕ-in-𝕋 : ℕ → 𝕋
ℕ-in-𝕋 zero-ℕ = zero-𝕋
ℕ-in-𝕋 (succ-ℕ n) = succ-𝕋 (ℕ-in-𝕋 n)

-- Probably it is better to define this where we first need it.
add-𝕋 : 𝕋 → 𝕋 → 𝕋
add-𝕋 neg-two-𝕋 neg-two-𝕋 = neg-two-𝕋
add-𝕋 neg-two-𝕋 (succ-𝕋 neg-two-𝕋) = neg-two-𝕋
add-𝕋 neg-two-𝕋 (succ-𝕋 (succ-𝕋 y)) = y
add-𝕋 (succ-𝕋 neg-two-𝕋) neg-two-𝕋 = neg-two-𝕋
add-𝕋 (succ-𝕋 neg-two-𝕋) (succ-𝕋 y) = y
add-𝕋 (succ-𝕋 (succ-𝕋 neg-two-𝕋)) y = y
add-𝕋 (succ-𝕋 (succ-𝕋 (succ-𝕋 x))) y = succ-𝕋 (add-𝕋 (succ-𝕋 (succ-𝕋 x)) y)

is-trunc : {i : Level} (k : 𝕋) → UU i → UU i
is-trunc neg-two-𝕋 A = is-contr A
is-trunc (succ-𝕋 k) A = (x y : A) → is-trunc k (Id x y)

1-type : (l : Level) → UU (lsuc l)
1-type l = Σ (UU l) (is-trunc one-𝕋)

_Truncated-Type_ : 𝕋 → (l : Level) → UU (lsuc l)
k Truncated-Type l = Σ (UU l) (is-trunc k)

abstract
  is-trunc-succ-is-trunc :
    {i : Level} (k : 𝕋) (A : UU i) →
    is-trunc k A → is-trunc (succ-𝕋 k) A
  is-trunc-succ-is-trunc neg-two-𝕋 A H = is-prop-is-contr H
  is-trunc-succ-is-trunc (succ-𝕋 k) A H x y =
    is-trunc-succ-is-trunc k (Id x y) (H x y)

truncated-type-succ-𝕋 :
  (l : Level) (k : 𝕋) → k Truncated-Type l → (succ-𝕋 k) Truncated-Type l
truncated-type-succ-𝕋 l k (pair A is-trunc-A) =
  pair A (is-trunc-succ-is-trunc k A is-trunc-A)

abstract
  is-trunc-is-equiv :
    {i j : Level} (k : 𝕋) {A : UU i} (B : UU j) (f : A → B) → is-equiv f →
    is-trunc k B → is-trunc k A
  is-trunc-is-equiv neg-two-𝕋 B f is-equiv-f H =
    is-contr-is-equiv B f is-equiv-f H
  is-trunc-is-equiv (succ-𝕋 k) B f is-equiv-f H x y =
    is-trunc-is-equiv k (Id (f x) (f y)) (ap f {x} {y})
      (is-emb-is-equiv f is-equiv-f x y) (H (f x) (f y))

abstract
  is-set-is-equiv :
    {i j : Level} {A : UU i} (B : UU j) (f : A → B) → is-equiv f →
    is-set B → is-set A
  is-set-is-equiv = is-trunc-is-equiv zero-𝕋

abstract
  is-trunc-equiv :
    {i j : Level} (k : 𝕋) {A : UU i} (B : UU  j) (e : A ≃ B) →
    is-trunc k B → is-trunc k A
  is-trunc-equiv k B (pair f is-equiv-f) =
    is-trunc-is-equiv k B f is-equiv-f

abstract
  is-set-equiv :
    {i j : Level} {A : UU i} (B : UU j) (e : A ≃ B) →
    is-set B → is-set A
  is-set-equiv = is-trunc-equiv zero-𝕋

abstract
  is-trunc-is-equiv' :
    {i j : Level} (k : 𝕋) (A : UU i) {B : UU j} (f : A → B) →
    is-equiv f → is-trunc k A → is-trunc k B
  is-trunc-is-equiv' k A  f is-equiv-f is-trunc-A =
    is-trunc-is-equiv k A
      ( inv-is-equiv is-equiv-f)
      ( is-equiv-inv-is-equiv is-equiv-f)
      ( is-trunc-A)

abstract
  is-set-is-equiv' :
    {i j : Level} (A : UU i) {B : UU j} (f : A → B) → is-equiv f →
    is-set A → is-set B
  is-set-is-equiv' = is-trunc-is-equiv' zero-𝕋

abstract
  is-trunc-equiv' :
    {i j : Level} (k : 𝕋) (A : UU i) {B : UU j} (e : A ≃ B) →
    is-trunc k A → is-trunc k B
  is-trunc-equiv' k A (pair f is-equiv-f) =
    is-trunc-is-equiv' k A f is-equiv-f

abstract
  is-set-equiv' :
    {i j : Level} (A : UU i) {B : UU j} (e : A ≃ B) →
    is-set A → is-set B
  is-set-equiv' = is-trunc-equiv' zero-𝕋

abstract
  is-trunc-succ-is-emb : {i j : Level} (k : 𝕋) {A : UU i} {B : UU j}
    (f : A → B) → is-emb f → is-trunc (succ-𝕋 k) B → is-trunc (succ-𝕋 k) A
  is-trunc-succ-is-emb k f Ef H x y =
    is-trunc-is-equiv k (Id (f x) (f y)) (ap f {x} {y}) (Ef x y) (H (f x) (f y))

is-trunc-map :
  {i j : Level} (k : 𝕋) {A : UU i} {B : UU j} → (A → B) → UU (i ⊔ j)
is-trunc-map k f = (y : _) → is-trunc k (fib f y)

trunc-map : {i j : Level} (k : 𝕋) (A : UU i) (B : UU j) → UU (i ⊔ j)
trunc-map k A B = Σ (A → B) (is-trunc-map k)

abstract
  is-trunc-pr1-is-trunc-fam :
    {i j : Level} (k : 𝕋) {A : UU i} (B : A → UU j) →
    ((x : A) → is-trunc k (B x)) → is-trunc-map k (pr1 {i} {j} {A} {B})
  is-trunc-pr1-is-trunc-fam k B H x =
    is-trunc-is-equiv k
      ( B x)
      ( fib-fam-fib-pr1 B x)
      ( is-equiv-fib-fam-fib-pr1 B x)
      ( H x)

trunc-pr1 :
  {i j : Level} (k : 𝕋) {A : UU i} (B : A → k Truncated-Type j) →
  trunc-map k (Σ A (λ x → pr1 (B x))) A
trunc-pr1 k B =
  pair pr1 (is-trunc-pr1-is-trunc-fam k (λ x → pr1 (B x)) (λ x → pr2 (B x)))

abstract
  is-trunc-fam-is-trunc-pr1 : {i j : Level} (k : 𝕋) {A : UU i} (B : A → UU j) →
    is-trunc-map k (pr1 {i} {j} {A} {B}) → ((x : A) → is-trunc k (B x))
  is-trunc-fam-is-trunc-pr1 k B is-trunc-pr1 x =
    is-trunc-is-equiv k
      ( fib pr1 x)
      ( fib-pr1-fib-fam B x)
      ( is-equiv-fib-pr1-fib-fam B x)
      ( is-trunc-pr1 x)

abstract
  is-trunc-map-is-trunc-ap : {i j : Level} (k : 𝕋) {A : UU i} {B : UU j}
    (f : A → B) → ((x y : A) → is-trunc-map k (ap f {x = x} {y = y})) →
    is-trunc-map (succ-𝕋 k) f
  is-trunc-map-is-trunc-ap k f is-trunc-ap-f b (pair x p) (pair x' p') =
    is-trunc-is-equiv k
      ( fib (ap f) (p ∙ (inv p')))
      ( fib-ap-eq-fib f (pair x p) (pair x' p'))
      ( is-equiv-fib-ap-eq-fib f (pair x p) (pair x' p'))
      ( is-trunc-ap-f x x' (p ∙ (inv p')))

abstract
  is-trunc-ap-is-trunc-map : {i j : Level} (k : 𝕋) {A : UU i} {B : UU j}
    (f : A → B) → is-trunc-map (succ-𝕋 k) f →
    (x y : A) → is-trunc-map k (ap f {x = x} {y = y})
  is-trunc-ap-is-trunc-map k f is-trunc-map-f x y p =
    is-trunc-is-equiv' k
      ( Id (pair x p) (pair y refl))
      ( eq-fib-fib-ap f x y p)
      ( is-equiv-eq-fib-fib-ap f x y p)
      ( is-trunc-map-f (f y) (pair x p) (pair y refl))

is-prop-map : {i j : Level} {A : UU i} {B : UU j} (f : A → B) → UU (i ⊔ j)
is-prop-map f = (b : _) → is-trunc neg-one-𝕋 (fib f b)

abstract
  is-emb-is-prop-map : {i j : Level} {A : UU i} {B : UU j} (f : A → B) →
    is-prop-map f → is-emb f
  is-emb-is-prop-map f is-prop-map-f x y =
    is-equiv-is-contr-map
      ( is-trunc-ap-is-trunc-map neg-two-𝕋 f is-prop-map-f x y)

abstract
  is-prop-map-is-emb : {i j : Level} {A : UU i} {B : UU j} (f : A → B) →
    is-emb f → is-prop-map f
  is-prop-map-is-emb f is-emb-f =
    is-trunc-map-is-trunc-ap neg-two-𝕋 f
      ( λ x y → is-contr-map-is-equiv (is-emb-f x y))

abstract
  is-emb-pr1-is-subtype : {i j : Level} {A : UU i} {B : A → UU j} →
    is-subtype B → is-emb (pr1 {B = B})
  is-emb-pr1-is-subtype {B = B} is-subtype-B =
    is-emb-is-prop-map pr1
      ( λ x → is-trunc-is-equiv neg-one-𝕋
        ( B x)
        ( fib-fam-fib-pr1 _ x)
        ( is-equiv-fib-fam-fib-pr1 _ x)
        ( is-subtype-B x))

equiv-ap-pr1-is-subtype : {i j : Level} {A : UU i} {B : A → UU j} →
  is-subtype B → {s t : Σ A B} → Id s t ≃ Id (pr1 s) (pr1 t)
equiv-ap-pr1-is-subtype is-subtype-B {s} {t} =
  pair
    ( ap pr1)
    ( is-emb-pr1-is-subtype is-subtype-B s t)

abstract
  is-subtype-is-emb-pr1 : {i j : Level} {A : UU i} {B : A → UU j} →
    is-emb (pr1 {B = B}) → is-subtype B
  is-subtype-is-emb-pr1 is-emb-pr1-B x =
    is-trunc-is-equiv neg-one-𝕋
      ( fib pr1 x)
      ( fib-pr1-fib-fam _ x)
      ( is-equiv-fib-pr1-fib-fam _ x)
      ( is-prop-map-is-emb pr1 is-emb-pr1-B x)

is-fiberwise-trunc : {l1 l2 l3 : Level} (k : 𝕋)  {A : UU l1} {B : A → UU l2}
  {C : A → UU l3} (f : (x : A) → B x → C x) → UU (l1 ⊔ (l2 ⊔ l3))
is-fiberwise-trunc k f = (x : _) → is-trunc-map k (f x)

abstract
  is-trunc-tot-is-fiberwise-trunc : {l1 l2 l3 : Level} (k : 𝕋)
    {A : UU l1} {B : A → UU l2} {C : A → UU l3} (f : (x : A) → B x → C x) →
    is-fiberwise-trunc k f → is-trunc-map k (tot f)
  is-trunc-tot-is-fiberwise-trunc k f is-fiberwise-trunc-f (pair x z) =
    is-trunc-is-equiv k
      ( fib (f x) z)
      ( fib-ftr-fib-tot f (pair x z))
      ( is-equiv-fib-ftr-fib-tot f (pair x z))
      ( is-fiberwise-trunc-f x z)

abstract
  is-fiberwise-trunc-is-trunc-tot : {l1 l2 l3 : Level} (k : 𝕋)
    {A : UU l1} {B : A → UU l2} {C : A → UU l3} (f : (x : A) → B x → C x) →
    is-trunc-map k (tot f) → is-fiberwise-trunc k f
  is-fiberwise-trunc-is-trunc-tot k f is-trunc-tot-f x z =
    is-trunc-is-equiv k
      ( fib (tot f) (pair x z))
      ( fib-tot-fib-ftr f (pair x z))
      ( is-equiv-fib-tot-fib-ftr f (pair x z))
      ( is-trunc-tot-f (pair x z))

-- Exercises

-- Exercise 8.1

-- Exercise 8.1

diagonal : {l : Level} (A : UU l) → A → A × A
diagonal A x = pair x x

abstract
  is-prop-is-equiv-diagonal : {l : Level} (A : UU l) →
    is-equiv (diagonal A) → is-prop A
  is-prop-is-equiv-diagonal A is-equiv-d =
    is-prop-is-prop' ( λ x y →
      let α = issec-inv-is-equiv is-equiv-d (pair x y) in
      ( inv (ap pr1 α)) ∙ (ap pr2 α))

eq-fib-diagonal : {l : Level} (A : UU l) (t : A × A) →
  fib (diagonal A) t → Id (pr1 t) (pr2 t)
eq-fib-diagonal A (pair x y) (pair z α) = (inv (ap pr1 α)) ∙ (ap pr2 α)

fib-diagonal-eq : {l : Level} (A : UU l) (t : A × A) →
  Id (pr1 t) (pr2 t) → fib (diagonal A) t
fib-diagonal-eq A (pair x y) β =
  pair x (eq-pair-triv (pair refl β))

issec-fib-diagonal-eq : {l : Level} (A : UU l) (t : A × A) →
  ((eq-fib-diagonal A t) ∘ (fib-diagonal-eq A t)) ~ id
issec-fib-diagonal-eq A (pair x .x) refl = refl

isretr-fib-diagonal-eq : {l : Level} (A : UU l) (t : A × A) →
  ((fib-diagonal-eq A t) ∘ (eq-fib-diagonal A t)) ~ id
isretr-fib-diagonal-eq A .(pair z z) (pair z refl) = refl

abstract
  is-equiv-eq-fib-diagonal : {l : Level} (A : UU l) (t : A × A) →
    is-equiv (eq-fib-diagonal A t)
  is-equiv-eq-fib-diagonal A t =
    is-equiv-has-inverse
      ( fib-diagonal-eq A t)
      ( issec-fib-diagonal-eq A t)
      ( isretr-fib-diagonal-eq A t)

abstract
  is-trunc-is-trunc-diagonal : {l : Level} (k : 𝕋) (A : UU l) →
    is-trunc-map k (diagonal A) → is-trunc (succ-𝕋 k) A
  is-trunc-is-trunc-diagonal k A is-trunc-d x y =
    is-trunc-is-equiv' k
      ( fib (diagonal A) (pair x y))
      ( eq-fib-diagonal A (pair x y))
      ( is-equiv-eq-fib-diagonal A (pair x y))
      ( is-trunc-d (pair x y))

abstract
  is-trunc-diagonal-is-trunc : {l : Level} (k : 𝕋) (A : UU l) →
    is-trunc (succ-𝕋 k) A → is-trunc-map k (diagonal A)
  is-trunc-diagonal-is-trunc k A is-trunc-A t =
    is-trunc-is-equiv k
      ( Id (pr1 t) (pr2 t))
      ( eq-fib-diagonal A t)
      ( is-equiv-eq-fib-diagonal A t)
      ( is-trunc-A (pr1 t) (pr2 t))

-- Exercise 8.2

-- Exercise 8.2(a)

abstract
  is-trunc-Σ : {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : A → UU l2} →
    is-trunc k A → ((x : A) → is-trunc k (B x)) → is-trunc k (Σ A B)
  is-trunc-Σ neg-two-𝕋 is-trunc-A is-trunc-B =
    is-contr-Σ is-trunc-A is-trunc-B
  is-trunc-Σ (succ-𝕋 k) {B = B} is-trunc-A is-trunc-B s t =
    is-trunc-is-equiv k
      ( Σ (Id (pr1 s) (pr1 t)) (λ p → Id (tr B p (pr2 s)) (pr2 t)))
      ( pair-eq)
      ( is-equiv-pair-eq s t)
      ( is-trunc-Σ k
        ( is-trunc-A (pr1 s) (pr1 t))
        ( λ p → is-trunc-B (pr1 t) (tr B p (pr2 s)) (pr2 t)))

abstract
  is-trunc-prod : {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} →
    is-trunc k A → is-trunc k B → is-trunc k (A × B)
  is-trunc-prod k is-trunc-A is-trunc-B =
    is-trunc-Σ k is-trunc-A (λ x → is-trunc-B)

abstract
  is-prop-Σ : {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
    is-prop A → is-subtype B → is-prop (Σ A B)
  is-prop-Σ = is-trunc-Σ neg-one-𝕋

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

abstract
  is-prop-prod : {l1 l2 : Level} {A : UU l1} {B : UU l2} →
    is-prop A → is-prop B → is-prop (A × B)
  is-prop-prod = is-trunc-prod neg-one-𝕋

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

abstract
  is-set-Σ : {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
    is-set A → ((x : A) → is-set (B x)) → is-set (Σ A B)
  is-set-Σ = is-trunc-Σ zero-𝕋

set-Σ :
  {l1 l2 : Level} (A : UU-Set l1) (B : pr1 A → UU-Set l2) → UU-Set (l1 ⊔ l2)
set-Σ (pair A is-set-A) B =
  pair
    ( Σ A (λ x → (pr1 (B x))))
    ( is-set-Σ is-set-A (λ x → pr2 (B x)))

abstract
  is-set-prod : {l1 l2 : Level} {A : UU l1} {B : UU l2} →
    is-set A → is-set B → is-set (A × B)
  is-set-prod = is-trunc-prod zero-𝕋

set-prod :
  {l1 l2 : Level} (A : UU-Set l1) (B : UU-Set l2) → UU-Set (l1 ⊔ l2)
set-prod (pair A is-set-A) (pair B is-set-B) =
  pair (A × B) (is-set-prod is-set-A is-set-B)

-- Exercise 8.2 (b)

abstract
  is-trunc-Id : {l : Level} (k : 𝕋) {A : UU l} →
    is-trunc k A → (x y : A) → is-trunc k (Id x y)
  is-trunc-Id neg-two-𝕋 is-trunc-A = is-prop-is-contr is-trunc-A
  is-trunc-Id (succ-𝕋 k) is-trunc-A x y =
    is-trunc-succ-is-trunc k (Id x y) (is-trunc-A x y)

-- Exercise 8.2 (c)

abstract
  is-trunc-map-is-trunc-domain-codomain : {l1 l2 : Level} (k : 𝕋) {A : UU l1}
    {B : UU l2} {f : A → B} → is-trunc k A → is-trunc k B → is-trunc-map k f
  is-trunc-map-is-trunc-domain-codomain k {f = f} is-trunc-A is-trunc-B b =
    is-trunc-Σ k is-trunc-A (λ x → is-trunc-Id k is-trunc-B (f x) b)

-- Exercise 8.2 (d)

abstract
  is-trunc-fam-is-trunc-Σ :
    {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : A → UU l2} →
    is-trunc k A → is-trunc k (Σ A B) → (x : A) → is-trunc k (B x)
  is-trunc-fam-is-trunc-Σ k {B = B} is-trunc-A is-trunc-ΣAB x =
    is-trunc-is-equiv' k
      ( fib pr1 x)
      ( fib-fam-fib-pr1 B x)
      ( is-equiv-fib-fam-fib-pr1 B x)
      ( is-trunc-map-is-trunc-domain-codomain k is-trunc-ΣAB is-trunc-A x)

-- Exercise 8.3

abstract
  is-prop-Eq-𝟚 : (x y : bool) → is-prop (Eq-𝟚 x y)
  is-prop-Eq-𝟚 true true = is-prop-unit
  is-prop-Eq-𝟚 true false = is-prop-empty
  is-prop-Eq-𝟚 false true = is-prop-empty
  is-prop-Eq-𝟚 false false = is-prop-unit

abstract
  eq-Eq-𝟚 : (x y : bool) → Eq-𝟚 x y → Id x y
  eq-Eq-𝟚 true true star = refl
  eq-Eq-𝟚 true false ()
  eq-Eq-𝟚 false true ()
  eq-Eq-𝟚 false false star = refl

abstract
  is-set-bool : is-set bool
  is-set-bool = is-set-prop-in-id Eq-𝟚 is-prop-Eq-𝟚 reflexive-Eq-𝟚 eq-Eq-𝟚

set-bool : UU-Set lzero
set-bool = pair bool is-set-bool

-- Exercise 8.4

abstract
  is-trunc-succ-empty : (k : 𝕋) → is-trunc (succ-𝕋 k) empty
  is-trunc-succ-empty k = ind-empty

abstract
  is-trunc-coprod : {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} →
    is-trunc (succ-𝕋 (succ-𝕋 k)) A → is-trunc (succ-𝕋 (succ-𝕋 k)) B →
    is-trunc (succ-𝕋 (succ-𝕋 k)) (coprod A B)
  is-trunc-coprod k {A} {B} is-trunc-A is-trunc-B (inl x) (inl y) =
    is-trunc-is-equiv (succ-𝕋 k)
      ( Eq-coprod A B (inl x) (inl y))
      ( Eq-coprod-eq A B (inl x) (inl y))
      ( is-equiv-Eq-coprod-eq A B (inl x) (inl y))
      ( is-trunc-is-equiv' (succ-𝕋 k)
        ( Id x y)
        ( map-raise _ (Id x y))
        ( is-equiv-map-raise _ (Id x y))
        ( is-trunc-A x y))
  is-trunc-coprod k {A} {B} is-trunc-A is-trunc-B (inl x) (inr y) =
    is-trunc-is-equiv (succ-𝕋 k)
      ( Eq-coprod A B (inl x) (inr y))
      ( Eq-coprod-eq A B (inl x) (inr y))
      ( is-equiv-Eq-coprod-eq A B (inl x) (inr y))
      ( is-trunc-is-equiv' (succ-𝕋 k)
        ( empty)
        ( map-raise _ empty)
        ( is-equiv-map-raise _ empty)
        ( is-trunc-succ-empty k))
  is-trunc-coprod k {A} {B} is-trunc-A is-trunc-B (inr x) (inl y) =
    is-trunc-is-equiv (succ-𝕋 k)
      ( Eq-coprod A B (inr x) (inl y))
      ( Eq-coprod-eq A B (inr x) (inl y))
      ( is-equiv-Eq-coprod-eq A B (inr x) (inl y))
      ( is-trunc-is-equiv' (succ-𝕋 k)
        ( empty)
        ( map-raise _ empty)
        ( is-equiv-map-raise _ empty)
        ( is-trunc-succ-empty k))
  is-trunc-coprod k {A} {B} is-trunc-A is-trunc-B (inr x) (inr y) =
    is-trunc-is-equiv (succ-𝕋 k)
      ( Eq-coprod A B (inr x) (inr y))
      ( Eq-coprod-eq A B (inr x) (inr y))
      ( is-equiv-Eq-coprod-eq A B (inr x) (inr y))
      ( is-trunc-is-equiv' (succ-𝕋 k)
        ( Id x y)
        ( map-raise _ (Id x y))
        ( is-equiv-map-raise _ (Id x y))
        ( is-trunc-B x y))

abstract
  is-set-coprod : {l1 l2 : Level} {A : UU l1} {B : UU l2} →
    is-set A → is-set B → is-set (coprod A B)
  is-set-coprod = is-trunc-coprod neg-two-𝕋

set-coprod :
  {l1 l2 : Level} (A : UU-Set l1) (B : UU-Set l2) → UU-Set (l1 ⊔ l2)
set-coprod (pair A is-set-A) (pair B is-set-B) =
  pair (coprod A B) (is-set-coprod is-set-A is-set-B)

abstract
  is-set-unit : is-set unit
  is-set-unit = is-trunc-succ-is-trunc neg-one-𝕋 unit is-prop-unit

set-unit : UU-Set lzero
set-unit = pair unit is-set-unit

abstract
  is-set-ℤ : is-set ℤ
  is-set-ℤ = is-set-coprod is-set-ℕ (is-set-coprod is-set-unit is-set-ℕ)

set-ℤ : UU-Set lzero
set-ℤ = pair ℤ is-set-ℤ

is-set-empty : is-set empty
is-set-empty ()

abstract
  is-set-Fin :
    (n : ℕ) → is-set (Fin n)
  is-set-Fin zero-ℕ = is-set-empty
  is-set-Fin (succ-ℕ n) =
    is-set-coprod (is-set-Fin n) is-set-unit

set-Fin :
  (n : ℕ) → UU-Set lzero
set-Fin n = pair (Fin n) (is-set-Fin n)

-- Exercise 8.7

abstract
  is-trunc-retract-of : {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} →
    A retract-of B → is-trunc k B → is-trunc k A
  is-trunc-retract-of neg-two-𝕋 (pair i (pair r H)) is-trunc-B =
    is-contr-retract-of _ (pair i (pair r H)) is-trunc-B
  is-trunc-retract-of (succ-𝕋 k) (pair i retr-i) is-trunc-B x y =
    is-trunc-retract-of k
      ( pair (ap i) (retr-ap i retr-i x y))
      ( is-trunc-B (i x) (i y))

-- Exercise 8.8

is-injective : {l1 l2 : Level} {A : UU l1} (is-set-A : is-set A) {B : UU l2}
  (is-set-B : is-set B) (f : A → B) → UU (l1 ⊔ l2)
is-injective {A = A} is-set-A is-set-B f = (x y : A) → Id (f x) (f y) → Id x y

is-injective-const-true : is-injective is-set-unit is-set-bool
  (const unit bool true)
is-injective-const-true x y p = center (is-prop-unit x y)

is-injective-const-false : is-injective is-set-unit is-set-bool
  (const unit bool false)
is-injective-const-false x y p = center (is-prop-unit x y)

abstract
  is-equiv-is-prop : {l1 l2 : Level} {A : UU l1} {B : UU l2} → is-prop A →
    is-prop B → {f : A → B} → (B → A) → is-equiv f
  is-equiv-is-prop is-prop-A is-prop-B {f} g =
    is-equiv-has-inverse
      ( g)
      ( λ y → center (is-prop-B (f (g y)) y))
      ( λ x → center (is-prop-A (g (f x)) x))

equiv-prop :
  { l1 l2 : Level} {A : UU l1} {B : UU l2} → is-prop A → is-prop B →
  ( A → B) → (B → A) → A ≃ B
equiv-prop is-prop-A is-prop-B f g =
  pair f (is-equiv-is-prop is-prop-A is-prop-B g)

equiv-total-subtype :
  { l1 l2 l3 : Level} {A : UU l1} {P : A → UU l2} {Q : A → UU l3} →
  ( is-subtype-P : is-subtype P) (is-subtype-Q : is-subtype Q) →
  ( f : (x : A) → P x → Q x) →
  ( g : (x : A) → Q x → P x) →
  ( Σ A P) ≃ (Σ A Q)
equiv-total-subtype is-subtype-P is-subtype-Q f g =
  pair
    ( tot f)
    ( is-equiv-tot-is-fiberwise-equiv {f = f}
      ( λ x → is-equiv-is-prop (is-subtype-P x) (is-subtype-Q x) (g x)))

abstract
  is-emb-is-injective : {l1 l2 : Level} {A : UU l1} (is-set-A : is-set A)
    {B : UU l2} (is-set-B : is-set B) (f : A → B) →
    is-injective is-set-A is-set-B f → is-emb f
  is-emb-is-injective is-set-A is-set-B f is-injective-f x y =
    is-equiv-is-prop
      ( is-set-A x y)
      ( is-set-B (f x) (f y))
      ( is-injective-f x y)

abstract
  is-injective-is-emb : {l1 l2 : Level} {A : UU l1} {is-set-A : is-set A}
    {B : UU l2} {is-set-B : is-set B} {f : A → B} →
    is-emb f → is-injective is-set-A is-set-B f
  is-injective-is-emb is-emb-f x y = inv-is-equiv (is-emb-f x y)

-- Exercise 8.9

abstract
  is-trunc-const-is-trunc : {l : Level} (k : 𝕋) {A : UU l} →
    is-trunc (succ-𝕋 k) A → (x : A) → is-trunc-map k (const unit A x)
  is-trunc-const-is-trunc k is-trunc-A x y =
    is-trunc-is-equiv' k
      ( Id x y)
      ( left-unit-law-Σ-map (λ t → Id x y) is-contr-unit)
      ( is-equiv-left-unit-law-Σ-map (λ t → Id x y) is-contr-unit)
      ( is-trunc-A x y)

abstract
  is-trunc-is-trunc-const : {l : Level} (k : 𝕋) {A : UU l} →
    ((x : A) → is-trunc-map k (const unit A x)) → is-trunc (succ-𝕋 k) A
  is-trunc-is-trunc-const k is-trunc-const x y =
    is-trunc-is-equiv k
      ( Σ unit (λ t → Id x y))
      ( left-unit-law-Σ-map (λ t → Id x y) is-contr-unit)
      ( is-equiv-left-unit-law-Σ-map (λ t → Id x y) is-contr-unit)
      ( is-trunc-const x y)

-- Exercise 8.10

map-fib-comp : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
  {X : UU l3} (g : B → X) (h : A → B) →
  (x : X) → fib (g ∘ h) x → Σ (fib g x) (λ t → fib h (pr1 t))
map-fib-comp g h x (pair a p) =
  pair
    ( pair (h a) p)
    ( pair a refl)

inv-map-fib-comp : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
  {X : UU l3} (g : B → X) (h : A → B) →
  (x : X) → Σ (fib g x) (λ t → fib h (pr1 t)) → fib (g ∘ h) x
inv-map-fib-comp g h c t =
  pair (pr1 (pr2 t)) ((ap g (pr2 (pr2 t))) ∙ (pr2 (pr1 t)))

issec-inv-map-fib-comp : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
  {X : UU l3} (g : B → X) (h : A → B) →
  (x : X) →
  ((map-fib-comp g h x) ∘ (inv-map-fib-comp g h x)) ~ id
issec-inv-map-fib-comp g h x
  (pair (pair .(h a) refl) (pair a refl)) = refl

isretr-inv-map-fib-comp : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
  {X : UU l3} (g : B → X) (h : A → B) (x : X) →
  ((inv-map-fib-comp g h x) ∘ (map-fib-comp g h x)) ~ id
isretr-inv-map-fib-comp g h .(g (h a)) (pair a refl) = refl

abstract
  is-equiv-map-fib-comp : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
    {X : UU l3} (g : B → X) (h : A → B) (x : X) →
    is-equiv (map-fib-comp g h x)
  is-equiv-map-fib-comp g h x =
    is-equiv-has-inverse
      ( inv-map-fib-comp g h x)
      ( issec-inv-map-fib-comp g h x)
      ( isretr-inv-map-fib-comp g h x)

abstract
  is-equiv-inv-map-fib-comp : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
    {X : UU l3} (g : B → X) (h : A → B) (x : X) →
    is-equiv (inv-map-fib-comp g h x)
  is-equiv-inv-map-fib-comp g h x =
    is-equiv-has-inverse
      ( map-fib-comp g h x)
      ( isretr-inv-map-fib-comp g h x)
      ( issec-inv-map-fib-comp g h x)

abstract
  is-trunc-map-htpy : {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2}
    (f g : A → B) → f ~ g → is-trunc-map k g → is-trunc-map k f
  is-trunc-map-htpy k {A} f g H is-trunc-g b =
    is-trunc-is-equiv k
      ( Σ A (λ z → Id (g z) b))
      ( fib-triangle f g id H b)
      ( is-fiberwise-equiv-is-equiv-triangle f g id H (is-equiv-id _) b)
      ( is-trunc-g b)

abstract
  is-trunc-map-comp : {l1 l2 l3 : Level} (k : 𝕋) {A : UU l1} {B : UU l2}
    {X : UU l3} (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h)) →
    is-trunc-map k g → is-trunc-map k h → is-trunc-map k f
  is-trunc-map-comp k f g h H is-trunc-g is-trunc-h =
    is-trunc-map-htpy k f (g ∘ h) H
      ( λ x → is-trunc-is-equiv k
        ( Σ (fib g x) (λ t → fib h (pr1 t)))
        ( map-fib-comp g h x)
        ( is-equiv-map-fib-comp g h x)
        ( is-trunc-Σ k
          ( is-trunc-g x)
          ( λ t → is-trunc-h (pr1 t))))

abstract
  is-trunc-map-right-factor : {l1 l2 l3 : Level} (k : 𝕋) {A : UU l1} {B : UU l2}
    {X : UU l3} (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h)) →
    is-trunc-map k g → is-trunc-map k f → is-trunc-map k h
  is-trunc-map-right-factor k {A} f g h H is-trunc-g is-trunc-f b =
    is-trunc-fam-is-trunc-Σ k
      ( is-trunc-g (g b))
      ( is-trunc-is-equiv' k
        ( Σ A (λ z → Id (g (h z)) (g b)))
        ( map-fib-comp g h (g b))
        ( is-equiv-map-fib-comp g h (g b))
        ( is-trunc-map-htpy k (g ∘ h) f (htpy-inv H) is-trunc-f (g b)))
      ( pair b refl)

abstract
  is-trunc-map-succ-is-trunc-map :
    {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2}
    (f : A → B) → is-trunc-map k f → is-trunc-map (succ-𝕋 k) f
  is-trunc-map-succ-is-trunc-map k f is-trunc-f b =
    is-trunc-succ-is-trunc k (fib f b) (is-trunc-f b)

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
module RevMachine where
open import Level
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Product

record RevMachine {ℓ} : Set (suc ℓ) where
  field
    State : Set ℓ
    _↦_ : Rel State ℓ
    deterministic : ∀ {st st₁ st₂} → st ↦ st₁ → st ↦ st₂ → st₁ ≡ st₂
    deterministicᵣₑᵥ : ∀ {st st₁ st₂} → st₁ ↦ st → st₂ ↦ st → st₁ ≡ st₂

record PartialRevMachine {ℓ} : Set (suc ℓ) where
  field
    State : Set ℓ
    _↦_ : Rel State ℓ
    is-fail : State → Set ℓ
    is-fail? : (st : State) → Dec (is-fail st)
    fail-is-stuck : ∀ {st} → is-fail st → ∄[ st' ] (st ↦ st')
    deterministic : ∀ {st st₁ st₂} → st ↦ st₁ → st ↦ st₂ → st₁ ≡ st₂
    deterministicᵣₑᵥ : ∀ {st st₁ st₂} → st₁ ↦ st → st₂ ↦ st → ¬ (is-fail st) → st₁ ≡ st₂


text:
module Structure.Numeral.Natural where

open import Lang.Instance
import      Lvl
open import Logic.Predicate
open import Logic.Propositional
open import Structure.Setoid
open import Structure.Function.Domain
open import Structure.Function
open import Structure.Operator
open import Structure.Relator
open import Structure.Setoid
open import Syntax.Function
open import Type

private variable ℓₒ ℓₗ ℓₑ ℓₗ₁ ℓₗ₂ : Lvl.Level
private variable N : Type{ℓₒ}

module _ ⦃ equiv : Equiv{ℓₑ}(N) ⦄ where
  private variable 𝟎 : N
  private variable 𝐒 : N → N
  private variable _+_ _⋅_ _^_ : N → N → N

  module _ {ℓ} (𝟎 : N) (𝐒 : N → N) where
    record Induction : Type{ℓₑ Lvl.⊔ Lvl.of(N) Lvl.⊔ Lvl.𝐒(ℓ)} where
      constructor intro
      field proof : (P : N → Type{ℓ}) ⦃ rel : UnaryRelator(P) ⦄ → P(𝟎) → ((n : N) → P(n) → P(𝐒(n))) → ((n : N) → P(n))
    induction = inst-fn Induction.proof

  record Elemental (𝟎 : N) (𝐒 : N → N) : Type{ℓₑ Lvl.⊔ Lvl.of(N)} where
    constructor intro
    field
      ⦃ 𝐒-function ⦄    : Function(𝐒)
      ⦃ 𝐒-injectivity ⦄ : Injective(𝐒)
      𝐒-positivity      : ∀{x} → (𝐒(x) ≢ 𝟎)

  record Addition ⦃ elemn : Elemental(𝟎)(𝐒) ⦄ (_+_ : N → N → N) : Type{ℓₑ Lvl.⊔ Lvl.of(N)} where
    constructor intro
    field
      ⦃ operator ⦄ : BinaryOperator(_+_)
      base : ∀{a}   → (a + 𝟎    ≡ a)
      step : ∀{a b} → (a + 𝐒(b) ≡ 𝐒(a + b))

  record Multiplication ⦃ elemn : Elemental(𝟎)(𝐒) ⦄ ⦃ addi : Addition(_+_) ⦄ (_⋅_ : N → N → N) : Type{ℓₑ Lvl.⊔ Lvl.of(N)} where
    constructor intro
    field
      ⦃ operator ⦄ : BinaryOperator(_⋅_)
      base : ∀{a}   → (a ⋅ 𝟎    ≡ 𝟎)
      step : ∀{a b} → (a ⋅ 𝐒(b) ≡ a + (a ⋅ b))

  record Exponentiation ⦃ elemn : Elemental(𝟎)(𝐒) ⦄ ⦃ addi : Addition(_+_) ⦄ ⦃ multi : Multiplication(_⋅_) ⦄ (_^_ : N → N → N) : Type{ℓₑ Lvl.⊔ Lvl.of(N)} where
    constructor intro
    field
      ⦃ operator ⦄ : BinaryOperator(_^_)
      base : ∀{a}   → (a ^ 𝟎    ≡ 𝐒(𝟎))
      step : ∀{a b} → (a ^ 𝐒(b) ≡ a ⋅ (a ^ b))

  record WeakOrdering ⦃ elemn : Elemental(𝟎)(𝐒) ⦄ {_+_ : N → N → N} ⦃ addi : Addition(_+_) ⦄ (_≤_ : N → N → Type{ℓₗ}) : Type{ℓₑ Lvl.⊔ Lvl.of(N) Lvl.⊔ ℓₗ} where
    constructor intro
    field
      ⦃ relator ⦄ : BinaryRelator(_≤_)
      proof : ∀{a b} → (a ≤ b) ↔ ∃(c ↦ a + c ≡ b)

  module _ ⦃ ind : Induction(𝟎)(𝐒) ⦄ ⦃ elem : Elemental(𝟎)(𝐒) ⦄ where
    open import Structure.Relator.Proofs
    open import Structure.Relator.Properties

    open Elemental(elem)
    open Induction(ind)

    𝟎-or-𝐒 : ∀{x} → (x ≡ 𝟎) ∨ ∃(y ↦ x ≡ 𝐒(y))
    𝟎-or-𝐒 {x} = induction(𝟎)(𝐒)
      (x ↦ (x ≡ 𝟎) ∨ ∃(y ↦ x ≡ 𝐒(y))) ⦃ [∨]-unaryRelator ⦃ rel-P = BinaryRelator.left [≡]-binaryRelator ⦄ ⦃ rel-Q = [∃]-unaryRelator ⦃ rel-P = BinaryRelator.left [≡]-binaryRelator ⦄ ⦄ ⦄
      ([∨]-introₗ (reflexivity(_≡_)))
      (x ↦ [∨]-elim
        (p ↦ [∨]-introᵣ([∃]-intro 𝟎 ⦃ congruence₁(𝐒) p ⦄))
        (\{([∃]-intro y ⦃ p ⦄) → [∨]-introᵣ([∃]-intro (𝐒(y)) ⦃ congruence₁(𝐒) p ⦄)})
      )
      x

{-
  module _ ⦃ ind : Induction(𝟎)(𝐒) ⦄ where
    import      Data.Either as Either
    open import Functional
    open import Numeral.Natural as ℕ using (ℕ)
    open import Relator.Equals renaming (_≡_ to _≡ₑ_)
    open import Structure.Relator.Proofs
    open import Syntax.Number

    from-ℕ : ℕ → N
    from-ℕ (ℕ.𝟎)    = 𝟎
    from-ℕ (ℕ.𝐒(n)) = 𝐒(from-ℕ n)
-}

  -- TODO: Also include the definition of a "naturally ordered semigroup" here

{-
  module _ (_<_ : T → T → Stmt{ℓₗ}) where
    record Minimal : Type{Lvl.of(T) Lvl.⊔ ℓₗ} where
      open From-[<][≡] (_<_) (_≡_)

      field
        ⦃ elemental ⦄ : Elemental
        [<]ₗ-𝟎 : ∀{x} → (𝟎 < x) ↔ (x ≢ 𝟎)
        [<]ᵣ-𝟎 : ∀{x} → (𝟎 ≤ x) -- Minimum in the order (TODO: Is (∀x. x≥0) neccessary? Which means (0<x)∨(0=x))
        [<]ₗ-𝐒 : ∀{x y} → (𝐒(x) < y) ↔ ((x < y)∧(𝐒(x) ≢ y)) -- TODO: Also the definition of (_≤_)?
        [<]ᵣ-𝐒 : ∀{x y} → (x < 𝐒(y)) ↔ (x ≤ y)

-}

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:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

------------------------------------------------------------------------------
import      LibraBFT.Impl.OBM.Crypto            as TODO
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.PKCS
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                         using (String)
------------------------------------------------------------------------------

module LibraBFT.Impl.Consensus.SafetyRules.PersistentSafetyStorage where

new : Author → Waypoint → SK → PersistentSafetyStorage
new author waypoint sk = mkPersistentSafetyStorage
     {- _pssSafetyData =-} (SafetyData∙new
                           {-  _sdEpoch          = Epoch-} 1
                           {-, _sdLastVotedRound = Round-} 0
                           {-, _sdPreferredRound = Round-} 0
                           {-, _sdLastVote       =-}       nothing)
     {-, _pssAuthor    =-} author
     {-, _pssWaypoint  =-} waypoint
     {-, _pssObmSK     =-} (just sk)

consensusKeyForVersion : PersistentSafetyStorage → PK → Either ErrLog SK
consensusKeyForVersion self pk =
  -- LBFT-OBM-DIFF
  maybeS (self ^∙ pssObmSK) (Left fakeErr {-"pssObmSK Nothing"-}) $ λ sk →
    if TODO.makePK sk /= pk
    then Left fakeErr -- ["sk /= pk"]
    else pure sk
 where
  here' : List String → List String
  here' t = "PersistentSafetyStorage" ∷ "consensusKeyForVersion" ∷ t


text:
module UniDB.Subst.Reg where

open import UniDB.Spec
open import UniDB.Subst.Core
open import UniDB.Morph.Reg
open import UniDB.Morph.WeakenPrime

module _ {T : STX} {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}} where

  instance
    iCompReg : Comp (Reg T)
    _⊙_ {{iCompReg}} (baseR ξ)             ζ = ξ ⊡ ζ
    _⊙_ {{iCompReg}} (snocR {γ₁} {γ₂} ξ t) ζ = snocR (ξ ⊙ ζ) (ap {T} ζ t)

    iWkmHomReg : WkmHom (Reg T)
    wkm-zero {{iWkmHomReg}} = refl
    wkm-suc  {{iWkmHomReg}} δ = refl

    iWkmBetaReg : WkmBeta T (Reg T)
    wkm-beta {{iWkmBetaReg}} t = refl

  reg-zero : (γ : Dom) → Reg T zero γ
  reg-zero zero    = baseR baseW
  reg-zero (suc γ) = reg-zero γ ⊙ wkm {Reg T} 1

  complete : (γ₁ γ₂ : Dom) (f : Ix γ₁ → T γ₂) → Reg T γ₁ γ₂
  complete zero     γ₂ f = reg-zero γ₂
  complete (suc γ₁) γ₂ f = snocR (complete γ₁ γ₂ (f ∘ suc)) (f zero)

  ⊡-⊙-assoc : {γ₁ γ₂ γ₃ γ₄ : Dom} (ξ₁ : Weaken` γ₁ γ₂) (ξ₂ : Reg T γ₂ γ₃) (ξ₃ : Reg T γ₃ γ₄) →
    ξ₁ ⊡ (ξ₂ ⊙ ξ₃) ≡ (ξ₁ ⊡ ξ₂) ⊙ ξ₃
  ⊡-⊙-assoc ξ₁        (baseR ξ₂)   ξ₃ = ⊡-⊡-assoc ξ₁ ξ₂ ξ₃
  ⊡-⊙-assoc baseW      ξ₂           ξ₃ rewrite idm-⊡ {Weaken`} {Reg T} (ξ₂ ⊙ ξ₃) | idm-⊡ {Weaken`} {Reg T} ξ₂ = refl
  ⊡-⊙-assoc (stepW ξ₁) (snocR ξ₂ t) ξ₃ = ⊡-⊙-assoc ξ₁ ξ₂ ξ₃

  wk₁-⊡ : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Weaken` γ₁ γ₂) (ξ₂ : Reg T γ₂ γ₃) →
    wk₁ (_⊡_ {Weaken`} {Reg T} {Reg T} ξ₁ ξ₂) ≡ ξ₁ ⊡ wk₁ ξ₂
  wk₁-⊡ ξ₁ (baseR ξ)            = refl
  wk₁-⊡ baseW (snocR ξ₂ t)      = refl
  wk₁-⊡ (stepW ξ₁) (snocR ξ₂ t) = wk₁-⊡ ξ₁ ξ₂

module _
  {T : STX} {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}} {{wkVrT : WkVr T}}
  where

  instance
    iCompIdmReg : {{apRelTT : ApRel T T}} {{apIdmTT : ApIdm T T}} → CompIdm (Reg T)
    ⊙-idm {{iCompIdmReg}} (baseR ξ) = refl
    ⊙-idm {{iCompIdmReg}} (snocR ξ t) = cong₂ snocR (⊙-idm {Reg T} ξ) (ap-idm` {T} t)
    idm-⊙ {{iCompIdmReg}} ξ = idm-⊡ {Weaken`} {Reg T} ξ

  lk-⊡ : {{apVr : ApVr T}}
    {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Weaken` γ₁ γ₂) (ξ₂ : Reg T γ₂ γ₃) →
    (i : Ix γ₁) → lk {T} {Reg T} (ξ₁ ⊡ ξ₂) i ≡ ap {T} ξ₂ (lk {T} ξ₁ i)
  lk-⊡ ξ₁ (baseR ξ₂) i = begin
    lk (ξ₁ ⊙ ξ₂) i                           ≡⟨ lk-ren-comp {T} ξ₁ ξ₂ i ⟩
    lk ξ₂ (lk ξ₁ i)                          ≡⟨ sym (ap-vr {T} (baseR ξ₂) (lk ξ₁ i)) ⟩
    ap {T} (baseR ξ₂) (vr (lk  ξ₁ i))        ≡⟨ cong (ap {T} (baseR ξ₂)) (sym (lk-ren {T} ξ₁ i)) ⟩
    ap {T} (baseR ξ₂) (lk ξ₁ i)              ∎
  lk-⊡ baseW ξ₂ i = begin
    lk {T} {Reg T} (baseW ⊡ ξ₂) i             ≡⟨ cong₂ lk (idm-⊡ {Weaken`} ξ₂) refl ⟩
    lk {T} {Reg T} ξ₂ i                      ≡⟨ sym (ap-vr {T} ξ₂ i) ⟩
    ap {T} ξ₂ (vr i)                         ∎
  lk-⊡ (stepW ξ₁) (snocR ξ₂ t) i = begin
    lk {T} {Reg T} (ξ₁ ⊡ ξ₂) i               ≡⟨ lk-⊡ ξ₁ ξ₂ i ⟩
    ap {T} ξ₂ (vr (lk ξ₁ i))                 ≡⟨ ap-vr {T} ξ₂ (lk ξ₁ i) ⟩
    lk ξ₂ (lk ξ₁ i)                          ≡⟨ refl ⟩
    lk (snocR ξ₂ t) (suc (lk ξ₁ i))          ≡⟨ sym (ap-vr {T} (snocR ξ₂ t) (suc (lk ξ₁ i))) ⟩
    ap {T} (snocR ξ₂ t) (vr (suc (lk ξ₁ i))) ∎

  instance
    iLkCompApReg : {{apVr : ApVr T}} → LkCompAp T (Reg T)
    lk-⊙-ap {{iLkCompApReg}} (baseR ξ₁)    ξ₂ i       = lk-⊡ ξ₁ ξ₂ i
    lk-⊙-ap {{iLkCompApReg}} (snocR ξ₁ t) ξ₂ zero    = refl
    lk-⊙-ap {{iLkCompApReg}} (snocR ξ₁ t) ξ₂ (suc i) = lk-⊙-ap {T} ξ₁ ξ₂ i

  wk₁-⊙ : {{apWkTT : ApWk T T}}
    {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Reg T γ₁ γ₂) (ξ₂ : Reg T γ₂ γ₃) →
    wk₁ (ξ₁ ⊙ ξ₂) ≡ wk₁ ξ₁ ⊙ snocR (wk₁ ξ₂) (Vr.vr vrT zero)
  wk₁-⊙ (baseR ξ)     ξ₂ = wk₁-⊡ ξ ξ₂
  wk₁-⊙ (snocR ξ₁ t) ξ₂ = cong₂ snocR (wk₁-⊙ ξ₁ ξ₂) (sym (ap-wk₁ {T} ξ₂ t))

  instance
    iUpCompReg : {{apVrT : ApVr T}} {{apWkTT : ApWk T T}} → UpComp (Reg T)
    ⊙-↑₁ {{iUpCompReg}} ξ₁ ξ₂ = cong₂ snocR
      (wk₁-⊙ ξ₁ ξ₂)
      (sym (ap-vr {T} (snocR (wk₁ ξ₂) (vr zero)) zero))

    iCompAssocReg : {{apVrT : ApVr T}} {{apCompT : ApComp T T}} {{apWkTT : ApWk T T}} →
      CompAssoc (Reg T)
    ⊙-assoc {{iCompAssocReg}} (baseR ξ₁)    ξ₂ ξ₃ = ⊡-⊙-assoc ξ₁ ξ₂ ξ₃
    ⊙-assoc {{iCompAssocReg}} (snocR ξ₁ t) ξ₂ ξ₃ =
      cong₂ snocR (⊙-assoc {Reg T} ξ₁ ξ₂ ξ₃) (ap-⊙ {T} ξ₂ ξ₃ t)

  ⊙-wkm₁-reg : {{apWkmWkTT : ApWkmWk T T}}
    {γ₁ γ₂ : Dom} (ξ : Reg T γ₁ γ₂) →
    ξ ⊙ wkm {Reg T} 1 ≡ wk₁ ξ
  ⊙-wkm₁-reg (baseR ξ)     = refl
  ⊙-wkm₁-reg (snocR ξ t) rewrite sym (wk1-wk₁ t) =
    cong₂ snocR (⊙-wkm₁-reg ξ) (ap-wkm-wk {T} 1 t)

  instance
    iWkmCommReg : {{apVr : ApVr T}} {{apCompT : ApComp T T}} {{apWkTT : ApWk T T}}
      {{apWkmWkTT : ApWkmWk T T}} {{apRelTT : ApRel T T}} {{apIdmTT : ApIdm T T}} →
      WkmComm (Reg T)
    wkm₁-comm {{iWkmCommReg}} (baseR baseW) = refl
    wkm₁-comm {{iWkmCommReg}} (baseR (stepW ξ)) rewrite idm-⊙ {Weaken`} ξ = refl
    wkm₁-comm {{iWkmCommReg}} (snocR ξ t) = ⊙-wkm₁-reg (snocR ξ t)

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
{-# OPTIONS --safe --without-K #-}
module JVM.Builtins where

open import Data.List

open import JVM.Types

Object = "java/lang/Object"
Str    = "java/lang/String"

jre : Constantpool
jre = staticref ("java/lang/System"    / "out"     ∶ ref "java/io/PrintStream")
    ∷ virtual   ("java/io/PrintStream" / "println" :⟨ [ int ] ⟩ void)
    ∷ class     (Object)
    ∷ virtual   (Object / "<init>" :⟨ [] ⟩ void)
    ∷ []