text:
------------------------------------------------------------------------
-- The figure of eight
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

-- The module is parametrised by a notion of equality. The higher
-- constructor of the HIT defining the circle uses path equality, but
-- the supplied notion of equality is used for many other things.

import Equality.Path as P

module Figure-of-eight
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

import Equality.Path.Univalence as EPU
open import Prelude

open import Bijection equality-with-J using (_↔_)
import Bijection P.equality-with-J as PB
open import Circle eq as Circle using (𝕊¹; base; loopᴾ)
open import Equality.Decision-procedures equality-with-J
open import Equality.Path.Isomorphisms eq
import Equality.Tactic P.equality-with-J as PT
open import Equivalence equality-with-J as Eq using (_≃_)
import Equivalence P.equality-with-J as PE
open import Erased.Cubical eq
open import Function-universe equality-with-J hiding (_∘_)
open import Pushout eq as Pushout using (Wedge; inl; inr; glueᴾ)
import Univalence-axiom P.equality-with-J as PU

private
  variable
    a p   : Level
    A     : Type a
    P     : A → Type p
    e r x : A

------------------------------------------------------------------------
-- The type

-- The figure of eight
-- (https://topospaces.subwiki.org/wiki/Wedge_of_two_circles).

data ∞ : Type where
  base          : ∞
  loop₁ᴾ loop₂ᴾ : base P.≡ base

-- The higher constructors.

loop₁ : base ≡ base
loop₁ = _↔_.from ≡↔≡ loop₁ᴾ

loop₂ : base ≡ base
loop₂ = _↔_.from ≡↔≡ loop₂ᴾ

------------------------------------------------------------------------
-- Eliminators

-- An eliminator, expressed using paths.

record Elimᴾ (P : ∞ → Type p) : Type p where
  no-eta-equality
  field
    baseʳ  : P base
    loop₁ʳ : P.[ (λ i → P (loop₁ᴾ i)) ] baseʳ ≡ baseʳ
    loop₂ʳ : P.[ (λ i → P (loop₂ᴾ i)) ] baseʳ ≡ baseʳ

open Elimᴾ public

elimᴾ : Elimᴾ P → (x : ∞) → P x
elimᴾ {P = P} e = helper
  where
  module E = Elimᴾ e

  helper : (x : ∞) → P x
  helper base       = E.baseʳ
  helper (loop₁ᴾ i) = E.loop₁ʳ i
  helper (loop₂ᴾ i) = E.loop₂ʳ i

-- A non-dependent eliminator, expressed using paths.

record Recᴾ (A : Type a) : Type a where
  no-eta-equality
  field
    baseʳ         : A
    loop₁ʳ loop₂ʳ : baseʳ P.≡ baseʳ

open Recᴾ public

recᴾ : Recᴾ A → ∞ → A
recᴾ r = elimᴾ λ where
    .baseʳ  → R.baseʳ
    .loop₁ʳ → R.loop₁ʳ
    .loop₂ʳ → R.loop₂ʳ
  where
  module R = Recᴾ r

-- An eliminator.

record Elim (P : ∞ → Type p) : Type p where
  no-eta-equality
  field
    baseʳ  : P base
    loop₁ʳ : subst P loop₁ baseʳ ≡ baseʳ
    loop₂ʳ : subst P loop₂ baseʳ ≡ baseʳ

open Elim public

elim : Elim P → (x : ∞) → P x
elim e = elimᴾ λ where
    .baseʳ  → E.baseʳ
    .loop₁ʳ → subst≡→[]≡ E.loop₁ʳ
    .loop₂ʳ → subst≡→[]≡ E.loop₂ʳ
  where
  module E = Elim e

-- Two "computation" rules.

elim-loop₁ : dcong (elim e) loop₁ ≡ e .Elim.loop₁ʳ
elim-loop₁ = dcong-subst≡→[]≡ (refl _)

elim-loop₂ : dcong (elim e) loop₂ ≡ e .Elim.loop₂ʳ
elim-loop₂ = dcong-subst≡→[]≡ (refl _)

-- A non-dependent eliminator.

record Rec (A : Type a) : Type a where
  no-eta-equality
  field
    baseʳ         : A
    loop₁ʳ loop₂ʳ : baseʳ ≡ baseʳ

open Rec public

rec : Rec A → ∞ → A
rec r = recᴾ λ where
    .baseʳ  → R.baseʳ
    .loop₁ʳ → _↔_.to ≡↔≡ R.loop₁ʳ
    .loop₂ʳ → _↔_.to ≡↔≡ R.loop₂ʳ
  where
  module R = Rec r

-- Two "computation" rules.

rec-loop₁ : cong (rec r) loop₁ ≡ r .Rec.loop₁ʳ
rec-loop₁ = cong-≡↔≡ (refl _)

rec-loop₂ : cong (rec r) loop₂ ≡ r .Rec.loop₂ʳ
rec-loop₂ = cong-≡↔≡ (refl _)

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

-- The two higher constructors are not equal.
--
-- The proof is based on the one from the HoTT book that shows that
-- the circle's higher constructor is not equal to reflexivity.

loop₁≢loop₂ : loop₁ ≢ loop₂
loop₁≢loop₂ =
  Stable-¬
    [ loop₁ ≡ loop₂      ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ (inverse ≡↔≡)) ⟩
      loop₁ᴾ ≡ loop₂ᴾ    ↔⟨ ≡↔≡ ⟩
      loop₁ᴾ P.≡ loop₂ᴾ  ↝⟨ PU.¬-Type-set EPU.univ ∘ Type-set ⟩□
      ⊥                  □
    ]
  where
  module _ (hyp : loop₁ᴾ P.≡ loop₂ᴾ) where
    refl≡ : (A : Type) (A≡A : A P.≡ A) → P.refl P.≡ A≡A
    refl≡ A A≡A =
      P.refl           P.≡⟨⟩
      P.cong F loop₁ᴾ  P.≡⟨ P.cong (P.cong F) hyp ⟩
      P.cong F loop₂ᴾ  P.≡⟨⟩
      A≡A              P.∎
      where
      F : ∞ → Type
      F base       = A
      F (loop₁ᴾ i) = P.refl i
      F (loop₂ᴾ i) = A≡A i

    Type-set : P.Is-set Type
    Type-set {x = A} {y = B} =
      P.elim¹ (λ p → ∀ q → p P.≡ q)
              (refl≡ A)

-- The two higher constructors provide a counterexample to
-- commutativity of transitivity.
--
-- This proof is a minor variant of a proof due to Andrea Vezzosi.

trans-not-commutative : trans loop₁ loop₂ ≢ trans loop₂ loop₁
trans-not-commutative =
  Stable-¬
    [ trans loop₁ loop₂ ≡ trans loop₂ loop₁          ↝⟨ (λ hyp → trans (sym (_↔_.from-to ≡↔≡ (sym trans≡trans)))
                                                                   (trans (cong (_↔_.to ≡↔≡) hyp) (_↔_.from-to ≡↔≡ (sym trans≡trans)))) ⟩

      P.trans loop₁ᴾ loop₂ᴾ ≡ P.trans loop₂ᴾ loop₁ᴾ  ↝⟨ cong (P.subst F) ⟩

      P.subst F (P.trans loop₁ᴾ loop₂ᴾ) ≡
      P.subst F (P.trans loop₂ᴾ loop₁ᴾ)              ↝⟨ (λ hyp → trans (sym (_↔_.from ≡↔≡ lemma₁₂))
                                                                   (trans hyp (_↔_.from ≡↔≡ lemma₂₁))) ⟩
      PE._≃_.to eq₂ ∘ PE._≃_.to eq₁ ≡
      PE._≃_.to eq₁ ∘ PE._≃_.to eq₂                  ↝⟨ cong (_$ fzero) ⟩

      fzero ≡ fsuc fzero                             ↝⟨ ⊎.inj₁≢inj₂ ⟩□

      ⊥                                              □
    ]
  where
  eq₁ : Fin 3 PE.≃ Fin 3
  eq₁ = PE.↔⇒≃ (record
    { surjection = record
      { logical-equivalence = record
        { to   = λ where
                   fzero               → fsuc (fsuc fzero)
                   (fsuc fzero)        → fsuc fzero
                   (fsuc (fsuc fzero)) → fzero
        ; from = λ where
                   fzero               → fsuc (fsuc fzero)
                   (fsuc fzero)        → fsuc fzero
                   (fsuc (fsuc fzero)) → fzero
        }
      ; right-inverse-of = λ where
          fzero               → P.refl
          (fsuc fzero)        → P.refl
          (fsuc (fsuc fzero)) → P.refl
      }
    ; left-inverse-of = λ where
        fzero               → P.refl
        (fsuc fzero)        → P.refl
        (fsuc (fsuc fzero)) → P.refl
    })

  eq₂ : Fin 3 PE.≃ Fin 3
  eq₂ = PE.↔⇒≃ (record
    { surjection = record
      { logical-equivalence = record
        { to   = λ where
                   fzero               → fsuc fzero
                   (fsuc fzero)        → fsuc (fsuc fzero)
                   (fsuc (fsuc fzero)) → fzero
        ; from = λ where
                   fzero               → fsuc (fsuc fzero)
                   (fsuc fzero)        → fzero
                   (fsuc (fsuc fzero)) → fsuc fzero
        }
      ; right-inverse-of = λ where
          fzero               → P.refl
          (fsuc fzero)        → P.refl
          (fsuc (fsuc fzero)) → P.refl
      }
    ; left-inverse-of = λ where
        fzero               → P.refl
        (fsuc fzero)        → P.refl
        (fsuc (fsuc fzero)) → P.refl
    })

  @0 F : ∞ → Type
  F base       = Fin 3
  F (loop₁ᴾ i) = EPU.≃⇒≡ eq₁ i
  F (loop₂ᴾ i) = EPU.≃⇒≡ eq₂ i

  lemma₁₂ :
    P.subst F (P.trans loop₁ᴾ loop₂ᴾ) P.≡
    PE._≃_.to eq₂ ∘ PE._≃_.to eq₁
  lemma₁₂ _ i@fzero               = PE._≃_.to eq₂ (PE._≃_.to eq₁ i)
  lemma₁₂ _ i@(fsuc fzero)        = PE._≃_.to eq₂ (PE._≃_.to eq₁ i)
  lemma₁₂ _ i@(fsuc (fsuc fzero)) = PE._≃_.to eq₂ (PE._≃_.to eq₁ i)

  lemma₂₁ :
    P.subst F (P.trans loop₂ᴾ loop₁ᴾ) P.≡
    PE._≃_.to eq₁ ∘ PE._≃_.to eq₂
  lemma₂₁ _ i@fzero               = PE._≃_.to eq₁ (PE._≃_.to eq₂ i)
  lemma₂₁ _ i@(fsuc fzero)        = PE._≃_.to eq₁ (PE._≃_.to eq₂ i)
  lemma₂₁ _ i@(fsuc (fsuc fzero)) = PE._≃_.to eq₁ (PE._≃_.to eq₂ i)

private

  -- A lemma used below.

  trans-sometimes-commutative′ :
    {p q : x ≡ x} (f : (x : ∞) → x ≡ x) →
    f x ≡ p →
    trans p q ≡ trans q p
  trans-sometimes-commutative′ {x = x} {p = p} {q = q} f f-x≡p =
    trans p q      ≡⟨ cong (flip trans _) $ sym f-x≡p ⟩
    trans (f x) q  ≡⟨ trans-sometimes-commutative f ⟩
    trans q (f x)  ≡⟨ cong (trans q) f-x≡p ⟩∎
    trans q p      ∎

-- There is no function of type (x : ∞) → x ≡ x which returns loop₁
-- when applied to base.

¬-base↦loop₁ : ¬ ∃ λ (f : (x : ∞) → x ≡ x) → f base ≡ loop₁
¬-base↦loop₁ (f , f-base≡loop₁) =
  trans-not-commutative (
    trans loop₁ loop₂  ≡⟨ trans-sometimes-commutative′ f f-base≡loop₁ ⟩∎
    trans loop₂ loop₁  ∎)

-- There is no function of type (x : ∞) → x ≡ x which returns loop₂
-- when applied to base.

¬-base↦loop₂ : ¬ ∃ λ (f : (x : ∞) → x ≡ x) → f base ≡ loop₂
¬-base↦loop₂ (f , f-base≡loop₂) =
  trans-not-commutative (
    trans loop₁ loop₂  ≡⟨ sym $ trans-sometimes-commutative′ f f-base≡loop₂ ⟩∎
    trans loop₂ loop₁  ∎)

-- There is no function of type (x : ∞) → x ≡ x which returns
-- trans loop₁ loop₂ when applied to base.

¬-base↦trans-loop₁-loop₂ :
  ¬ ∃ λ (f : (x : ∞) → x ≡ x) → f base ≡ trans loop₁ loop₂
¬-base↦trans-loop₁-loop₂ (f , f-base≡trans-loop₁-loop₂) =
  trans-not-commutative (
    trans loop₁ loop₂                                    ≡⟨ sym $ trans-reflˡ _ ⟩
    trans (refl _) (trans loop₁ loop₂)                   ≡⟨ cong (flip trans _) $ sym $ trans-symˡ _ ⟩
    trans (trans (sym loop₁) loop₁) (trans loop₁ loop₂)  ≡⟨ trans-assoc _ _ _ ⟩
    trans (sym loop₁) (trans loop₁ (trans loop₁ loop₂))  ≡⟨ cong (trans (sym loop₁)) $ sym $
                                                            trans-sometimes-commutative′ f f-base≡trans-loop₁-loop₂ ⟩
    trans (sym loop₁) (trans (trans loop₁ loop₂) loop₁)  ≡⟨ cong (trans (sym loop₁)) $ trans-assoc _ _ _ ⟩
    trans (sym loop₁) (trans loop₁ (trans loop₂ loop₁))  ≡⟨ sym $ trans-assoc _ _ _ ⟩
    trans (trans (sym loop₁) loop₁) (trans loop₂ loop₁)  ≡⟨ cong (flip trans _) $ trans-symˡ _ ⟩
    trans (refl _) (trans loop₂ loop₁)                   ≡⟨ trans-reflˡ _ ⟩∎
    trans loop₂ loop₁                                    ∎)

-- There is no function of type (x : ∞) → x ≡ x which returns
-- trans loop₂ loop₁ when applied to base.

¬-base↦trans-loop₂-loop₁ :
  ¬ ∃ λ (f : (x : ∞) → x ≡ x) → f base ≡ trans loop₂ loop₁
¬-base↦trans-loop₂-loop₁ (f , f-base≡trans-loop₂-loop₁) =
  trans-not-commutative (
    trans loop₁ loop₂                                    ≡⟨ sym $ trans-reflˡ _ ⟩
    trans (refl _) (trans loop₁ loop₂)                   ≡⟨ cong (flip trans _) $ sym $ trans-symˡ _ ⟩
    trans (trans (sym loop₂) loop₂) (trans loop₁ loop₂)  ≡⟨ trans-assoc _ _ _ ⟩
    trans (sym loop₂) (trans loop₂ (trans loop₁ loop₂))  ≡⟨ cong (trans (sym loop₂)) $ sym $ trans-assoc _ _ _ ⟩
    trans (sym loop₂) (trans (trans loop₂ loop₁) loop₂)  ≡⟨ cong (trans (sym loop₂)) $
                                                            trans-sometimes-commutative′ f f-base≡trans-loop₂-loop₁ ⟩
    trans (sym loop₂) (trans loop₂ (trans loop₂ loop₁))  ≡⟨ sym $ trans-assoc _ _ _ ⟩
    trans (trans (sym loop₂) loop₂) (trans loop₂ loop₁)  ≡⟨ cong (flip trans _) $ trans-symˡ _ ⟩
    trans (refl _) (trans loop₂ loop₁)                   ≡⟨ trans-reflˡ _ ⟩∎
    trans loop₂ loop₁                                    ∎)

-- TODO: Can one prove that functions of type (x : ∞) → x ≡ x must map
-- base to refl base?

------------------------------------------------------------------------
-- A positive result

-- The figure of eight can be expressed as a wedge of two circles.
--
-- This result was suggested to me by Anders Mörtberg.

∞≃Wedge-𝕊¹-𝕊¹ : ∞ ≃ Wedge (𝕊¹ , base) (𝕊¹ , base)
∞≃Wedge-𝕊¹-𝕊¹ = Eq.↔⇒≃ (record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = _↔_.from ≡↔≡ ∘ from∘to
  })
  where
  lemma : inl base P.≡ inl base
  lemma =
    inl base  P.≡⟨ glueᴾ tt ⟩
    inr base  P.≡⟨ P.sym (P.cong inr loopᴾ) ⟩
    inr base  P.≡⟨ P.sym (glueᴾ tt) ⟩∎
    inl base  ∎

  Glue  = PT.Lift (glueᴾ tt)
  Loop  = PT.Lift (P.cong inr loopᴾ)
  Loop₂ = PT.Lift loop₂ᴾ
  Lemma =
    PT.Trans Glue $
    PT.Trans (PT.Sym Loop) $
    PT.Sym Glue

  to : ∞ → Wedge (𝕊¹ , base) (𝕊¹ , base)
  to base       = inl base
  to (loop₁ᴾ i) = P.cong inl loopᴾ i
  to (loop₂ᴾ i) = P.sym lemma i

  from : Wedge (𝕊¹ , base) (𝕊¹ , base) → ∞
  from = Pushout.recᴾ
    (Circle.recᴾ base loop₁ᴾ)
    (Circle.recᴾ base loop₂ᴾ)
    (λ _ → P.refl)

  to∘from : ∀ x → to (from x) ≡ x
  to∘from =
    _↔_.from ≡↔≡ ∘
    Pushout.elimᴾ _
      (Circle.elimᴾ _ P.refl (λ _ → P.refl))
      (Circle.elimᴾ _ (glueᴾ _)
         (PB._↔_.from (P.heterogeneous↔homogeneous _)
         (P.transport (λ i → P.sym lemma i P.≡ inr (loopᴾ i))
            P.0̲ (glueᴾ tt)                                       P.≡⟨ P.transport-≡ (glueᴾ tt) ⟩

          P.trans lemma (P.trans (glueᴾ tt) (P.cong inr loopᴾ))  P.≡⟨ PT.prove
                                                                        (PT.Trans Lemma (PT.Trans Glue Loop))
                                                                        (PT.Trans Glue (PT.Trans (PT.Sym Loop)
                                                                                (PT.Trans (PT.Trans (PT.Sym Glue) Glue) Loop)))
                                                                        P.refl ⟩
          P.trans (glueᴾ tt)
            (P.trans (P.sym (P.cong inr loopᴾ))
               (P.trans (P.trans (P.sym (glueᴾ tt)) (glueᴾ tt))
                  (P.cong inr loopᴾ)))                           P.≡⟨ P.cong (λ eq → P.trans (glueᴾ tt) (P.trans (P.sym (P.cong inr loopᴾ))
                                                                                (P.trans eq (P.cong inr loopᴾ)))) $
                                                                      P.trans-symˡ _ ⟩
          P.trans (glueᴾ tt)
            (P.trans (P.sym (P.cong inr loopᴾ))
               (P.trans P.refl
                  (P.cong inr loopᴾ)))                           P.≡⟨ P.cong (λ eq → P.trans (glueᴾ tt)
                                                                                (P.trans (P.sym (P.cong inr loopᴾ)) eq)) $
                                                                      P.trans-reflˡ _ ⟩
          P.trans (glueᴾ tt)
            (P.trans (P.sym (P.cong inr loopᴾ))
               (P.cong inr loopᴾ))                               P.≡⟨ P.cong (P.trans (glueᴾ tt)) $ P.trans-symˡ _ ⟩

          P.trans (glueᴾ tt) P.refl                              P.≡⟨ P.trans-reflʳ _ ⟩∎

          glueᴾ tt                                               ∎)))
      (λ _ → PB._↔_.from (P.heterogeneous↔homogeneous _) (
         P.subst (inl base P.≡_) (glueᴾ tt) P.refl  P.≡⟨ P.sym $ P.trans-subst {x≡y = P.refl} ⟩
         P.trans P.refl (glueᴾ tt)                  P.≡⟨ P.trans-reflˡ _ ⟩∎
         glueᴾ tt                                   ∎))

  from∘to : ∀ x → from (to x) P.≡ x
  from∘to base       = P.refl
  from∘to (loop₁ᴾ i) = P.refl
  from∘to (loop₂ᴾ i) = lemma′ i
    where
    lemma′ : P.[ (λ i → P.cong from (P.sym lemma) i P.≡ loop₂ᴾ i) ]
               P.refl ≡ P.refl
    lemma′ = PB._↔_.from (P.heterogeneous↔homogeneous _) (
      P.transport (λ i → P.cong from (P.sym lemma) i P.≡ loop₂ᴾ i)
        P.0̲ P.refl                                                     P.≡⟨ P.transport-≡ P.refl ⟩

      P.trans (P.cong from lemma) (P.trans P.refl loop₂ᴾ)              P.≡⟨ PT.prove
                                                                              (PT.Trans (PT.Cong from Lemma) (PT.Trans PT.Refl Loop₂))
                                                                              (PT.Trans (PT.Trans (PT.Cong from Glue)
                                                                                (PT.Trans (PT.Cong from (PT.Sym Loop))
                                                                                (PT.Cong from (PT.Sym Glue))))
                                                                                Loop₂)
                                                                              P.refl ⟩
      P.trans (P.trans (P.cong from (glueᴾ tt))
                 (P.trans (P.cong from (P.sym (P.cong inr loopᴾ)))
                    (P.cong from (P.sym (glueᴾ tt)))))
        loop₂ᴾ                                                         P.≡⟨⟩

      P.trans (P.trans P.refl (P.trans (P.sym loop₂ᴾ) P.refl)) loop₂ᴾ  P.≡⟨ P.cong (flip P.trans loop₂ᴾ) $
                                                                            P.trans-reflˡ (P.trans (P.sym loop₂ᴾ) P.refl) ⟩

      P.trans (P.trans (P.sym loop₂ᴾ) P.refl) loop₂ᴾ                   P.≡⟨ P.cong (flip P.trans loop₂ᴾ) $
                                                                            P.trans-reflʳ (P.sym loop₂ᴾ) ⟩

      P.trans (P.sym loop₂ᴾ) loop₂ᴾ                                    P.≡⟨ P.trans-symˡ _ ⟩∎

      P.refl                                                           ∎)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Prelude

module Implicits.Resolution.Infinite.Algorithm.Soundness where

open import Data.Vec hiding (_∈_)
open import Data.List hiding (map)
open import Data.List.Any hiding (tail)
open Membership-≡
open import Data.Bool
open import Data.Unit.Base
open import Data.Maybe as Maybe hiding (All)
open import Coinduction
open import Data.Fin.Substitution
open import Implicits.Syntax
open import Implicits.Substitutions
open import Implicits.Substitutions.MetaType
open import Implicits.Substitutions.Lemmas
open import Implicits.Syntax.Type.Unification
open import Implicits.Syntax.Type.Unification.Lemmas renaming (sound to mgu-sound)
open import Implicits.Resolution.Infinite.Resolution
open import Implicits.Resolution.Infinite.Algorithm
open import Implicits.Resolution.Termination
open Inductive

open import Induction.WellFounded
open import Category.Functor
open import Category.Monad.Partiality as P
open import Category.Monad.Partiality.All using (All; module Alternative)
open Alternative renaming (sound to AllP-sound)

private module MaybeFunctor {f} = RawFunctor (functor {f})

open import Extensions.Bool as B hiding (All)
open import Relation.Binary.PropositionalEquality as PEq using (_≡_)
module PR = P.Reasoning (PEq.isEquivalence {A = Bool})

private
  module M = MetaTypeMetaSubst

  postulate lem₄ : ∀ {m ν} (a : MetaType m (suc ν)) u us →
                    from-meta (((M.open-meta a) M./ (us M.↑)) M./ (M.sub u))
                      ≡ (from-meta (a M./ (us M.↑tp))) tp[/tp from-meta u ]

open-↓-∀ : ∀ {ν m} {Δ : ICtx ν} (a : MetaType m (suc ν)) τ u us →
      Δ ⊢ (from-meta ((open-meta a) M./ (u ∷ us))) ↓ τ →
      Δ ⊢ (from-meta (∀' a M./ us)) ↓ τ
open-↓-∀ {Δ = Δ} a τ u us p = (i-tabs (from-meta u) (subst (λ v → Δ ⊢ v ↓ τ) (begin
      from-meta (M._/_ (open-meta a) (u ∷ us))
        ≡⟨ cong (λ v → from-meta (M._/_ (open-meta a) v)) (sym $ us↑-⊙-sub-u≡u∷us u us) ⟩
      from-meta ((open-meta a) M./ (us M.↑ M.⊙ (M.sub u)))
        ≡⟨ cong from-meta (/-⊙ (open-meta a)) ⟩
      from-meta ((open-meta a) M./ us M.↑ M./ (M.sub u))
        ≡⟨ lem₄ a u us ⟩
      from-meta (M._/_ a (us M.↑tp)) tp[/tp from-meta u ] ∎) p))
    where open MetaTypeMetaLemmas hiding (subst)

mutual

  delayed-resolve-sound : ∀ {ν} (Δ : ICtx ν) (a : Type ν) →
                          AllP (B.All (Δ ⊢ᵣ a)) (delayed-resolve Δ a)
  delayed-resolve-sound Δ a = later (♯ (resolve'-sound Δ a))

  resolve-context-sound : ∀ {ν m} (Δ : ICtx ν) (a : MetaType m ν) b {τ v} →
                          Maybe.All (λ u → Δ ⊢ from-meta (b M./ u) ↓ τ) v →
                          AllP (Maybe.All (λ u →
                            (Δ ⊢ from-meta (a M./ u) ⇒ from-meta (b M./ u) ↓ τ))
                          ) (resolve-context Δ a v)
  resolve-context-sound Δ a b {τ = τ} (just {x = u} px) = _
    ≅⟨ resolve-context-comp Δ a u ⟩P delayed-resolve-sound Δ (from-meta (M._/_ a u)) >>=-congP lem
    where
      lem : ∀ {v} → B.All (Δ ⊢ᵣ from-meta (a M./ u)) v →
            AllP (Maybe.All (λ u → Δ ⊢ from-meta (a M./ u) ⇒ from-meta (b M./ u) ↓ τ)) (map-bool u v)
      lem (true x) = now (just (i-iabs x px))
      lem (false) = now nothing
  resolve-context-sound Δ a b nothing = now nothing

  match-u-sound : ∀ {ν m} (Δ : ICtx ν) τ (r : MetaType m ν) → (r-acc : m<-Acc r) →
                  AllP (Maybe.All (λ u → (Δ ⊢ from-meta (r M./ u) ↓ τ))) (match-u Δ τ r r-acc)
  match-u-sound Δ τ (a ⇒ b) (acc rs) = _ ≅⟨ match-u-iabs-comp Δ τ a b rs ⟩P
    match-u-sound Δ τ b (rs _ (b-m<-a⇒b a b)) >>=-congP resolve-context-sound Δ a b
  match-u-sound Δ τ (∀' r) (acc rs) = _ ≅⟨ match-u-tabs-comp Δ τ r rs ⟩P
    match-u-sound Δ τ (open-meta r) _ >>=-congP lem
    where
      lem : ∀ {v} → Maybe.All (λ u → Δ ⊢ from-meta (open-meta r M./ u) ↓ τ) v →
            AllP (Maybe.All (λ u → Δ ⊢ ∀' (from-meta (r M./ u M.↑tp)) ↓ τ ))
                ((now ∘ (MaybeFunctor._<$>_ tail)) v)
      lem (just {x = u ∷ us} px) = now (just (open-↓-∀ r τ u us px))
      lem nothing = now nothing
  match-u-sound Δ τ (simpl x) (acc rs) with mgu (simpl x) τ | mgu-sound (simpl x) τ
  match-u-sound Δ τ (simpl x) (acc rs) | just us | just x/us≡τ =
    now (just (subst (λ z → Δ ⊢ z ↓ τ) (sym x/us≡τ) (i-simp τ)))
  match-u-sound Δ τ (simpl x) (acc rs) | nothing | nothing = now nothing

  match-sound : ∀ {ν} (Δ : ICtx ν) τ r →
                AllP (B.All (Δ ⊢ r ↓ τ)) (match Δ τ r)
  match-sound Δ τ r = _
    ≅⟨ match-comp Δ τ r ⟩P
    match-u-sound Δ τ (to-meta {zero} r) (m<-well-founded _) >>=-congP lem
    where
      eq : ∀ {ν} {a : Type ν} {s} → from-meta (to-meta {zero} a M./ s) ≡ a
      eq {a = a} {s = []} = begin
          from-meta (M._/_ (to-meta {zero} a) [])
        ≡⟨ cong (λ q → from-meta q) (MetaTypeMetaLemmas.id-vanishes (to-meta {zero} a)) ⟩
          from-meta (to-meta {zero} a)
        ≡⟨ to-meta-zero-vanishes ⟩
          a ∎

      lem : ∀ {v} → Maybe.All (λ u → (Δ ⊢ from-meta ((to-meta {zero} r) M./ u) ↓ τ)) v →
            AllP (B.All (Δ ⊢ r ↓ τ)) ((now ∘ is-just) v)
      lem (just px) = now (true (subst (λ z → Δ ⊢ z ↓ τ) eq px))
      lem nothing = now false

  match1st-recover-sound : ∀ {ν b} x (Δ ρs : ICtx ν) τ → B.All (Δ ⊢ x ↓ τ) b →
                          AllP (B.All (∃₂ λ r (r∈Δ : r ∈ (x ∷ ρs)) → Δ ⊢ r ↓ τ))
                                (match1st-recover Δ ρs τ b)
  match1st-recover-sound x Δ ρs τ (true p) = now (true (x , (here refl) , p))
  match1st-recover-sound x Δ ρs τ false = _
    ≅⟨ PR.sym (right-identity refl (match1st Δ ρs τ)) ⟩P
    match1st'-sound Δ ρs τ >>=-congP lem
    where
      lem : ∀ {v} → B.All (∃₂ λ r (r∈Δ : r ∈ ρs)→ Δ ⊢ r ↓ τ) v →
            AllP (B.All (∃₂ λ r (r∈Δ : r ∈ x ∷ ρs) → Δ ⊢ r ↓ τ)) (now v)
      lem (true (r , r∈ρs , p)) = now (true (r , (there r∈ρs) , p))
      lem false = now false

    -- {!match1st'-sound Δ ρs τ!}

  match1st'-sound : ∀ {ν} (Δ ρs : ICtx ν) τ →
                    AllP (B.All (∃₂ λ r (r∈Δ : r ∈ ρs) → Δ ⊢ r ↓ τ)) (match1st Δ ρs τ)
  match1st'-sound Δ [] τ = now false
  match1st'-sound Δ (x ∷ ρs) τ = _
    ≅⟨ match1st-comp Δ x ρs τ ⟩P
    match-sound Δ τ x >>=-congP match1st-recover-sound x Δ ρs τ

  resolve'-sound : ∀ {ν} (Δ : ICtx ν) r → AllP (B.All (Δ ⊢ᵣ r)) (resolve Δ r)
  resolve'-sound Δ (simpl x) = _
    ≅⟨ PR.sym (right-identity refl (match1st Δ Δ x)) ⟩P
    match1st'-sound Δ Δ x >>=-congP (λ x → now (B.all-map x (λ{ (r , r∈Δ , p) → r-simp r∈Δ p })))
  resolve'-sound Δ (a ⇒ b) = _
    ≅⟨ PR.sym (right-identity refl (resolve (a ∷ Δ) b)) ⟩P
    resolve'-sound (a ∷ Δ) b >>=-congP (λ x → now (B.all-map x r-iabs))
  resolve'-sound Δ (∀' r) = _
    ≅⟨ PR.sym (right-identity refl (resolve (ictx-weaken Δ) r)) ⟩P
    resolve'-sound (ictx-weaken Δ) r >>=-congP (λ x → now (B.all-map x r-tabs))

  -- Soundness means:
  -- for all terminating runs of the algorithm we have a finite resolution proof.
  sound : ∀ {ν} (Δ : ICtx ν) r → All (B.All (Δ ⊢ᵣ r)) (resolve Δ r)
  sound Δ r = AllP-sound (resolve'-sound Δ r)

ext: agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
{-
This file contains a proof that the generator of Π₃S² has
hopf invariant ±1.
-}
module Cubical.Homotopy.HopfInvariant.HopfMap where

open import Cubical.Homotopy.HopfInvariant.Base
open import Cubical.Homotopy.Hopf
open S¹Hopf
open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.HSpace

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.Groups.Sn
open import Cubical.ZCohomology.RingStructure.CupProduct
open import Cubical.ZCohomology.RingStructure.RingLaws
open import Cubical.ZCohomology.Gysin

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Path
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Pointed.Homogeneous
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence

open import Cubical.Data.Sum
open import Cubical.Data.Sigma
open import Cubical.Data.Int hiding (_+'_)
open import Cubical.Data.Nat renaming (_+_ to _+ℕ_ ; _·_ to _·ℕ_)
open import Cubical.Data.Unit

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.ZAction
open import Cubical.Algebra.Group.Exact
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Int
open import Cubical.Algebra.Group.GroupPath

open import Cubical.HITs.Pushout
open import Cubical.HITs.Join
open import Cubical.HITs.S1 renaming (_·_ to _*_)
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp
open import Cubical.HITs.Truncation
  renaming (rec to trRec ; elim to trElim)
open import Cubical.HITs.SetTruncation
  renaming (rec to sRec ; rec2 to sRec2
          ; elim to sElim ; elim2 to sElim2 ; map to sMap)
open import Cubical.HITs.PropositionalTruncation
  renaming (rec to pRec)

HopfMap : S₊∙ 3 →∙ S₊∙ 2
fst HopfMap x = JoinS¹S¹→TotalHopf (Iso.inv (IsoSphereJoin 1 1) x) .fst
snd HopfMap = refl

-- We use the Hopf fibration in order to connect it to the Gysin Sequence
module hopfS¹ =
  Hopf S1-AssocHSpace (sphereElim2 _ (λ _ _ → squash₁) ∣ refl ∣₁)

S¹Hopf = hopfS¹.Hopf
E* = hopfS¹.TotalSpacePush²'
IsoE*join = hopfS¹.joinIso₂
IsoTotalHopf' = hopfS¹.joinIso₁
CP² = hopfS¹.TotalSpaceHopfPush²
fibr = hopfS¹.P

TotalHopf' : Type _
TotalHopf' = Σ (S₊ 2) S¹Hopf

IsoJoins : (join S¹ (join S¹ S¹)) ≡ join S¹ (S₊ 3)
IsoJoins = cong (join S¹) (isoToPath (IsoSphereJoin 1 1))

-- CP² is 1-connected
conCP² : (x y : CP²) → ∥ x ≡ y ∥₂
conCP² x y = sRec2 squash₂ (λ p q → ∣ p ∙ sym q ∣₂) (conCP²' x) (conCP²' y)
  where
  conCP²' : (x : CP²) → ∥ x ≡ inl tt ∥₂
  conCP²' (inl x) = ∣ refl ∣₂
  conCP²' (inr x) = sphereElim 1 {A = λ x → ∥ inr x ≡ inl tt ∥₂}
                                 (λ _ → squash₂) ∣ sym (push (inl base)) ∣₂ x
  conCP²' (push a i) = main a i
    where
    indLem : ∀ {ℓ} {A : hopfS¹.TotalSpaceHopfPush → Type ℓ}
        → ((a : _) → isProp (A a))
        → A (inl base)
        → ((a : hopfS¹.TotalSpaceHopfPush) → A a)
    indLem {A = A} p b =
      PushoutToProp p
        (sphereElim 0 (λ _ → p _) b)
        (sphereElim 0 (λ _ → p _) (subst A (push (base , base)) b))

    main : (a : hopfS¹.TotalSpaceHopfPush)
         → PathP (λ i → ∥ Path CP² (push a i) (inl tt) ∥₂)
                  (conCP²' (inl tt)) (conCP²' (inr (hopfS¹.induced a)))
    main = indLem (λ _ → isOfHLevelPathP' 1 squash₂ _ _)
                   λ j → ∣ (λ i → push (inl base) (~ i ∧ j)) ∣₂

module GysinS² = Gysin (CP² , inl tt) fibr conCP² 2 idIso refl

E'S⁴Iso : Iso GysinS².E' (S₊ 5)
E'S⁴Iso =
  compIso IsoE*join
    (compIso (Iso→joinIso idIso (IsoSphereJoin 1 1))
             (IsoSphereJoin 1 3))

isContrH³E : isContr (coHom 3 (GysinS².E'))
isContrH³E =
  subst isContr (sym (isoToPath
                      (fst (Hⁿ-Sᵐ≅0 2 4
                      λ p → snotz (sym (cong (predℕ ∘ predℕ) p)))))
               ∙ cong (coHom 3) (sym (isoToPath E'S⁴Iso)))
        isContrUnit

isContrH⁴E : isContr (coHom 4 (GysinS².E'))
isContrH⁴E =
  subst isContr (sym (isoToPath
                     (fst (Hⁿ-Sᵐ≅0 3 4
                       λ p → snotz (sym (cong (predℕ ∘ predℕ ∘ predℕ) p)))))
               ∙ cong (coHom 4) (sym (isoToPath E'S⁴Iso)))
        isContrUnit

-- We will need a bunch of elimination principles
joinS¹S¹→Groupoid : ∀ {ℓ} (P : join S¹ S¹ → Type ℓ)
            → ((x : _) → isGroupoid (P x))
            → P (inl base)
            → (x : _) → P x
joinS¹S¹→Groupoid P grp b =
  transport (λ i → (x : (isoToPath (invIso (IsoSphereJoin 1 1))) i)
        → P (transp (λ j → isoToPath (invIso (IsoSphereJoin 1 1)) (i ∨ j)) i x))
        (sphereElim _ (λ _ → grp _) b)

TotalHopf→Gpd : ∀ {ℓ} (P : hopfS¹.TotalSpaceHopfPush → Type ℓ)
            → ((x : _) → isGroupoid (P x))
            → P (inl base)
            → (x : _) → P x
TotalHopf→Gpd P grp b =
  transport (λ i → (x : sym (isoToPath IsoTotalHopf') i)
                 → P (transp (λ j → isoToPath IsoTotalHopf' (~ i ∧ ~ j)) i x))
    (joinS¹S¹→Groupoid _ (λ _ → grp _) b)

TotalHopf→Gpd' : ∀ {ℓ} (P : Σ (S₊ 2) hopfS¹.Hopf → Type ℓ)
            → ((x : _) → isGroupoid (P x))
            → P (north , base)
            → (x : _) → P x
TotalHopf→Gpd' P grp b =
  transport (λ i → (x : ua (_ , hopfS¹.isEquivTotalSpaceHopfPush→TotalSpace) i)
          → P (transp (λ j → ua (_ , hopfS¹.isEquivTotalSpaceHopfPush→TotalSpace)
                                  (i ∨ j)) i x))
          (TotalHopf→Gpd _ (λ _ → grp _) b)

CP²→Groupoid : ∀ {ℓ} {P : CP² → Type ℓ}
               → ((x : _) → is2Groupoid (P x))
               → (b : P (inl tt))
               → (s2 : ((x : _) → P (inr x)))
               → PathP (λ i → P (push (inl base) i)) b (s2 north)
               → (x : _) → P x
CP²→Groupoid {P = P} grp b s2 pp (inl x) = b
CP²→Groupoid {P = P} grp b s2 pp (inr x) = s2 x
CP²→Groupoid {P = P} grp b s2 pp (push a i₁) = lem a i₁
  where
  lem : (a : hopfS¹.TotalSpaceHopfPush) → PathP (λ i → P (push a i)) b (s2 _)
  lem = TotalHopf→Gpd _  (λ _ → isOfHLevelPathP' 3 (grp _) _ _) pp

-- The function inducing the iso H²(S²) ≅ H²(CP²)
H²S²→H²CP²-raw : (S₊ 2 → coHomK 2) → (CP² → coHomK 2)
H²S²→H²CP²-raw f (inl x) = 0ₖ _
H²S²→H²CP²-raw f (inr x) = f x -ₖ f north
H²S²→H²CP²-raw f (push a i) =
    TotalHopf→Gpd (λ x → 0ₖ 2
  ≡ f (hopfS¹.TotalSpaceHopfPush→TotalSpace x .fst) -ₖ f north)
      (λ _ → isOfHLevelTrunc 4 _ _)
      (sym (rCancelₖ 2 (f north)))
      a i

H²S²→H²CP² : coHomGr 2 (S₊ 2) .fst → coHomGr 2 CP² .fst
H²S²→H²CP² = sMap H²S²→H²CP²-raw

cancel-H²S²→H²CP² : (f : CP² → coHomK 2)
  → ∥ H²S²→H²CP²-raw (f ∘ inr) ≡ f ∥₁
cancel-H²S²→H²CP² f =
  pRec squash₁
    (λ p → pRec squash₁
                (λ f → ∣ funExt f ∣₁)
                (cancelLem p))
    (connLem (f (inl tt)))
  where
  connLem : (x : coHomK 2) →  ∥ x ≡ 0ₖ 2 ∥₁
  connLem = coHomK-elim _ (λ _ → isOfHLevelSuc 1 squash₁) ∣ refl ∣₁

  cancelLem : (p : f (inl tt) ≡ 0ₖ 2)
    → ∥ ((x : CP²) → H²S²→H²CP²-raw (f ∘ inr) x ≡ f x) ∥₁
  cancelLem p = trRec squash₁ (λ pp →
    ∣ CP²→Groupoid (λ _ → isOfHLevelPath 4 (isOfHLevelTrunc 4) _ _)
                 (sym p)
                 (λ x → (λ i → f (inr x) -ₖ f (push (inl base) (~ i)))
                       ∙∙ (λ i → f (inr x) -ₖ p i)
                       ∙∙ rUnitₖ 2 (f (inr x))) pp ∣₁)
                help
    where
    help :
      hLevelTrunc 1
        (PathP (λ i₁ → H²S²→H²CP²-raw (f ∘ inr) (push (inl base) i₁)
                     ≡ f (push (inl base) i₁))
              (sym p)
              (((λ i₁ → f (inr north) -ₖ f (push (inl base) (~ i₁))) ∙∙
                (λ i₁ → f (inr north) -ₖ p i₁) ∙∙ rUnitₖ 2 (f (inr north)))))
    help = isConnectedPathP 1 (isConnectedPath 2 (isConnectedKn 1) _ _) _ _ .fst

H²CP²≅H²S² : GroupIso (coHomGr 2 CP²) (coHomGr 2 (S₊ 2))
Iso.fun (fst H²CP²≅H²S²) = sMap (_∘ inr)
Iso.inv (fst H²CP²≅H²S²) = H²S²→H²CP²
Iso.rightInv (fst H²CP²≅H²S²) =
  sElim (λ _ → isOfHLevelPath 2 squash₂ _ _)
    λ f → trRec {B = Iso.fun (fst H²CP²≅H²S²) (Iso.inv (fst H²CP²≅H²S²) ∣ f ∣₂)
                   ≡ ∣ f ∣₂}
    (isOfHLevelPath 2 squash₂ _ _)
    (λ p → cong ∣_∣₂ (funExt λ x → cong (λ y → (f x) -ₖ y) p ∙ rUnitₖ 2 (f x)))
    (Iso.fun (PathIdTruncIso _)
             (isContr→isProp (isConnectedKn 1) ∣ f north ∣ ∣ 0ₖ 2 ∣))
Iso.leftInv (fst H²CP²≅H²S²) =
  sElim (λ _ → isOfHLevelPath 2 squash₂ _ _)
    λ f → pRec (squash₂ _ _) (cong ∣_∣₂) (cancel-H²S²→H²CP² f)
snd H²CP²≅H²S² =
  makeIsGroupHom
    (sElim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _) λ f g → refl)

H²CP²≅ℤ : GroupIso (coHomGr 2 CP²) ℤGroup
H²CP²≅ℤ = compGroupIso H²CP²≅H²S² (Hⁿ-Sⁿ≅ℤ 1)

-- ⌣ gives a groupEquiv H²(CP²) ≃ H⁴(CP²)
⌣Equiv : GroupEquiv (coHomGr 2 CP²) (coHomGr 4 CP²)
fst (fst ⌣Equiv) = GysinS².⌣-hom 2 .fst
snd (fst ⌣Equiv) = isEq⌣
  where
  isEq⌣ : isEquiv (GysinS².⌣-hom 2 .fst)
  isEq⌣ =
    SES→isEquiv
      (GroupPath _ _ .fst (invGroupEquiv
        (isContr→≃Unit isContrH³E
        , makeIsGroupHom λ _ _ → refl)))
      (GroupPath _ _ .fst (invGroupEquiv
        (isContr→≃Unit isContrH⁴E
        , makeIsGroupHom λ _ _ → refl)))
      (GysinS².susp∘ϕ 1)
      (GysinS².⌣-hom 2)
      (GysinS².p-hom 4)
      (GysinS².Ker-⌣e⊂Im-Susp∘ϕ _)
      (GysinS².Ker-p⊂Im-⌣e _)
snd ⌣Equiv = GysinS².⌣-hom 2 .snd

-- The generator of H²(CP²)
genCP² : coHom 2 CP²
genCP² = ∣ CP²→Groupoid (λ _ → isOfHLevelTrunc 4)
                      (0ₖ _)
                      ∣_∣
                      refl ∣₂

inrInjective : (f g : CP² → coHomK 2) → ∥ f ∘ inr ≡ g ∘ inr ∥₁
             → Path (coHom 2 CP²) ∣ f ∣₂ ∣ g ∣₂
inrInjective f g = pRec (squash₂ _ _)
  (λ p → pRec (squash₂ _ _) (λ id → trRec (squash₂ _ _)
               (λ pp → cong ∣_∣₂
                 (funExt (CP²→Groupoid
                           (λ _ → isOfHLevelPath 4 (isOfHLevelTrunc 4) _ _)
                         id
                         (funExt⁻ p)
                         (compPathR→PathP pp))))
                   (conn2 (f (inl tt)) (g (inl tt)) id
                     (cong f (push (inl base))
                       ∙ (funExt⁻ p north) ∙ cong g (sym (push (inl base))))))
               (conn (f (inl tt)) (g (inl tt))))

  where
  conn : (x y : coHomK 2) → ∥ x ≡ y ∥₁
  conn = coHomK-elim _ (λ _ → isSetΠ λ _ → isOfHLevelSuc 1 squash₁)
           (coHomK-elim _ (λ _ → isOfHLevelSuc 1 squash₁) ∣ refl ∣₁)

  conn2 : (x y : coHomK 2) (p q : x ≡ y) → hLevelTrunc 1 (p ≡ q)
  conn2 x y p q =
    Iso.fun (PathIdTruncIso _)
      (isContr→isProp (isConnectedPath _ (isConnectedKn 1) x y) ∣ p ∣ ∣ q ∣)

-- A couple of basic lemma concerning the hSpace structure on S¹
private
  invLooperLem₁ : (a x : S¹)
    → (invEq (hopfS¹.μ-eq a) x) * a ≡ (invLooper a * x) * a
  invLooperLem₁ a x =
       secEq (hopfS¹.μ-eq a) x
    ∙∙ cong (_* x) (rCancelS¹ a)
    ∙∙ AssocHSpace.μ-assoc S1-AssocHSpace a (invLooper a) x
     ∙ commS¹ _ _

  invLooperLem₂ : (a x : S¹) → invEq (hopfS¹.μ-eq a) x ≡ invLooper a * x
  invLooperLem₂ a x = sym (retEq (hopfS¹.μ-eq a) (invEq (hopfS¹.μ-eq a) x))
          ∙∙ cong (invEq (hopfS¹.μ-eq a)) (invLooperLem₁ a x)
          ∙∙ retEq (hopfS¹.μ-eq a) (invLooper a * x)

  rotLoop² : (a : S¹) → Path (a ≡ a) (λ i → rotLoop (rotLoop a i) (~ i)) refl
  rotLoop² =
    sphereElim 0 (λ _ → isGroupoidS¹ _ _ _ _)
      λ i j → hcomp (λ {k → λ { (i = i1) → base
                                ; (j = i0) → base
                                ; (j = i1) → base}})
                    base

-- We prove that the generator of CP² given by Gysin is the same one
-- as genCP², which is much easier to work with
Gysin-e≡genCP² : GysinS².e ≡ genCP²
Gysin-e≡genCP² =
  inrInjective _ _ ∣ funExt (λ x → funExt⁻ (cong fst (main x)) south) ∣₁
  where
  mainId : (x : Σ (S₊ 2) hopfS¹.Hopf)
         → Path (hLevelTrunc 4 _) ∣ fst x ∣ ∣ north ∣
  mainId = uncurry λ { north → λ y → cong ∣_∣ₕ (merid base ∙ sym (merid y))
                     ; south → λ y → cong ∣_∣ₕ (sym (merid y))
                     ; (merid a i) → main a i}
    where
    main : (a : S¹) → PathP (λ i → (y : hopfS¹.Hopf (merid a i))
                    → Path (HubAndSpoke (Susp S¹) 3) ∣ merid a i ∣ ∣ north ∣)
                            (λ y → cong ∣_∣ₕ (merid base ∙ sym (merid y)))
                            λ y → cong ∣_∣ₕ (sym (merid y))
    main a =
      toPathP
        (funExt λ x →
          cong (transport (λ i₁
               → Path (HubAndSpoke (Susp S¹) 3) ∣ merid a i₁ ∣ ∣ north ∣))
               ((λ i → (λ z → cong ∣_∣ₕ
                         (merid base
                        ∙ sym (merid (transport
                            (λ j → uaInvEquiv (hopfS¹.μ-eq a) (~ i) j) x))) z))
               ∙ λ i → cong ∣_∣ₕ (merid base
                     ∙ sym (merid (transportRefl (invEq (hopfS¹.μ-eq a) x) i))))
      ∙∙ (λ i → transp (λ i₁ → Path (HubAndSpoke (Susp S¹) 3)
                                      ∣ merid a (i₁ ∨ i) ∣ ∣ north ∣) i
                        (compPath-filler' (cong ∣_∣ₕ (sym (merid a)))
                          (cong ∣_∣ₕ (merid base
                                  ∙ sym (merid (invLooperLem₂ a x i)))) i))
      ∙∙ cong ((cong ∣_∣ₕ) (sym (merid a)) ∙_)
          (cong (cong ∣_∣ₕ) (cong sym (symDistr (merid base)
                                               (sym (merid (invLooper a * x)))))
         ∙ cong sym (SuspS¹-hom (invLooper a) x)
         ∙ symDistr ((cong ∣_∣ₕ) (merid (invLooper a) ∙ sym (merid base)))
                     ((cong ∣_∣ₕ) (merid x ∙ sym (merid base)))
         ∙ isCommΩK 2 (sym (λ i₁ → ∣ (merid x
                                   ∙ (λ i₂ → merid base (~ i₂))) i₁ ∣))
                      (sym (λ i₁ → ∣ (merid (invLooper a)
                                   ∙ (λ i₂ → merid base (~ i₂))) i₁ ∣))
         ∙ cong₂ _∙_ (cong sym (SuspS¹-inv a)
                       ∙ cong-∙ ∣_∣ₕ (merid a) (sym (merid base)))
                     (cong (cong ∣_∣ₕ) (symDistr (merid x) (sym (merid base)))
                       ∙ cong-∙ ∣_∣ₕ (merid base) (sym (merid x))))
      ∙∙ (λ j → (λ i₁ → ∣ merid a (~ i₁ ∨ j) ∣) ∙ ((λ i₁ → ∣ merid a (i₁ ∨ j) ∣)
                 ∙ (λ i₁ → ∣ merid base (~ i₁ ∨ j) ∣))
                 ∙ (λ i₁ → ∣ merid base (i₁ ∨ j) ∣)
                 ∙ (λ i₁ → ∣ merid x (~ i₁) ∣ₕ))
      ∙∙ sym (lUnit _)
      ∙∙ sym (assoc _ _ _)
      ∙∙ (sym (lUnit _) ∙ sym (lUnit _) ∙ sym (lUnit _)))

  gen' : (x : S₊ 2) → preThom.Q (CP² , inl tt) fibr (inr x) →∙ coHomK-ptd 2
  fst (gen' x) north = ∣ north ∣
  fst (gen' x) south = ∣ x ∣
  fst (gen' x) (merid a i₁) = mainId (x , a) (~ i₁)
  snd (gen' x) = refl

  gen'Id : GysinS².c (inr north) .fst ≡ gen' north .fst
  gen'Id = cong fst (GysinS².cEq (inr north) ∣ push (inl base) ∣₂)
           ∙ (funExt lem)
    where
    lem : (qb : _) →
       ∣ (subst (fst ∘ preThom.Q (CP² , inl tt) fibr)
                (sym (push (inl base))) qb) ∣
      ≡ gen' north .fst qb
    lem north = refl
    lem south = cong ∣_∣ₕ (sym (merid base))
    lem (merid a i) j =
      hcomp (λ k →
        λ { (i = i0) → ∣ merid a (~ k ∧ j) ∣
          ; (i  = i1) → ∣ merid base (~ j) ∣
          ; (j = i0) → ∣ transportRefl (merid a i) (~ k) ∣
          ; (j = i1) → ∣ compPath-filler
                          (merid base) (sym (merid a)) k (~ i) ∣ₕ})
            (hcomp (λ k →
              λ { (i = i0) → ∣ merid a (j ∨ ~ k) ∣
                ; (i  = i1) → ∣ merid base (~ j ∨ ~ k) ∣
                ; (j = i0) → ∣ merid a (~ k ∨ i) ∣
                ; (j = i1) → ∣ merid base (~ i ∨ ~ k) ∣ₕ})
             ∣ south ∣)

  setHelp : (x : S₊ 2)
    → isSet (preThom.Q (CP² , inl tt) fibr (inr x) →∙ coHomK-ptd 2)
  setHelp = sphereElim _ (λ _ → isProp→isOfHLevelSuc 1 (isPropIsOfHLevel 2))
                            (isOfHLevel↑∙' 0 1)

  main : (x : S₊ 2) →  (GysinS².c (inr x) ≡ gen' x)
  main = sphereElim _ (λ x → isOfHLevelPath 2 (setHelp x) _ _)
         (→∙Homogeneous≡ (isHomogeneousKn _) gen'Id)

isGenerator≃ℤ : ∀ {ℓ} (G : Group ℓ) (g : fst G) → Type ℓ
isGenerator≃ℤ G g =
  Σ[ e ∈ GroupIso G ℤGroup ] abs (Iso.fun (fst e) g) ≡ 1

isGenerator≃ℤ-e : isGenerator≃ℤ (coHomGr 2 CP²) GysinS².e
isGenerator≃ℤ-e =
  subst (isGenerator≃ℤ (coHomGr 2 CP²)) (sym Gysin-e≡genCP²)
    (H²CP²≅ℤ , refl)

-- Alternative definition of the hopfMap
HopfMap' : S₊ 3 → S₊ 2
HopfMap' x =
  hopfS¹.TotalSpaceHopfPush→TotalSpace
    (Iso.inv IsoTotalHopf'
      (Iso.inv (IsoSphereJoin 1 1) x)) .fst

hopfMap≡HopfMap' : HopfMap ≡ (HopfMap' , refl)
hopfMap≡HopfMap' =
  ΣPathP ((funExt (λ x →
            cong (λ x → JoinS¹S¹→TotalHopf x .fst)
              (sym (Iso.rightInv IsoTotalHopf'
                   (Iso.inv (IsoSphereJoin 1 1) x)))
             ∙ sym (lem (Iso.inv IsoTotalHopf'
                   (Iso.inv (IsoSphereJoin 1 1) x)))))
         , flipSquare (sym (rUnit refl) ◁ λ _ _ → north))
  where
  lem : (x : _) → hopfS¹.TotalSpaceHopfPush→TotalSpace x .fst
               ≡ JoinS¹S¹→TotalHopf (Iso.fun IsoTotalHopf' x) .fst
  lem (inl x) = refl
  lem (inr x) = refl
  lem (push (base , snd₁) i) = refl
  lem (push (loop i₁ , a) i) k = merid (rotLoop² a (~ k) i₁) i

CP²' : Type _
CP²' = Pushout {A = S₊ 3} (λ _ → tt) HopfMap'

PushoutReplaceBase : ∀ {ℓ ℓ' ℓ''} {A B : Type ℓ} {C : Type ℓ'} {D : Type ℓ''}
       {f : A → C} {g : A → D} (e : B ≃ A)
    → Pushout (f ∘ fst e) (g ∘ fst e) ≡ Pushout f g
PushoutReplaceBase {f = f} {g = g} =
  EquivJ (λ _ e → Pushout (f ∘ fst e) (g ∘ fst e) ≡ Pushout f g) refl

CP2≡CP²' : CP²' ≡ CP²
CP2≡CP²' =
  PushoutReplaceBase
    (isoToEquiv (compIso (invIso (IsoSphereJoin 1 1)) (invIso IsoTotalHopf')))

-- packaging everything up:
⌣equiv→pres1 : ∀ {ℓ} {G H : Type ℓ} → (G ≡ H)
        → (g₁ : coHom 2 G) (h₁ : coHom 2 H)
        → (fstEq : (Σ[ ϕ ∈ GroupEquiv (coHomGr 2 G) ℤGroup ]
                      abs (fst (fst ϕ) g₁) ≡ 1))
        → (sndEq : ((Σ[ ϕ ∈ GroupEquiv (coHomGr 2 H) ℤGroup ]
                      abs (fst (fst ϕ) h₁) ≡ 1)))
        → isEquiv {A = coHom 2 G} {B = coHom 4 G} (_⌣ g₁)
        → (3rdEq : GroupEquiv (coHomGr 4 H) ℤGroup)
        → abs (fst (fst 3rdEq) (h₁ ⌣ h₁)) ≡ 1
⌣equiv→pres1 {G = G} = J (λ H _ → (g₁ : coHom 2 G) (h₁ : coHom 2 H)
        → (fstEq : (Σ[ ϕ ∈ GroupEquiv (coHomGr 2 G) ℤGroup ]
                      abs (fst (fst ϕ) g₁) ≡ 1))
        → (sndEq : ((Σ[ ϕ ∈ GroupEquiv (coHomGr 2 H) ℤGroup ]
                       abs (fst (fst ϕ) h₁) ≡ 1)))
        → isEquiv {A = coHom 2 G} {B = coHom 4 G} (_⌣ g₁)
        → (3rdEq : GroupEquiv (coHomGr 4 H) ℤGroup)
        → abs (fst (fst 3rdEq) (h₁ ⌣ h₁)) ≡ 1)
              help
  where
  help : (g₁ h₁ : coHom 2 G)
        → (fstEq : (Σ[ ϕ ∈ GroupEquiv (coHomGr 2 G) ℤGroup ]
                      abs (fst (fst ϕ) g₁) ≡ 1))
        → (sndEq : ((Σ[ ϕ ∈ GroupEquiv (coHomGr 2 G) ℤGroup ]
                       abs (fst (fst ϕ) h₁) ≡ 1)))
        → isEquiv {A = coHom 2 G} {B = coHom 4 G} (_⌣ g₁)
        → (3rdEq : GroupEquiv (coHomGr 4 G) ℤGroup)
        → abs (fst (fst 3rdEq) (h₁ ⌣ h₁)) ≡ 1
  help g h (ϕ , idg) (ψ , idh) ⌣eq ξ =
    ⊎→abs _ _
      (groupEquivPresGen _
        (compGroupEquiv main (compGroupEquiv (invGroupEquiv main) ψ))
        h (abs→⊎ _ _ (cong abs (cong (fst (fst ψ)) (retEq (fst main) h))
                     ∙ idh)) (compGroupEquiv main ξ))
    where
    lem₁ : ((fst (fst ψ) h) ≡ 1) ⊎ (fst (fst ψ) h ≡ -1)
      → abs (fst (fst ϕ) h) ≡ 1
    lem₁ p = ⊎→abs _ _ (groupEquivPresGen _ ψ h p ϕ)

    lem₂ : ((fst (fst ϕ) h) ≡ 1) ⊎ (fst (fst ϕ) h ≡ -1)
          → ((fst (fst ϕ) g) ≡ 1) ⊎ (fst (fst ϕ) g ≡ -1)
          → (h ≡ g) ⊎ (h ≡ (-ₕ g))
    lem₂ (inl x) (inl x₁) =
      inl (sym (retEq (fst ϕ) h)
        ∙∙ cong (invEq (fst ϕ)) (x ∙ sym x₁)
        ∙∙ retEq (fst ϕ) g)
    lem₂ (inl x) (inr x₁) =
      inr (sym (retEq (fst ϕ) h)
        ∙∙ cong (invEq (fst ϕ)) x
         ∙ IsGroupHom.presinv (snd (invGroupEquiv ϕ)) (negsuc zero)
         ∙∙ cong (-ₕ_) (cong (invEq (fst ϕ)) (sym x₁) ∙ (retEq (fst ϕ) g)))
    lem₂ (inr x) (inl x₁) =
      inr (sym (retEq (fst ϕ) h)
        ∙∙ cong (invEq (fst ϕ)) x
        ∙∙ (IsGroupHom.presinv (snd (invGroupEquiv ϕ)) 1
          ∙ cong (-ₕ_) (cong (invEq (fst ϕ)) (sym x₁) ∙ (retEq (fst ϕ) g))))
    lem₂ (inr x) (inr x₁) =
      inl (sym (retEq (fst ϕ) h)
        ∙∙ cong (invEq (fst ϕ)) (x ∙ sym x₁)
        ∙∙ retEq (fst ϕ) g)

    -ₕeq : ∀ {ℓ} {A : Type ℓ} (n : ℕ) → Iso (coHom n A) (coHom n A)
    Iso.fun (-ₕeq n) = -ₕ_
    Iso.inv (-ₕeq n) = -ₕ_
    Iso.rightInv (-ₕeq n) =
      sElim (λ _ → isOfHLevelPath 2 squash₂ _ _)
        λ f → cong ∣_∣₂ (funExt λ x → -ₖ^2 (f x))
    Iso.leftInv (-ₕeq n) =
      sElim (λ _ → isOfHLevelPath 2 squash₂ _ _)
        λ f → cong ∣_∣₂ (funExt λ x → -ₖ^2 (f x))

    theEq : coHom 2 G ≃ coHom 4 G
    theEq = compEquiv (_ , ⌣eq) (isoToEquiv (-ₕeq 4))

    lem₃ : (h ≡ g) ⊎ (h ≡ (-ₕ g)) → isEquiv {A = coHom 2 G} (_⌣ h)
    lem₃ (inl x) = subst isEquiv (λ i → _⌣ (x (~ i))) ⌣eq
    lem₃ (inr x) =
      subst isEquiv (funExt (λ x → -ₕDistᵣ 2 2 x g) ∙ (λ i → _⌣ (x (~ i))))
            (theEq .snd)

    main : GroupEquiv (coHomGr 2 G) (coHomGr 4 G)
    fst main = _ ,
      (lem₃ (lem₂ (abs→⊎ _ _ (lem₁ (abs→⊎ _ _ idh))) (abs→⊎ _ _ idg)))
    snd main =
      makeIsGroupHom λ g1 g2 → rightDistr-⌣ _ _ g1 g2 h

-- The hopf invariant is ±1 for both definitions of the hopf map
HopfInvariant-HopfMap' :
  abs (HopfInvariant zero (HopfMap' , λ _ → HopfMap' (snd (S₊∙ 3)))) ≡ 1
HopfInvariant-HopfMap' =
  cong abs (cong (Iso.fun (fst (Hopfβ-Iso zero (HopfMap' , refl))))
           (transportRefl (⌣-α 0 (HopfMap' , refl))))
            ∙ ⌣equiv→pres1 (sym CP2≡CP²')
                GysinS².e (Hopfα zero (HopfMap' , refl))
           (l isGenerator≃ℤ-e)
           (GroupIso→GroupEquiv (Hopfα-Iso 0 (HopfMap' , refl)) , refl)
           (snd (fst ⌣Equiv))
           (GroupIso→GroupEquiv (Hopfβ-Iso zero (HopfMap' , refl)))
  where
  l : Σ[ ϕ ∈ GroupIso (coHomGr 2 CP²) ℤGroup ]
       (abs (Iso.fun (fst ϕ) GysinS².e) ≡ 1)
      → Σ[ ϕ ∈ GroupEquiv (coHomGr 2 CP²) ℤGroup ]
          (abs (fst (fst ϕ) GysinS².e) ≡ 1)
  l p = (GroupIso→GroupEquiv (fst p)) , (snd p)

HopfInvariant-HopfMap : abs (HopfInvariant zero HopfMap) ≡ 1
HopfInvariant-HopfMap = cong abs (cong (HopfInvariant zero) hopfMap≡HopfMap')
                      ∙ HopfInvariant-HopfMap'

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

module Categories.Category.Lift where

open import Level
open import Categories.Category

liftC : ∀ {o ℓ e} o′ ℓ′ e′ → Category o ℓ e → Category (o ⊔ o′) (ℓ ⊔ ℓ′) (e ⊔ e′)
liftC o′ ℓ′ e′ C = record
  { Obj       = Lift o′ Obj
  ; _⇒_       = λ X Y → Lift ℓ′ (lower X ⇒ lower Y)
  ; _≈_       = λ f g → Lift e′ (lower f ≈ lower g)
  ; id        = lift id
  ; _∘_       = λ f g → lift (lower f ∘ lower g)
  ; assoc     = lift assoc
  ; sym-assoc = lift sym-assoc
  ; identityˡ = lift identityˡ
  ; identityʳ = lift identityʳ
  ; identity² = lift identity²
  ; equiv     = record
    { refl  = lift Equiv.refl
    ; sym   = λ eq → lift (Equiv.sym (lower eq))
    ; trans = λ eq eq′ → lift (Equiv.trans (lower eq) (lower eq′))
    }
  ; ∘-resp-≈  = λ eq eq′ → lift (∘-resp-≈ (lower eq) (lower eq′))
  }
  where open Category C

max_stars_repo_name: laMudri/agda-categories

max_issues_repo_name: laMudri/agda-categories

max_forks_repo_name: laMudri/agda-categories


text:
-- Andreas, 2012-03-13
module Issue585t where

postulate
  A : Set
  a : A    -- just so that A is not empty and the constraints are solvable
           -- however, Agda picks the wrong solution

data B : Set where
  inn : A -> B

out : B -> A
out (inn a) = a

postulate
  P : (y : A) (z : B) → Set
  p : (x : B) → P (out x) x

mutual
  d : B
  d = inn _           -- Y

  g : P (out d) d
  g = p _             -- X

-- Agda previously solved  d = inn (out d)
--
-- out X = out d = out (inn Y) = Y
-- X = d
--
-- Now this does not pass the occurs check, so unsolved metas should remain.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
postulate
  ℤ     : Set
  n     : ℤ
  -_ _! : ℤ → ℤ

-- Note that an unrelated prefix/postfix operator can be combined with
-- itself:

ok : ℤ
ok = n ! ! ! !

also-ok : ℤ
also-ok = - - - - - - - n


text:
open import Prelude

module Implicits.Resolution.Infinite.Resolution where

open import Coinduction
open import Data.Fin.Substitution
open import Data.List
open import Data.List.Any.Membership using (map-mono)
open import Data.List.Any
open Membership-≡

open import Implicits.Syntax
open import Implicits.Substitutions

module Coinductive where
  infixl 5 _⊢ᵣ_ _⊢_↓_

  mutual
    data _⊢_↓_ {ν} (Δ : ICtx ν) : Type ν → SimpleType ν → Set where
      i-simp : ∀ a → Δ ⊢ simpl a ↓ a
      i-iabs : ∀ {ρ₁ ρ₂ a} → ∞ (Δ ⊢ᵣ ρ₁) → Δ ⊢ ρ₂ ↓ a → Δ ⊢ ρ₁ ⇒ ρ₂ ↓ a
      i-tabs : ∀ {ρ a} b → Δ ⊢ ρ tp[/tp b ] ↓ a → Δ ⊢ ∀' ρ ↓ a

    data _⊢ᵣ_ {ν} (Δ : ICtx ν) : Type ν → Set where
      r-simp : ∀ {r τ} → (r ∈ Δ) → Δ ⊢ r ↓ τ → Δ ⊢ᵣ simpl τ
      r-iabs : ∀ {ρ₁ ρ₂} → ((ρ₁ ∷ Δ) ⊢ᵣ ρ₂) → Δ ⊢ᵣ (ρ₁ ⇒ ρ₂)
      r-tabs : ∀ {ρ} → (ictx-weaken Δ ⊢ᵣ ρ) → Δ ⊢ᵣ ∀' ρ

  mutual
    -- extending contexts is safe: it preserves the r ↓ a relation
    -- (this is not true for Oliveira's deterministic calculus)
    ⊆-r↓a : ∀ {ν} {Δ Δ' : ICtx ν} {a r} → Δ ⊢ r ↓ a → Δ ⊆ Δ' → Δ' ⊢ r ↓ a
    ⊆-r↓a (i-simp a) _ = i-simp a
    ⊆-r↓a (i-iabs x₁ x₂) f = i-iabs (♯ (⊆-Δ⊢a (♭ x₁) f)) (⊆-r↓a x₂ f)
    ⊆-r↓a (i-tabs b x₁) f = i-tabs b (⊆-r↓a x₁ f)

    -- extending contexts is safe: it preserves the ⊢ᵣ a relation
    -- (this is not true for Oliveira's deterministic calculus)
    ⊆-Δ⊢a : ∀ {ν} {Δ Δ' : ICtx ν} {a} → Δ ⊢ᵣ a → Δ ⊆ Δ' → Δ' ⊢ᵣ a
    ⊆-Δ⊢a (r-simp x₁ x₂) f = r-simp (f x₁) (⊆-r↓a x₂ f)
    ⊆-Δ⊢a (r-iabs x₁) f =
      r-iabs (⊆-Δ⊢a x₁ (λ{ (here px) → here px ; (there x₂) → there (f x₂) }))
    ⊆-Δ⊢a (r-tabs x) f = r-tabs (⊆-Δ⊢a x f')
      where
        f' = map-mono (flip TypeSubst._/_ TypeSubst.wk) f

module Inductive where
  infixl 5 _⊢ᵣ_ _⊢_↓_

  mutual
    data _⊢_↓_ {ν} (Δ : ICtx ν) : Type ν → SimpleType ν → Set where
      i-simp : ∀ a → Δ ⊢ simpl a ↓ a
      i-iabs : ∀ {ρ₁ ρ₂ a} → (Δ ⊢ᵣ ρ₁) → Δ ⊢ ρ₂ ↓ a → Δ ⊢ ρ₁ ⇒ ρ₂ ↓ a
      i-tabs : ∀ {ρ a} b → Δ ⊢ ρ tp[/tp b ] ↓ a → Δ ⊢ ∀' ρ ↓ a

    data _⊢ᵣ_ {ν} (Δ : ICtx ν) : Type ν → Set where
      r-simp : ∀ {r τ} → (r ∈ Δ) → Δ ⊢ r ↓ τ → Δ ⊢ᵣ simpl τ
      r-iabs : ∀ {ρ₁ ρ₂} → ((ρ₁ ∷ Δ) ⊢ᵣ ρ₂) → Δ ⊢ᵣ (ρ₁ ⇒ ρ₂)
      r-tabs : ∀ {ρ} → (ictx-weaken Δ ⊢ᵣ ρ) → Δ ⊢ᵣ ∀' ρ

  mutual -- extending contexts is safe: it preserves the r ↓ a relation
    -- (this is not true for Oliveira's deterministic calculus)
    ⊆-r↓a : ∀ {ν} {Δ Δ' : ICtx ν} {a r} → Δ ⊢ r ↓ a → Δ ⊆ Δ' → Δ' ⊢ r ↓ a
    ⊆-r↓a (i-simp a) _ = i-simp a
    ⊆-r↓a (i-iabs x₁ x₂) f = i-iabs (⊆-Δ⊢a x₁ f) (⊆-r↓a x₂ f)
    ⊆-r↓a (i-tabs b x₁) f = i-tabs b (⊆-r↓a x₁ f)

    -- extending contexts is safe: it preserves the ⊢ᵣ a relation
    -- (this is not true for Oliveira's deterministic calculus)
    ⊆-Δ⊢a : ∀ {ν} {Δ Δ' : ICtx ν} {a} → Δ ⊢ᵣ a → Δ ⊆ Δ' → Δ' ⊢ᵣ a
    ⊆-Δ⊢a (r-simp x₁ x₂) f = r-simp (f x₁) (⊆-r↓a x₂ f)
    ⊆-Δ⊢a (r-iabs x₁) f =
      r-iabs (⊆-Δ⊢a x₁ (λ{ (here px) → here px ; (there x₂) → there (f x₂) }))
    ⊆-Δ⊢a (r-tabs x) f = r-tabs (⊆-Δ⊢a x f')
      where
        f' = map-mono (flip TypeSubst._/_ TypeSubst.wk) f

open Inductive public


text:
{-# OPTIONS --safe #-}
module Cubical.Data.NatMinusOne where

open import Cubical.Data.NatMinusOne.Base public
open import Cubical.Data.NatMinusOne.Properties public


text:
module Lang.Irrelevance where

open import Type

postulate .axiom : ∀{ℓ}{T : Type{ℓ}} -> .T -> T

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:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Library.Data.Both where

open import Light.Level using (Level ; Setω)
open import Light.Variable.Sets
open import Light.Variable.Levels
open import Light.Library.Relation.Binary
      using (SelfTransitive ; SelfSymmetric ; Reflexive)
open import Light.Library.Relation.Binary.Equality.Decidable using (DecidableEquality ; DecidableSelfEquality)

record Dependencies : Setω where

record Library (dependencies : Dependencies) : Setω where
      field
            ℓf : Level → Level → Level
            Both : Set aℓ → Set bℓ → Set (ℓf aℓ bℓ)
            both : 𝕒 → 𝕓 → Both 𝕒 𝕓
            first : Both 𝕒 𝕓 → 𝕒
            second : Both 𝕒 𝕓 → 𝕓
            ⦃ equals ⦄ :
                  ∀ ⦃ a‐c‐equals : DecidableEquality 𝕒 𝕔 ⦄ ⦃ b‐d‐equals : DecidableEquality 𝕓 𝕕 ⦄
                  → DecidableEquality (Both 𝕒 𝕓) (Both 𝕔 𝕕)

open Library ⦃ ... ⦄ public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
module Cats.Category.Fun where

open import Cats.Trans public using (Trans ; component ; natural ; id ; _∘_)

open import Relation.Binary using (Rel ; IsEquivalence ; _Preserves₂_⟶_⟶_)
open import Level

open import Cats.Category
open import Cats.Functor using (Functor)

module _ {lo la l≈ lo′ la′ l≈′}
  (C : Category lo la l≈)
  (D : Category lo′ la′ l≈′)
  where

  infixr 4 _≈_

  private
    module C = Category C
    module D = Category D
    open D.≈
    open D.≈-Reasoning

  Obj : Set (lo ⊔ la ⊔ l≈ ⊔ lo′ ⊔ la′ ⊔ l≈′)
  Obj = Functor C D

  _⇒_ : Obj → Obj → Set (lo ⊔ la ⊔ la′ ⊔ l≈′)
  _⇒_ = Trans

  record _≈_ {F G} (θ ι : F ⇒ G) : Set (lo ⊔ l≈′) where
    constructor ≈-intro
    field
      ≈-elim : ∀ {c} → component θ c D.≈ component ι c

  open _≈_ public

  equiv : ∀ {F G} → IsEquivalence (_≈_ {F} {G})
  equiv = record
      { refl = ≈-intro refl
      ; sym = λ eq → ≈-intro (sym (≈-elim eq))
      ; trans = λ eq₁ eq₂ → ≈-intro (trans (≈-elim eq₁) (≈-elim eq₂))
      }

  Fun : Category (lo ⊔ la ⊔ l≈ ⊔ lo′ ⊔ la′ ⊔ l≈′) (lo ⊔ la ⊔ la′ ⊔ l≈′) (lo ⊔ l≈′)
  Fun = record
      { Obj = Obj
      ; _⇒_ = _⇒_
      ; _≈_ = _≈_
      ; id = id
      ; _∘_ = _∘_
      ; equiv = equiv
      ; ∘-resp = λ θ≈θ′ ι≈ι′ → ≈-intro (D.∘-resp (≈-elim θ≈θ′) (≈-elim ι≈ι′))
      ; id-r = ≈-intro D.id-r
      ; id-l = ≈-intro D.id-l
      ; assoc = ≈-intro D.assoc
      }

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
{-

Theory about isomorphisms

- Definitions of [section] and [retract]
- Definition of isomorphisms ([Iso])
- Any isomorphism is an equivalence ([isoToEquiv])

-}
{-# OPTIONS --safe #-}
module Cubical.Foundations.Isomorphism where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv.Base

private
  variable
    ℓ ℓ' : Level
    A B C : Type ℓ

-- Section and retract
module _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} where
  section : (f : A → B) → (g : B → A) → Type ℓ'
  section f g = ∀ b → f (g b) ≡ b

  -- NB: `g` is the retraction!
  retract : (f : A → B) → (g : B → A) → Type ℓ
  retract f g = ∀ a → g (f a) ≡ a

record Iso {ℓ ℓ'} (A : Type ℓ) (B : Type ℓ') : Type (ℓ-max ℓ ℓ') where
  no-eta-equality
  constructor iso
  field
    fun : A → B
    inv : B → A
    rightInv : section fun inv
    leftInv  : retract fun inv

isIso : (A → B) → Type _
isIso {A = A} {B = B} f = Σ[ g ∈ (B → A) ] Σ[ _ ∈ section f g ] retract f g

isoFunInjective : (f : Iso A B) → (x y : A) → Iso.fun f x ≡ Iso.fun f y → x ≡ y
isoFunInjective f x y h = sym (Iso.leftInv f x) ∙∙ cong (Iso.inv f) h ∙∙ Iso.leftInv f y

isoInvInjective : (f : Iso A B) → (x y : B) → Iso.inv f x ≡ Iso.inv f y → x ≡ y
isoInvInjective f x y h = sym (Iso.rightInv f x) ∙∙ cong (Iso.fun f) h ∙∙ Iso.rightInv f y

-- Any iso is an equivalence
module _ (i : Iso A B) where
  open Iso i renaming ( fun to f
                      ; inv to g
                      ; rightInv to s
                      ; leftInv to t)

  private
    module _ (y : B) (x0 x1 : A) (p0 : f x0 ≡ y) (p1 : f x1 ≡ y) where
      fill0 : I → I → A
      fill0 i = hfill (λ k → λ { (i = i1) → t x0 k
                               ; (i = i0) → g y })
                      (inS (g (p0 (~ i))))

      fill1 : I → I → A
      fill1 i = hfill (λ k → λ { (i = i1) → t x1 k
                               ; (i = i0) → g y })
                      (inS (g (p1 (~ i))))

      fill2 : I → I → A
      fill2 i = hfill (λ k → λ { (i = i1) → fill1 k i1
                               ; (i = i0) → fill0 k i1 })
                      (inS (g y))

      p : x0 ≡ x1
      p i = fill2 i i1

      sq : I → I → A
      sq i j = hcomp (λ k → λ { (i = i1) → fill1 j (~ k)
                              ; (i = i0) → fill0 j (~ k)
                              ; (j = i1) → t (fill2 i i1) (~ k)
                              ; (j = i0) → g y })
                     (fill2 i j)

      sq1 : I → I → B
      sq1 i j = hcomp (λ k → λ { (i = i1) → s (p1 (~ j)) k
                               ; (i = i0) → s (p0 (~ j)) k
                               ; (j = i1) → s (f (p i)) k
                               ; (j = i0) → s y k })
                      (f (sq i j))

      lemIso : (x0 , p0) ≡ (x1 , p1)
      lemIso i .fst = p i
      lemIso i .snd = λ j → sq1 i (~ j)

  isoToIsEquiv : isEquiv f
  isoToIsEquiv .equiv-proof y .fst .fst = g y
  isoToIsEquiv .equiv-proof y .fst .snd = s y
  isoToIsEquiv .equiv-proof y .snd z = lemIso y (g y) (fst z) (s y) (snd z)

isoToEquiv : Iso A B → A ≃ B
isoToEquiv i .fst = i .Iso.fun
isoToEquiv i .snd = isoToIsEquiv i

isoToPath : Iso A B → A ≡ B
isoToPath {A = A} {B = B} f i =
  Glue B (λ { (i = i0) → (A , isoToEquiv f)
            ; (i = i1) → (B , idEquiv B) })

open Iso

invIso : Iso A B → Iso B A
fun (invIso f) = inv f
inv (invIso f) = fun f
rightInv (invIso f) = leftInv f
leftInv (invIso f)  = rightInv f

compIso : Iso A B → Iso B C → Iso A C
fun (compIso i j)       = fun j ∘ fun i
inv (compIso i j) = inv i ∘ inv j
rightInv (compIso i j) b = cong (fun j) (rightInv i (inv j b)) ∙ rightInv j b
leftInv (compIso i j) a = cong (inv i) (leftInv j (fun i a)) ∙ leftInv i a

composesToId→Iso : (G : Iso A B) (g : B → A) → G .fun ∘ g ≡ idfun B → Iso B A
fun (composesToId→Iso _ g _)             = g
inv (composesToId→Iso j _ _) = fun j
rightInv (composesToId→Iso i g path) b =
  sym (leftInv i (g (fun i b))) ∙∙ cong (λ g → inv i (g (fun i b))) path ∙∙ leftInv i b
leftInv (composesToId→Iso _ _ path) b i = path i b

idIso : Iso A A
fun idIso = idfun _
inv idIso = idfun _
rightInv idIso _ = refl
leftInv idIso _  = refl

LiftIso : Iso A (Lift {i = ℓ} {j = ℓ'} A)
fun LiftIso = lift
inv LiftIso = lower
rightInv LiftIso _ = refl
leftInv LiftIso _  = refl

isContr→Iso : isContr A → isContr B → Iso A B
fun (isContr→Iso _ Bctr) _ = Bctr .fst
inv (isContr→Iso Actr _) _ = Actr .fst
rightInv (isContr→Iso _ Bctr) = Bctr .snd
leftInv (isContr→Iso Actr _)  = Actr .snd

isProp→Iso :  (Aprop : isProp A) (Bprop : isProp B) (f : A → B) (g : B → A) → Iso A B
fun (isProp→Iso _ _ f _) = f
inv (isProp→Iso _ _ _ g) = g
rightInv (isProp→Iso _ Bprop f g) b = Bprop (f (g b)) b
leftInv (isProp→Iso Aprop _ f g) a  = Aprop (g (f a)) a

domIso : ∀ {ℓ} {C : Type ℓ} → Iso A B → Iso (A → C) (B → C)
fun (domIso e) f b = f (inv e b)
inv (domIso e) f a = f (fun e a)
rightInv (domIso e) f i x = f (rightInv e x i)
leftInv (domIso e) f i x = f (leftInv e x i)

-- Helpful notation
_Iso⟨_⟩_ : ∀ {ℓ ℓ' ℓ''} {B : Type ℓ'} {C : Type ℓ''} (X : Type ℓ) → Iso X B → Iso B C → Iso X C
_ Iso⟨ f ⟩ g = compIso f g

_∎Iso : ∀ {ℓ} (A : Type ℓ) → Iso A A
A ∎Iso = idIso {A = A}

infixr  0 _Iso⟨_⟩_
infix   1 _∎Iso

codomainIsoDep : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {C : A → Type ℓ''}
                 → ((a : A) → Iso (B a) (C a))
                 → Iso ((a : A) → B a) ((a : A) → C a)
fun (codomainIsoDep is) f a = fun (is a) (f a)
inv (codomainIsoDep is) f a = inv (is a) (f a)
rightInv (codomainIsoDep is) f = funExt λ a → rightInv (is a) (f a)
leftInv (codomainIsoDep is) f = funExt λ a → leftInv (is a) (f a)

codomainIso : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
           → Iso B C
           → Iso (A → B) (A → C)
codomainIso z = codomainIsoDep λ _ → z

Iso≡Set : isSet A → isSet B → (f g : Iso A B)
        → ((x : A) → f .fun x ≡ g .fun x)
        → ((x : B) → f .inv x ≡ g .inv x)
        → f ≡ g
fun (Iso≡Set hA hB f g hfun hinv i) x = hfun x i
inv (Iso≡Set hA hB f g hfun hinv i) x = hinv x i
rightInv (Iso≡Set hA hB f g hfun hinv i) x j =
  isSet→isSet' hB (rightInv f x) (rightInv g x) (λ i → hfun (hinv x i) i) refl i j
leftInv (Iso≡Set hA hB f g hfun hinv i) x j =
  isSet→isSet' hA (leftInv f x) (leftInv g x) (λ i → hinv (hfun x i) i) refl i j

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
{-# OPTIONS --sized-types #-}
open import Relation.Binary.Core

module SelectSort.Correctness.Order  {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_)  where

open import Data.List
open import Data.Product
open import Data.Sum
open import Function using (_∘_)
open import List.Sorted _≤_
open import Order.Total _≤_ tot≤
open import Size
open import SList
open import SList.Order _≤_
open import SList.Order.Properties _≤_
open import SelectSort _≤_ tot≤

lemma-select-≤ : {ι : Size}(x : A) → (xs : SList A {ι}) → proj₁ (select x xs) ≤ x
lemma-select-≤ x snil = refl≤
lemma-select-≤ x (y ∙ ys)
    with tot≤ x y
... | inj₁ x≤y = lemma-select-≤ x ys
... | inj₂ y≤x = trans≤ (lemma-select-≤ y ys) y≤x

lemma-select-*≤ : {ι : Size}(x : A) → (xs : SList A {ι}) → proj₁ (select x xs) *≤ proj₂ (select x xs)
lemma-select-*≤ x snil = genx
lemma-select-*≤ x (y ∙ ys)
    with tot≤ x y
... | inj₁ x≤y = gecx (trans≤ (lemma-select-≤ x ys) x≤y) (lemma-select-*≤ x ys)
... | inj₂ y≤x = gecx (trans≤ (lemma-select-≤ y ys) y≤x) (lemma-select-*≤ y ys)

lemma-select-≤-*≤ : {ι : Size}{b x : A}{xs : SList A {ι}} → b ≤ x → b *≤ xs → b ≤ proj₁ (select x xs) × b *≤ proj₂ (select x xs)
lemma-select-≤-*≤ b≤x genx = b≤x , genx
lemma-select-≤-*≤ {x = x} b≤x (gecx {x = y} b≤y b*≤ys)
    with tot≤ x y
... | inj₁ x≤y = proj₁ (lemma-select-≤-*≤ b≤x b*≤ys) , gecx (trans≤ b≤x x≤y) (proj₂ (lemma-select-≤-*≤ b≤x b*≤ys))
... | inj₂ y≤x = proj₁ (lemma-select-≤-*≤ b≤y b*≤ys) , gecx (trans≤ b≤y y≤x) (proj₂ (lemma-select-≤-*≤ b≤y b*≤ys))

lemma-selectSort-*≤ : {ι : Size}{x : A}{xs : SList A {ι}} → x *≤ xs → x *≤ selectSort xs
lemma-selectSort-*≤ genx = genx
lemma-selectSort-*≤ (gecx x≤y x*≤ys)
    with lemma-select-≤-*≤ x≤y x*≤ys
... | (x≤z , x*≤zs) = gecx x≤z (lemma-selectSort-*≤ x*≤zs)

lemma-selectSort-sorted : {ι : Size}(xs : SList A {ι}) → Sorted (unsize A (selectSort xs))
lemma-selectSort-sorted snil = nils
lemma-selectSort-sorted (x ∙ xs) = lemma-slist-sorted (lemma-selectSort-*≤ (lemma-select-*≤ x xs)) (lemma-selectSort-sorted (proj₂ (select x xs)))

theorem-selectSort-sorted : (xs : List A) → Sorted (unsize A (selectSort (size A xs)))
theorem-selectSort-sorted = lemma-selectSort-sorted ∘ (size A)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
------------------------------------------------------------------------------
-- tptp4X yields an error because a duplicate formula
------------------------------------------------------------------------------

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

postulate
  D          : Set
  true false : D
  _≡_        : D → D → Set

data Bool : D → Set where
  btrue  : Bool true
  bfalse : Bool false
{-# ATP axioms btrue false #-}

postulate foo : ∀ d → d ≡ d
{-# ATP prove foo btrue #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-# OPTIONS --universe-polymorphism #-}

-- Check that unification can handle levels
module LevelUnification where

open import Common.Level

data _≡_ {a}{A : Set a}(x : A) : ∀ {b}{B : Set b} → B → Set where
  refl : x ≡ x

sym₁ : ∀ a b (A : Set a)(B : Set b)(x : A)(y : B) → x ≡ y → y ≡ x
sym₁ a .a A .A x .x refl = refl

sym₂ : ∀ a b (A : Set (lsuc a))(B : Set b)(x : A)(y : B) → x ≡ y → y ≡ x
sym₂ a .(lsuc a) A .A x .x refl = refl

homogenous : ∀ a (A : Set a)(x y : A) → x ≡ y → Set₁
homogenous a A x .x refl = Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --type-in-type #-} -- DANGER!
postulate HOLE : {A : Set} -> A -- MORE DANGER!

infixr 6 _\\ _/quad/
infixr 6 _\\&\indent
infixl 2 &_

infixr 3 [_
infixr 5 _,_
infixr 7 _]

infixr 5 _/xor/_ _/land/_ _/lor/_ _+_ _/ll/_ _/gg/_
infixr 5 /Sigma/ /Sigmap/ /Pi/ /Pip/ lambda tlambda
infixr 2 id
infixl 1 WHEN
infixl 1 AND

-- Definitions used in the main body

data ⊥ : Set where

record ⊤ : Set where
  constructor /epsilon/

record Π (A : Set) (B : A -> Set) : Set where
  constructor _,_
  field fst : A
  field snd : B(fst)

syntax Π A (\x -> B) = Π x ∈ A ∙ B

_×_ : Set → Set → Set
(A × B) = Π x ∈ A ∙ B

data 𝔹 : Set where
  /false/ : 𝔹
  /true/ : 𝔹

if_then_else_ : ∀ {A : 𝔹 -> Set} -> (b : 𝔹) -> A(/true/) -> A(/false/) -> A(b)
if /false/ then T else F = F
if /true/ then T else F = T

⟨_⟩ : 𝔹 → Set
⟨ /false/ ⟩ = ⊥
⟨ /true/ ⟩ = ⊤

data ℕ : Set where
  zero : ℕ
  succ : ℕ -> ℕ

one = succ zero
two = succ one
three = succ two
four = succ three

_+n_ : ℕ → ℕ → ℕ
zero +n k = k
(succ j) +n k = succ(j +n k)

_⊔_ : ℕ → ℕ → ℕ
zero ⊔ n = n
succ m ⊔ zero = succ m
succ m ⊔ succ n = succ (m ⊔ n)

_↑_ : Set → ℕ → Set
(A ↑ zero) = ⊤
(A ↑ (succ n)) = (A × (A ↑ n))

len : ∀ {k} → (𝔹 ↑ k) → ℕ
len {k} n = k

/IF/_/THEN/_/ELSE/_ : forall {A : 𝔹 -> Set} -> (b : 𝔹) -> A(/true/) -> A(/false/) -> A(b)
/IF/ /false/ /THEN/ T /ELSE/ F = F
/IF/ /true/ /THEN/ T /ELSE/ F = T

-- Binary arithmetic

indn : ∀ {k} {A : Set} → A → (A → A) → (𝔹 ↑ k) → A
indn {zero}   e f n = e
indn {succ k} e f (/false/ , n) = indn e (λ x → f (f x)) n
indn {succ k} e f (/true/ , n) = f (indn e (λ x → f (f x)) n)

unary : ∀ {k} → (𝔹 ↑ k) → ℕ
unary = indn zero succ

/zerop/ : ∀ {k} → (𝔹 ↑ k)
/zerop/ {zero}   = /epsilon/
/zerop/ {succ n} = (/false/ , /zerop/)

/epsilon/[_] :  ∀ {k} → (n : 𝔹 ↑ k) → (𝔹 ↑ unary n)
/epsilon/[ n ] = /zerop/

/onep/ : ∀ {k} → (𝔹 ↑ succ k)
/onep/ = (/true/ , /zerop/)

/one/ : (𝔹 ↑ one)
/one/ = /onep/

/max/ : ∀ {k} → (𝔹 ↑ k)
/max/ {zero}   = /epsilon/
/max/ {succ n} = (/true/ , /max/)

/IMPOSSIBLE/ : {A : Set} → {{p : ⊥}} → A
/IMPOSSIBLE/ {A} {{()}}

/not/ : 𝔹 → 𝔹
/not/ /false/ = /true/
/not/ /true/ = /false/

/extend/ : ∀ {k} → (𝔹 ↑ k) → (𝔹 ↑ succ k)
/extend/ {zero}   _       = (/false/ , /epsilon/)
/extend/ {succ k} (b , n) = (b , /extend/ n)

/succp/ :  ∀ {k} → (𝔹 ↑ k) → (𝔹 ↑ succ k)
/succp/ {zero} n = (/false/ , /epsilon/)
/succp/ {succ k} (/false/ , n) = (/true/ , /extend/ n)
/succp/ {succ k} (/true/ , n) = (/false/ , /succp/ n)

_/land/_ : 𝔹 → 𝔹 → 𝔹
(/false/ /land/ b) = /false/
(/true/ /land/ b) = b

_/lor/_ : 𝔹 → 𝔹 → 𝔹
(/false/ /lor/ b) = b
(/true/ /lor/ b) = /true/

/neg/ : 𝔹 → 𝔹
/neg/ /false/ = /true/
/neg/ /true/ = /false/

_/xor/_ : 𝔹 → 𝔹 → 𝔹
(/false/ /xor/ b) = b
(/true/ /xor/ /false/) = /true/
(/true/ /xor/ /true/) = /false/

/carry/ : 𝔹 → 𝔹 → 𝔹 → 𝔹
/carry/ /false/ a b = a /land/ b
/carry/ /true/ a b = a /lor/ b

addclen : ∀ {j k} → 𝔹 → (𝔹 ↑ j) → (𝔹 ↑ k) → ℕ
addclen {zero} {k}      /false/ m n = k
addclen {zero} {zero} /true/ m n = one
addclen {zero} {succ k} /true/ m (b , n) = succ (addclen b m n)
addclen {succ j} {zero}   /false/ m n = succ j
addclen {succ j} {zero}   /true/ (a , m) n = succ (addclen a m n)
addclen {succ j} {succ k} c   (a , m) (b , n) = succ (addclen (/carry/ c a b) m n)

addlen : ∀ {j k} → (𝔹 ↑ j) → (𝔹 ↑ k) → ℕ
addlen = addclen /false/

/addc/ : ∀ {j k} c → (m : 𝔹 ↑ j) → (n : 𝔹 ↑ k) → (𝔹 ↑ addclen c m n)
/addc/ {zero}   {k}      /false/ m n = n
/addc/ {zero} {zero} /true/ m n = /one/
/addc/ {zero} {succ k} /true/ m (b , n) = (/not/ b , /addc/ b m n)
/addc/ {succ j} {zero}   /false/ (a , m) n = (a , m)
/addc/ {succ j} {zero}   /true/ (a , m) n = (/not/ a , /addc/ a m n)
/addc/ {succ j} {succ k} c (a , m) (b , n) = ((c /xor/ a /xor/ b) , (/addc/ (/carry/ c a b) m n))

_+_ : ∀ {j k} → (m : 𝔹 ↑ j) → (n : 𝔹 ↑ k) → (𝔹 ↑ addlen m n)
_+_ = /addc/ /false/

/succ/ : ∀ {k} → (n : 𝔹 ↑ k) → (𝔹 ↑ addclen /true/ /epsilon/ n)
/succ/ = /addc/ /true/ /epsilon/

dindn : (A : ∀ {k} → (𝔹 ↑ k) → Set) → (∀ {k} → A(/zerop/ {k})) → (∀ {k} (n : 𝔹 ↑ k) → A(n) → A(/succ/(n))) → ∀ {k} → (n : 𝔹 ↑ k) → A(n)
dindn A e f {zero} n = e
dindn A e f {succ k} (/false/ , n) = dindn (λ {j} m → A (/false/ , m)) e (λ {j} m x → f (/true/ , m) (f (/false/ , m) x)) n
dindn A e f {succ k} (/true/ , n) = f (/false/ , n) (dindn (λ {j} m → A (/false/ , m)) e (λ {j} m x → f (/true/ , m) (f (/false/ , m) x)) n)

_++_ : ∀ {A j k} → (A ↑ j) → (A ↑ k) → (A ↑ (j +n k))
_++_ {A} {zero}   xs       ys = ys
_++_ {A} {succ j} (x , xs) ys = (x , xs ++ ys)

_/ll/_ : ∀ {j k} → (𝔹 ↑ j) → (n : 𝔹 ↑ k) → (𝔹 ↑ (unary n +n j))
(m /ll/ n) = (/zerop/ {unary n} ++ m)

_-n_ : ℕ → ℕ → ℕ
(m -n zero) = m
(zero -n n) = zero
(succ m -n succ n) = (m -n n)

drop : ∀ {A j} (k : ℕ) → (A ↑ j) → (A ↑ (j -n k))
drop zero xs = xs
drop {A} {zero} (succ k) xs = /epsilon/
drop {A} {succ j} (succ k) (x , xs) = drop k xs

_/gg/_ : ∀ {j k} → (𝔹 ↑ j) → (n : 𝔹 ↑ k) → (𝔹 ↑ (j -n unary n))
m /gg/ n = drop (unary n) m

/truncate/ : ∀ {j k} → (𝔹 ↑ j) → (𝔹 ↑ k)
/truncate/ {j} {zero} n = /epsilon/
/truncate/ {zero} {succ k} n = /zerop/
/truncate/ {succ j} {succ k} (a , n) = (a , /truncate/ n)

-- Finite sets

EncodableIn : ∀ {k} → Set → (𝔹 ↑ k) → Set
EncodableIn = HOLE

record FSet {k} (n : 𝔹 ↑ k) : Set where
  field Carrier : Set
  field .encodable : EncodableIn Carrier n
open FSet public

/sizeof/ : ∀ {k} → {n : 𝔹 ↑ k} → FSet(n) → (𝔹 ↑ k)
/sizeof/ {k} {n} A = n

data _≡_ {A : Set} (x : A) : A → Set where
  refl : (x ≡ x)

data ℂ : Set where
  less : ℂ
  eq : ℂ
  gtr : ℂ

isless : ℂ → Set
isless less = ⊤
isless _ = ⊥

isleq : ℂ → Set
isleq gtr = ⊥
isleq _ = ⊤

cmpb : 𝔹 → 𝔹 → ℂ
cmpb /false/ /false/ = eq
cmpb /false/ /true/ = less
cmpb /true/ /false/ = gtr
cmpb /true/ /true/ = eq

cmpcb : 𝔹 → 𝔹 → ℂ → ℂ
cmpcb /false/ /false/ c = c
cmpcb /false/ /true/ c = less
cmpcb /true/ /false/ c = gtr
cmpcb /true/ /true/ c = c

cmpc : ∀ {j k} → (𝔹 ↑ j) → (𝔹 ↑ k) → ℂ → ℂ
cmpc {zero} {zero} m n c = c
cmpc {zero} {succ k} m (b , n) c = cmpc m n (cmpcb /false/ b c)
cmpc {succ j} {zero} (a , m) n c = cmpc m n (cmpcb a /false/ c)
cmpc {succ j} {succ k} (a , m) (b , n) c = cmpc m n (cmpcb a b c)

cmp : ∀ {j k} → (𝔹 ↑ j) → (𝔹 ↑ k) → ℂ
cmp m n = cmpc m n eq

_<_ : ∀ {j k} → (𝔹 ↑ j) → (𝔹 ↑ k) → Set
(m < n) = isless (cmp m n)

_≤_ : ∀ {j k} → (𝔹 ↑ j) → (𝔹 ↑ k) → Set
(m ≤ n) with cmp m n
(m ≤ n) | gtr = ⊥
(m ≤ n) | _ = ⊤

borrow : 𝔹 → 𝔹 → 𝔹 → 𝔹
borrow /false/ /false/ c = c
borrow /false/ /true/ c = /true/
borrow /true/ /false/ c = /false/
borrow /true/ /true/ c = c

subc : ∀ {j k} → (m : 𝔹 ↑ j) → (n : 𝔹 ↑ k) → 𝔹 → (𝔹 ↑ j)
subc {zero} m n c = /epsilon/
subc {succ j} {zero} (a , m) n c = ((a /xor/ c) , (subc m n (borrow a /false/ c)))
subc {succ j} {succ k} (a , m) (b , n) c = ((a /xor/ b /xor/ c) , (subc m n (borrow a b c)))

_∸_ : ∀ {j k} → (m : 𝔹 ↑ j) → (n : 𝔹 ↑ k) → (𝔹 ↑ j)
(m ∸ n) = subc m n /false/

/FSetp/ : ∀ {j k} {m : 𝔹 ↑ j} -> (n : 𝔹 ↑ k) -> {p : n < m} -> FSet(m)
/FSetp/ n = record { Carrier = FSet(n); encodable = HOLE }

/FSet/ : ∀ {k} -> (n : 𝔹 ↑ k) -> FSet(/succp/ n)
/FSet/ n = record { Carrier = FSet(n); encodable = HOLE }

/nothingp/ : ∀ {k} {n : 𝔹 ↑ k} → FSet(n)
/nothingp/ = record { Carrier = ⊥; encodable = HOLE }

/nothing/ : FSet(/epsilon/)
/nothing/ = /nothingp/

/boolp/ : ∀ {k} {n : 𝔹 ↑ k} {p : /epsilon/ < n} → FSet(n)
/boolp/ = record { Carrier = 𝔹; encodable = HOLE }

/bool/ : FSet(/one/)
/bool/ = /boolp/

/unitp/ : ∀ {k} {n : 𝔹 ↑ k} → FSet(n)
/unitp/ = record { Carrier = ⊤; encodable = HOLE }

/unit/ : FSet(/epsilon/)
/unit/ = /unitp/

/bitsp/ : ∀ {j k} {m : 𝔹 ↑ j} → (n : 𝔹 ↑ k) -> {p : n ≤ m} ->  FSet(m)
/bitsp/ n = record { Carrier = (𝔹 ↑ unary n); encodable = HOLE }

/bits/ : ∀ {k} (n : 𝔹 ↑ k) -> {p : n ≤ n} ->  FSet(n)
/bits/ n {p} = /bitsp/ n {p}

/Pi/ : ∀ {j k} -> {m : 𝔹 ↑ j} {n : 𝔹 ↑ k} -> (A : FSet(m)) -> (Carrier(A) → FSet(n)) -> FSet(m + n)
/Pi/ A B = record { Carrier = Π x ∈ (Carrier A) ∙ Carrier (B x) ; encodable = HOLE }

syntax /Pi/ A (λ x → B) = /prod/ x /in/ A /cdot/ B

/Pip/ : ∀ {j k} -> {m : 𝔹 ↑ j} -> {n : 𝔹 ↑ k} -> (A : FSet(m)) -> {p : m ≤ n} → (Carrier(A) → FSet(n ∸ m)) -> FSet(n)
/Pip/ A B = record { Carrier = Π x ∈ (Carrier A) ∙ Carrier (B x) ; encodable = HOLE }

syntax /Pip/ A (λ x → B) = /prodp/ x /in/ A /cdot/ B

/Sigma/ : ∀ {j k} -> {m : 𝔹 ↑ j} {n : 𝔹 ↑ k} -> (A : FSet(m)) → ((Carrier A) → FSet(n)) -> FSet(n /ll/ m)
/Sigma/ A B = record { Carrier = (x : Carrier A) → (Carrier (B x)) ; encodable = HOLE }

syntax /Sigma/ A (λ x → B) = /sum/ x /in/ A /cdot/ B

/Sigmap/ : ∀ {j k} -> {m : 𝔹 ↑ j} {n : 𝔹 ↑ k} -> (A : FSet(m)) → {p : m ≤ n} → ((Carrier A) → FSet(n /gg/ m)) -> FSet(n)
/Sigmap/ A B = record { Carrier = (x : Carrier A) → (Carrier (B x)) ; encodable = HOLE }

syntax /Sigmap/ A (λ x → B) = /sump/ x /in/ A /cdot/ B

lambda : ∀ {A : Set} {B : A → Set} → (∀ x → B(x)) → (∀ x → B(x))
lambda f = f

syntax lambda (λ x → e) = /fn/ x /cdot/ e

tlambda : ∀ {k} {n : 𝔹 ↑ k} (A : FSet(n)) {B : Carrier A → Set} → (∀ x → B(x)) → (∀ x → B(x))
tlambda A f = f

syntax tlambda A (λ x → e) = /fn/ x /in/ A /cdot/ e

/indn/ :
  {h : ∀ {k} → (𝔹 ↑ k) → ℕ} →
  {g : ∀ {k} → (n : 𝔹 ↑ k) → (𝔹 ↑ h(n))} →
  (A : ∀ {k} → (n : 𝔹 ↑ k) → FSet(g(n))) →
  (∀ {k} → Carrier(A(/zerop/ {k}))) →
  (∀ {k} (n : 𝔹 ↑ k) → Carrier(A(n)) → Carrier(A(/one/ + n))) →
  ∀ {k} → (n : 𝔹 ↑ k) → Carrier(A(n))
/indn/ A e f = dindn (λ n → Carrier(A(n))) e (λ n x → g n (f n x)) where
  g : ∀ {k} → (n : 𝔹 ↑ k) → Carrier(A(/one/ + n)) → Carrier(A(/succ/(n)))
  g {zero}   n         x = x
  g {succ k} (/false/ , n) x = x
  g {succ k} (/true/ , n) x = x

-- Stuff to help with LaTeX layout

id : ∀ {k} → {n : 𝔹 ↑ k} → (A : FSet(n)) → (Carrier A) → (Carrier A)
id A x = x

typeof : ∀ {k} → {n : 𝔹 ↑ k} → (A : FSet(n)) → (Carrier A) → Set
typeof A x = Carrier A

WHEN : ∀ {k} → {n : 𝔹 ↑ k} → (A : FSet(n)) → {B : Carrier A → Set} → (∀ x → B(x)) → (∀ x → B(x))
WHEN A F = F

AND : ∀ {k} → {n : 𝔹 ↑ k} → (A : FSet(n)) → {B : Carrier A → Set} → (∀ x → B(x)) → (∀ x → B(x))
AND A F = F

[_ : ∀ {A k} → (A ↑ k) → (A ↑ k)
[_ x = x

_] : ∀ {A} → A → (A ↑ one)
_] x = (x , /epsilon/)

_\\ : forall {A : Set} -> A -> A
x \\ = x

_/quad/ : forall {A : Set} -> A -> A
x /quad/ = x

_\\&\indent : forall {A : Set} -> A -> A
x \\&\indent = x

&_ : forall {A : Set} -> A -> A
& x = x

syntax id A x = x &/in/ A
syntax WHEN A (λ x → B) = B &/WHEN/ x /in/ A
syntax AND A (λ x → B) = B /AND/ x /in/ A

max_stars_repo_name: asajeffrey/finite-dtypes

max_issues_repo_name: asajeffrey/finite-dtypes

max_forks_repo_name: asajeffrey/finite-dtypes


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Graphs.Underlying where

open import Categories.Support.PropositionalEquality

open import Categories.Category
  hiding (module Heterogeneous)
open import Categories.Categories
open import Categories.Graphs
open import Categories.Functor
  using (Functor; module Functor; ≡⇒≣)
  renaming (id to idF; _≡_ to _≡F_)
open import Data.Product
open import Graphs.Graph
open import Graphs.GraphMorphism

Underlying₀ : ∀ {o ℓ e} → Category o ℓ e → Graph o ℓ e
Underlying₀ C = record
  { Obj   = Obj
  ; _↝_   = _⇒_
  ; _≈_   = _≡_
  ; equiv = equiv
  } where open Category C

Underlying₁ : ∀ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
  {X : Category o₁ ℓ₁ e₁}
  {Y : Category o₂ ℓ₂ e₂}
  → Functor X Y
  → GraphMorphism (Underlying₀ X) (Underlying₀ Y)
Underlying₁ G = record
  { F₀        = G₀
  ; F₁        = G₁
  ; F-resp-≈  = G-resp-≡
  }
  where
    open Functor G
      renaming (F₀ to G₀; F₁ to G₁; F-resp-≡ to G-resp-≡)

Underlying : ∀ {o ℓ e} → Functor (Categories o ℓ e) (Graphs o ℓ e)
Underlying {o}{ℓ}{e} = record
  { F₀            = Underlying₀
  ; F₁            = Underlying₁
  ; identity      = (λ x → ≣-refl) , (λ f → Heterogeneous.refl _)
  ; homomorphism  = (λ x → ≣-refl) , (λ f → Heterogeneous.refl _)
  ; F-resp-≡      = λ {A B}{F G : Functor A B} → F-resp-≡ {A}{B}{F}{G}
  }
  where
    module Graphs     = Category (Graphs     o ℓ e)
    module Categories = Category (Categories o ℓ e)

    .F-resp-≡ : ∀ {A B : Categories.Obj} {G H : Functor A B}
      → G ≡F H
      → Underlying₁ G ≈ Underlying₁ H
    F-resp-≡ {A}{B}{G}{H} G≡H
      = (≡⇒≣ G H G≡H) , (λ f → convert-~ (G≡H f))
      where
        open Heterogeneous (Underlying₀ B)
          renaming (_~_ to _~₂_)
        open Categories.Category.Heterogeneous B
          renaming (_∼_ to _~₁_)

        convert-~ : ∀ {a b c d}{x : B [ a , b ]}{y : B [ c , d ]} → x ~₁ y → x ~₂ y
        convert-~ (≡⇒∼ foo) = ≈⇒~ foo

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
import Algebra.FunctionProperties using (LeftZero; RightZero; _DistributesOverˡ_;_DistributesOverʳ_; Idempotent)
import Function using (_on_)
import Level
import Relation.Binary.EqReasoning as EqReasoning
import Relation.Binary.On using (isEquivalence)
import Algebra.Structures using (module IsCommutativeMonoid; IsCommutativeMonoid)
open import Relation.Binary    using (module IsEquivalence; IsEquivalence; _Preserves₂_⟶_⟶_ ; Setoid)
open import Data.Product renaming (_,_ to _,,_) -- just to avoid clash with other commas

open import Preliminaries using (Rel; UniqueSolution; LowerBound)

module SemiNearRingRecords where

record SemiNearRing : Set₁ where                  -- \structure{1}{|SemiNearRing|}
  field                                           -- \structure{1.1}{Carriers, operators}
     s : Set
     _≃s_  : s → s → Set
     zers  : s
     _+s_  : s → s → s
     _*s_  : s → s → s

  open Algebra.Structures                using (IsCommutativeMonoid)
  open Algebra.FunctionProperties _≃s_   using (LeftZero; RightZero)

  field                                           -- \structure{1.2}{Commutative monoid |(+,0)|}
    isCommMon : IsCommutativeMonoid _≃s_ _+s_ zers

    zeroˡ  : LeftZero   zers  _*s_   -- expands to |∀ x →  (zers *s x)  ≃s  zers|
    zeroʳ  : RightZero  zers  _*s_   -- expands to |∀ x →  (x *s zers)  ≃s  zers|
    _<*>_  : ∀ {x y u v} →  (x ≃s y)  →  (u ≃s v)  →  (x *s u   ≃s   y *s v)

  open Algebra.FunctionProperties _≃s_
    using (Idempotent; _DistributesOverˡ_; _DistributesOverʳ_)

  field                                           -- \structure{1.3}{Distributive, idempotent, \ldots}
     idem   : Idempotent _+s_

     distl  : _*s_ DistributesOverˡ _+s_
     distr  : _*s_ DistributesOverʳ _+s_
       -- expands to |∀ a b c →  (a +s b) *s c   ≃s   (a *s c) +s (b *s c)|

  infix  4 _≤s_
  _≤s_ : s -> s -> Set
  x ≤s y =  x +s y ≃s y

  infix 4 _≃s_; infixl 6 _+s_; infixl 7 _*s_

                                                  -- \structure{1.4}{Exporting commutative monoid operations}
  open Algebra.Structures.IsCommutativeMonoid isCommMon public
    hiding (refl)
    renaming
     (  isEquivalence  to isEquivs
     ;  assoc          to assocs
     ;  comm           to comms
     ;  ∙-cong         to _<+>_
     ;  identityˡ      to identityˡs
     )
  identityʳs = proj₂ identity

  sSetoid : Setoid Level.zero Level.zero          -- \structure{1.5}{Setoid, \ldots}
  sSetoid = record {  Carrier        = s;
                      _≈_            = _≃s_;
                      isEquivalence  = isEquivs }

  open IsEquivalence isEquivs public
    hiding   (reflexive) renaming (refl to refls ; sym to syms ; trans to transs)

  LowerBounds  = LowerBound  _≤s_                 -- \structure{1.6}{Lower bounds}

record SemiNearRing2 : Set₁ where                 -- \structure{2}{|SemiNearRing2|}
  field
    snr : SemiNearRing
  open SemiNearRing snr public   -- public = export the "local" names from |SemiNearRing|
  field                                           -- \structure{2.1}{Plus and times for |u|, \ldots}
     u : Set
     _+u_  : u → u → u
     _*u_  : u → u → u
     u2s   : u → s

  _≃u_ : u → u → Set
  _≃u_  = _≃s_ Function.on u2s

  _u*s_ : u → s → s
  _u*s_ u s =   u2s u  *s  s

  _s*u_ : s → u → s
  _s*u_ s u =   s  *s  u2s u

  infix   4  _≃u_;  infixl  6  _+u_;  infixl  7  _*u_ _u*s_ _s*u_

  uSetoid : Setoid Level.zero Level.zero
  uSetoid = record { isEquivalence = Relation.Binary.On.isEquivalence u2s isEquivs }

  _≤u_  : u → u → Set
  _≤u_  = _≤s_ Function.on u2s

  L : u → s → u → s → Set                         -- \structure{2.2}{Linear equation |L|}
  L a y b x =  y  +s  (a u*s x  +s  x s*u b) ≃s x

                                                  -- \structure{2.3}{Properties of |L|}
  UniqueL  = ∀ {a y b} → UniqueSolution _≃s_ (L a y b)
  CongL    = ∀ {a x b} -> ∀ {y y'} -> y ≃s y' -> L a y b x -> L a y' b x

max_stars_repo_name: DSLsofMath/ValiantAgda

max_issues_repo_name: DSLsofMath/ValiantAgda

max_forks_repo_name: DSLsofMath/ValiantAgda


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

module NewWithoutK where

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

infixl 20 _+_
_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

infixl 30 _*_
_*_ : ℕ → ℕ → ℕ
zero * n = zero
(suc m) * n = n + (m * n)

infixl 5 _⊎_
data _⊎_ (A B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

infixl 10 _≡_
data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

data _≤_ : ℕ → ℕ → Set where
  z≤n : {n : ℕ} → zero ≤ n
  s≤s : {m n : ℕ} → m ≤ n → suc m ≤ suc n

foo : (k l m : ℕ) → k ≡ l + m → ℕ
foo .(l + m) l m refl = zero

bar : (n : ℕ) → n ≤ n → ℕ
bar .zero z≤n = zero
bar .(suc m) (s≤s {m} p) = zero

baz : ∀ m n → m * n ≡ zero → m ≡ zero ⊎ n ≡ zero
baz zero     n      h = inj₁ refl
baz (suc m) zero    h = inj₂ refl
baz (suc x) (suc x₁) ()


text:
module Structure.Function.Domain where

import      Lvl
open import Functional
import      Structure.Function.Names as Names
open import Structure.Function
open import Lang.Instance
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid
open import Type

private variable ℓₒ ℓₒ₁ ℓₒ₂ ℓₗ ℓₗ₁ ℓₗ₂ : Lvl.Level

module _ {A : Type{ℓₒ₁}} ⦃ _ : Equiv{ℓₗ₁}(A) ⦄ {B : Type{ℓₒ₂}} ⦃ _ : Equiv{ℓₗ₂}(B) ⦄ (f : A → B) where
  record Injective : Stmt{ℓₒ₁ Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂} where
    constructor intro
    field proof : Names.Injective(f)
  injective = inst-fn Injective.proof

module _ {A : Type{ℓₒ₁}} {B : Type{ℓₒ₂}} ⦃ _ : Equiv{ℓₗ₂}(B) ⦄ (f : A → B) where
  record Surjective : Stmt{ℓₒ₁ Lvl.⊔ ℓₒ₂ Lvl.⊔ ℓₗ₂} where
    constructor intro
    field proof : Names.Surjective(f)
  surjective = inst-fn Surjective.proof

module _ {A : Type{ℓₒ₁}} ⦃ _ : Equiv{ℓₗ₁}(A) ⦄ {B : Type{ℓₒ₂}} ⦃ _ : Equiv{ℓₗ₂}(B) ⦄ (f : A → B) where
  record Bijective : Stmt{ℓₒ₁ Lvl.⊔ ℓₒ₂ Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂} where
    constructor intro
    field proof : Names.Bijective(f)
  bijective = inst-fn Bijective.proof

module _ {A : Type{ℓₒ₁}} {B : Type{ℓₒ₂}} ⦃ _ : Equiv{ℓₗ₂}(B) ⦄ (f : A → B) where
  module _ (f⁻¹ : B → A) where
    record Inverseᵣ : Stmt{ℓₒ₂ Lvl.⊔ ℓₗ₂} where
      constructor intro
      field proof : Names.Inverses(f)(f⁻¹)
    inverseᵣ = inst-fn Inverseᵣ.proof

  module _ ⦃ _ : Equiv{ℓₗ₁}(A) ⦄ where
    Invertibleᵣ = ∃(f⁻¹ ↦ Function(f⁻¹) ∧ Inverseᵣ(f⁻¹))

module _ {A : Type{ℓₒ₁}} ⦃ _ : Equiv{ℓₗ₁}(A) ⦄ {B : Type{ℓₒ₂}} (f : A → B) where
  module _ (f⁻¹ : B → A) where
    Inverseₗ : Stmt
    Inverseₗ = Inverseᵣ(f⁻¹)(f)
    module Inverseₗ(inverseₗ) = Inverseᵣ{f = f⁻¹}{f⁻¹ = f}(inverseₗ)
    inverseₗ : ⦃ inverseₗ : Inverseₗ ⦄ → Names.Inverses(f⁻¹)(f)
    inverseₗ = inst-fn Inverseₗ.proof

  module _ ⦃ _ : Equiv{ℓₗ₂}(B) ⦄ where
    Invertibleₗ = ∃(f⁻¹ ↦ Function(f⁻¹) ∧ Inverseₗ(f⁻¹))

module _ {A : Type{ℓₒ₁}} ⦃ _ : Equiv{ℓₗ₁}(A) ⦄ {B : Type{ℓₒ₂}} ⦃ _ : Equiv{ℓₗ₂}(B) ⦄ (f : A → B) where
  module _ (f⁻¹ : B → A) where
    Inverse = Inverseₗ(f)(f⁻¹) ∧ Inverseᵣ(f)(f⁻¹)
    inverse-left : ⦃ inverse : Inverse ⦄ → Names.Inverses(f⁻¹)(f)
    inverse-left = inst-fn(Inverseₗ.proof ∘ [∧]-elimₗ)
    inverse-right : ⦃ inverse : Inverse ⦄ → Names.Inverses(f)(f⁻¹)
    inverse-right = inst-fn(Inverseᵣ.proof ∘ [∧]-elimᵣ)

  Invertible = ∃(f⁻¹ ↦ Function(f⁻¹) ∧ Inverse(f⁻¹))

module _ {A : Type{ℓₒ₁}} ⦃ _ : Equiv{ℓₗ₁}(A) ⦄ {B : Type{ℓₒ₂}} ⦃ _ : Equiv{ℓₗ₂}(B) ⦄ (([↔]-intro ba ab) : A ↔ B) where
  record InversePair : Type{Lvl.of(A) Lvl.⊔ Lvl.of(B) Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂} where
    constructor intro
    l = ba
    r = ab
    field
      ⦃ left ⦄ : Inverseₗ(l)(r)
      ⦃ right ⦄ : Inverseᵣ(l)(r)

module _ {A : Type{ℓₒ₁}} {B : Type{ℓₒ₂}} ⦃ _ : Equiv{ℓₗ₂}(B) ⦄ (f : A → B) where
  record Constant : Stmt{ℓₒ₁ Lvl.⊔ ℓₗ₂} where
    constructor intro
    field proof : Names.Constant(f)
  constant = inst-fn Constant.proof

module _ {A : Type{ℓₒ}} ⦃ _ : Equiv{ℓₗ}(A) ⦄ (f : A → A) where
  module _ (x : A) where
    record Fixpoint : Stmt{ℓₗ} where
      constructor intro
      field proof : Names.Fixpoint f(x)
    fixpoint = inst-fn Fixpoint.proof

  record Involution : Stmt{ℓₒ Lvl.⊔ ℓₗ} where
    constructor intro
    field proof : Names.Involution(f)
  involution = inst-fn Involution.proof

  record Idempotent : Stmt{ℓₒ Lvl.⊔ ℓₗ} where
    constructor intro
    field proof : Names.Idempotent(f)
  idempotent = inst-fn Idempotent.proof


text:
module TYPE where
data Pair (a b : Set1) : Set1 where
  pair : a -> b -> Pair a b

data Unit : Set1 where
  unit : Unit

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Experiments.NatMinusTwo.Base where

open import Cubical.Core.Primitives
open import Cubical.Data.Nat
open import Cubical.Data.Empty

record ℕ₋₂ : Type₀ where
  constructor -2+_
  field
    n : ℕ

pattern neg2 = -2+ zero
pattern neg1 = -2+ (suc zero)
pattern ℕ→ℕ₋₂ n = -2+ (suc (suc n))
pattern -1+_ n = -2+ (suc n)

2+_ : ℕ₋₂ → ℕ
2+ (-2+ n) = n

pred₋₂ : ℕ₋₂ → ℕ₋₂
pred₋₂ neg2 = neg2
pred₋₂ neg1 = neg2
pred₋₂ (ℕ→ℕ₋₂ zero) = neg1
pred₋₂ (ℕ→ℕ₋₂ (suc n)) = (ℕ→ℕ₋₂ n)

suc₋₂ : ℕ₋₂ → ℕ₋₂
suc₋₂ (-2+ n) = -2+ (suc n)

-- Natural number and negative integer literals for ℕ₋₂

open import Cubical.Data.Nat.Literals public

instance
  fromNatℕ₋₂ : HasFromNat ℕ₋₂
  fromNatℕ₋₂ = record { Constraint = λ _ → Unit ; fromNat = ℕ→ℕ₋₂ }

instance
  fromNegℕ₋₂ : HasFromNeg ℕ₋₂
  fromNegℕ₋₂ = record { Constraint = λ { (suc (suc (suc _))) → ⊥ ; _ → Unit }
                       ; fromNeg = λ { zero → 0 ; (suc zero) → neg1 ; (suc (suc zero)) → neg2 } }

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{- Formal verification of authenticated append-only skiplists in Agda, version 1.0.

   Copyright (c) 2020 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Data.Unit.NonEta
open import Data.Empty
open import Data.Sum
open import Data.Product
open import Data.Product.Properties hiding (≡-dec)
open import Data.Nat renaming (_≟_ to _≟ℕ_; _≤?_ to _≤?ℕ_)
open import Data.Nat.Properties
open import Data.List renaming (map to List-map)
open import Data.List.Properties using (∷-injective; ≡-dec)
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All
open import Data.Bool hiding (_<_; _≤_) renaming (_≟_ to _≟Bool_)
open import Data.Maybe renaming (map to Maybe-map)

open import Function

open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Core
open import Relation.Nullary

-- This module defins a type to represent hashes, functions for encoding
-- them, and properties about them

module AAOSL.Abstract.Hash where

 open import AAOSL.Lemmas

 -- We define a ByteString as a list of bits
 ByteString : Set
 ByteString = List Bool

 -- TODO-1 : Hash -> Digest (to be consistent with the paper)?  Or just comment?

 Hash : Set
 Hash = Σ ByteString (λ bs → length bs ≡ 32)

 _≟Hash_ : (h₁ h₂ : Hash) → Dec (h₁ ≡ h₂)
 (l , pl) ≟Hash (m , pm) with ≡-dec _≟Bool_ l m
 ...| yes refl = yes (cong (_,_ l) (≡-irrelevant pl pm))
 ...| no  abs  = no (abs ∘ ,-injectiveˡ)

 encodeH : Hash → ByteString
 encodeH (bs , _) = bs

 encodeH-inj : ∀ i j → encodeH i ≡ encodeH j → i ≡ j
 encodeH-inj (i , pi) (j , pj) refl = cong (_,_ i) (≡-irrelevant pi pj)

 encodeH-len : ∀{h} → length (encodeH h) ≡ 32
 encodeH-len { bs , p } = p

 encodeH-len-lemma : ∀ i j → length (encodeH i) ≡ length (encodeH j)
 encodeH-len-lemma i j = trans (encodeH-len {i}) (sym (encodeH-len {j}))

 -- This means that we can make a helper function that combines
 -- the necessary injections into one big injection
 ++b-2-inj : (h₁ h₂ : Hash){l₁ l₂ : Hash}
           → encodeH h₁ ++ encodeH l₁
              ≡ encodeH h₂ ++ encodeH l₂
           → h₁ ≡ h₂ × l₁ ≡ l₂
 ++b-2-inj h₁ h₂ {l₁} {l₂} hip
   with ++-inj {m = encodeH h₁} {n = encodeH h₂} (encodeH-len-lemma h₁ h₂) hip
 ...| hh , ll = encodeH-inj h₁ h₂ hh , encodeH-inj l₁ l₂ ll

 Collision : {A B : Set}(f : A → B)(a₁ a₂ : A) → Set
 Collision f a₁ a₂ = a₁ ≢ a₂ × f a₁ ≡ f a₂

 module WithCryptoHash
   -- A Hash function maps a bytestring into a hash.
   (hash    : ByteString → Hash)
   (hash-cr : ∀{x y} → hash x ≡ hash y → Collision hash x y ⊎ x ≡ y) where

  HashBroke : Set
  HashBroke = Σ ( ByteString × ByteString ) (λ { (x₁ , x₂) → Collision hash x₁ x₂ })

  hash-concat : List Hash  → Hash
  hash-concat l = hash (concat (List-map encodeH l))

  -- hash-concat isinjective, modulo hash collisions
  hash-concat-inj : ∀{l₁ l₂} → hash-concat l₁ ≡ hash-concat l₂ → HashBroke ⊎ l₁ ≡ l₂
  hash-concat-inj {[]} {x ∷ xs} h with hash-cr h
  ...| inj₁ col = inj₁ (([] , encodeH x ++ foldr _++_ [] (List-map encodeH xs)) , col)
  ...| inj₂ abs = ⊥-elim (++-abs (encodeH x) (subst (1 ≤_) (sym (encodeH-len {x})) (s≤s z≤n)) abs)
  hash-concat-inj {x ∷ xs} {[]} h with hash-cr h
  ...| inj₁ col = inj₁ ((encodeH x ++ foldr _++_ [] (List-map encodeH xs) , []) , col)
  ...| inj₂ abs = ⊥-elim (++-abs (encodeH x) (subst (1 ≤_) (sym (encodeH-len {x})) (s≤s z≤n)) (sym abs))
  hash-concat-inj {[]}    {[]} h = inj₂ refl
  hash-concat-inj {x ∷ xs} {y ∷ ys} h with hash-cr h
  ...| inj₁ col = inj₁ ((encodeH x ++ foldr _++_ [] (List-map encodeH xs) , encodeH y ++ foldr _++_ [] (List-map encodeH ys)) , col)
  ...| inj₂ res  with ++-inj {m = encodeH x} {n = encodeH y} (encodeH-len-lemma x y) res
  ...| xy , xsys with hash-concat-inj {l₁ = xs} {l₂ = ys} (cong hash xsys)
  ...| inj₁ hb    = inj₁ hb
  ...| inj₂ final = inj₂ (cong₂ _∷_ (encodeH-inj x y xy) final)


text:
------------------------------------------------------------------------
-- Characters
------------------------------------------------------------------------

module Data.Char where

open import Data.Nat  using (ℕ)
open import Data.Bool using (Bool; true; false)
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)

------------------------------------------------------------------------
-- The type

postulate
  Char : Set

{-# BUILTIN CHAR Char #-}
{-# COMPILED_TYPE Char Char #-}

------------------------------------------------------------------------
-- Operations

private
 primitive
  primCharToNat    : Char → ℕ
  primCharEquality : Char → Char → Bool

toNat : Char → ℕ
toNat = primCharToNat

infix 4 _==_

_==_ : Char → Char → Bool
_==_ = primCharEquality

_≟_ : Decidable {Char} _≡_
s₁ ≟ s₂ with s₁ == s₂
... | true  = yes trustMe
  where postulate trustMe : _
... | false = no trustMe
  where postulate trustMe : _

setoid : Setoid
setoid = PropEq.setoid Char

decSetoid : DecSetoid
decSetoid = PropEq.decSetoid _≟_

max_issues_repo_name: larrytheliquid/Lemmachine


text:
------------------------------------------------------------------------
-- A virtual machine
------------------------------------------------------------------------

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

module Lambda.Simplified.Delay-monad.Virtual-machine where

open import Equality.Propositional
open import Prelude

open import Monad equality-with-J

open import Delay-monad
open import Delay-monad.Monad

open import Lambda.Simplified.Delay-monad.Interpreter
open import Lambda.Simplified.Syntax
open import Lambda.Simplified.Virtual-machine

open Closure Code

-- A functional semantics for the VM.

exec : ∀ {i} → State → Delay (Maybe Value) i
exec s with step s
... | continue s′ = later λ { .force → exec s′ }
... | done v      = return (just v)
... | crash       = return nothing

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
{-# OPTIONS --safe #-}
module Cubical.Data.Maybe.Base where

open import Cubical.Core.Everything

private
  variable
    ℓ ℓA ℓB : Level
    A : Type ℓA
    B : Type ℓB

data Maybe (A : Type ℓ) : Type ℓ where
  nothing : Maybe A
  just    : A → Maybe A

caseMaybe : (n j : B) → Maybe A → B
caseMaybe n _ nothing  = n
caseMaybe _ j (just _) = j

map-Maybe : (A → B) → Maybe A → Maybe B
map-Maybe _ nothing  = nothing
map-Maybe f (just x) = just (f x)

rec : B → (A → B) → Maybe A → B
rec n j nothing = n
rec n j (just a) = j a

elim : ∀ {A : Type ℓA} (B : Maybe A → Type ℓB) → B nothing → ((x : A) → B (just x)) → (mx : Maybe A) → B mx
elim B n j nothing = n
elim B n j (just a) = j a

max_issues_repo_name: thomas-lamiaux/cubical


text:
module Issue833-2 where

-- Arbitrary data type
record unit : Set where
  constructor tt

module Test ⦃ m : unit ⦄ { n : unit } where

open Test { tt }

max_stars_repo_name: larrytheliquid/agda


text:
{-# OPTIONS --without-K  #-}
module sets.fin.universe where

open import level
open import sum
open import decidable
open import equality.core
open import equality.calculus
open import equality.inspect
open import function.isomorphism
open import function.core
open import function.extensionality
open import function.fibration
open import function.overloading
open import sets.core
open import sets.properties
open import sets.nat.core
  hiding (_≟_)
open import sets.nat.ordering
  hiding (compare)
open import sets.fin.core
open import sets.fin.ordering
open import sets.fin.properties
open import sets.unit
open import sets.empty
open import sets.bool
open import sets.vec.dependent
open import hott.level.core
open import hott.level.closure
open import hott.level.sets

fin-struct-iso : ∀ {n} → Fin (suc n) ≅ (⊤ {lzero} ⊎ Fin n)
fin-struct-iso = record
  { to = λ { zero → inj₁ tt; (suc i) → inj₂ i }
  ; from = [ (λ _ → zero) ,⊎ (suc) ]
  ; iso₁ = λ { zero → refl ; (suc i) → refl }
  ; iso₂ = λ { (inj₁ _) → refl; (inj₂ i) → refl } }

fin0-empty : ⊥ ≅ Fin 0
fin0-empty = sym≅ (empty-⊥-iso (λ ()))

fin1-unit : ∀ {i} → ⊤ {i} ≅ Fin 1
fin1-unit = record
  { to = λ _ → zero
  ; from = λ { zero → tt ; (suc ()) }
  ; iso₁ = λ _ → refl
  ; iso₂ = λ { zero → refl ; (suc ()) } }

fin2-bool : Bool ≅ Fin 2
fin2-bool = record
  { to = λ b → if b then # 0 else # 1
  ; from = true ∷∷ false ∷∷ ⟦⟧
  ; iso₁ = λ { true → refl ; false → refl }
  ; iso₂ = refl ∷∷ refl ∷∷ ⟦⟧ }

fin-sum : ∀ {n m} → (Fin n ⊎ Fin m) ≅ Fin (n + m)
fin-sum {0} = record
  { to = λ { (inj₁ ()) ; (inj₂ j) → j }
  ; from = λ { j → inj₂ j }
  ; iso₁ = λ { (inj₁ ()); (inj₂ j) → refl }
  ; iso₂ = λ _ → refl }
fin-sum {suc n}{m} = begin
    (Fin (suc n) ⊎ Fin m)
  ≅⟨ ⊎-ap-iso fin-struct-iso refl≅ ⟩
    ((⊤ ⊎ Fin n) ⊎ Fin m)
  ≅⟨ ⊎-assoc-iso ⟩
    (⊤ ⊎ (Fin n ⊎ Fin m))
  ≅⟨ ⊎-ap-iso refl≅ fin-sum ⟩
    (⊤ ⊎ Fin (n + m))
  ≅⟨ sym≅ fin-struct-iso ⟩
    Fin (suc (n + m))
  ∎
  where open ≅-Reasoning

fin-prod : ∀ {n m} → (Fin n × Fin m) ≅ Fin (n * m)
fin-prod {0} = iso (λ { (() , _) }) (λ ()) (λ { (() , _) }) (λ ())
fin-prod {suc n}{m} = begin
    (Fin (suc n) × Fin m)
  ≅⟨ ×-ap-iso fin-struct-iso refl≅ ⟩
    ((⊤ ⊎ Fin n) × Fin m)
  ≅⟨ ⊎×-distr-iso ⟩
    ((⊤ × Fin m) ⊎ (Fin n × Fin m))
  ≅⟨ ⊎-ap-iso ×-left-unit fin-prod ⟩
    (Fin m ⊎ (Fin (n * m)))
  ≅⟨ fin-sum ⟩
    (Fin (m + (n * m)))
  ≡⟨ refl ⟩
    Fin (suc n * m)
  ∎
  where open ≅-Reasoning

fin-exp : ∀ {n m} → (Fin n → Fin m) ≅ Fin (m ^ n)
fin-exp {0} = record
  { to = λ f → zero
  ; from = (λ ()) ∷∷ ⟦⟧
  ; iso₁ = λ f → funext λ ()
  ; iso₂ = refl ∷∷ ⟦⟧ }
fin-exp {suc n}{m} = begin
    (Fin (suc n) → Fin m)
  ≅⟨ (Π-ap-iso fin-struct-iso λ _ → refl≅) ⟩
    ((⊤ ⊎ Fin n) → Fin m)
  ≅⟨ iso (λ f → f (inj₁ tt) , f ∘' inj₂)
         (λ { (i , _) (inj₁ _) → i
            ; (_ , g) (inj₂ i) → g i })
         (λ f → funext λ { (inj₁ tt) → refl
                          ; (inj₂ i) → refl })
         (λ { (i , g) → refl }) ⟩
    (Fin m × (Fin n → Fin m))
  ≅⟨ ×-ap-iso refl≅ fin-exp ⟩
    (Fin m × Fin (m ^ n))
  ≅⟨ fin-prod ⟩
    Fin (m ^ (suc n))
  ∎
  where open ≅-Reasoning

factorial : ℕ → ℕ
factorial 0 = 1
factorial (suc n) = suc n * factorial n

fin-inj-iso : ∀ {n} → (Fin n ≅ Fin n) ≅ (Fin n ↣ Fin n)
fin-inj-iso {n} = record
  { to = λ f → (apply f , iso⇒inj f)
  ; from = λ { (f , inj) → inj⇒iso f inj }
  ; iso₁ = λ f → iso-eq-h2 (fin-set n) (fin-set n) refl
  ; iso₂ = λ { (f , inj) → inj-eq-h2 (fin-set n) refl } }

fin-iso-iso : ∀ {n} → (Fin n ↣ Fin n) ≅ Fin (factorial n)
fin-iso-iso {0} = record
  { to = λ { (f , _) → zero }
  ; from = λ _ → (λ ()) , (λ { {()} p })
  ; iso₁ = λ { (f , _) → inj-eq-h2 (fin-set _) (funext λ ()) }
  ; iso₂ = λ { zero → refl ; (suc ()) } }
fin-iso-iso {suc n} = begin
    (X ↣ X)
  ≅⟨ sym≅ (total-iso classify) ⟩
    (Σ X λ i → classify ⁻¹ i)
  ≅⟨ (Σ-ap-iso₂ λ i → trans≅ (sym≅ (const-fibre i)) fibre-zero-iso) ⟩
    (Fin (suc n) × (Fin n ↣ Fin n))
  ≅⟨ ×-ap-iso refl≅ fin-iso-iso ⟩
    (Fin (suc n) × Fin (factorial n))
  ≅⟨ fin-prod ⟩
    Fin (factorial (suc n))
  ∎
  where
    X = Fin (suc n)
    open ≅-Reasoning

    classify : (X ↣ X) → X
    classify (f , _) = f zero

    const-fibre : (i : X) → classify ⁻¹ zero ≅ classify ⁻¹ i
    const-fibre i = begin
        ( Σ (X ↣ X) λ { (f , _) → f zero ≡ zero } )
      ≅⟨ ( Σ-ap-iso (transpose-inj-iso' zero i) (λ { (f , inj)
         → mk-prop-iso (fin-set _ _ _) (fin-set _ _ _)
                       (ap (transpose zero i)) (u f) }) ) ⟩
        ( Σ (X ↣ X) λ { (f , _) → f zero ≡ i } )
      ∎
      where
        u : (f : X → X)
          → transpose zero i (f zero) ≡ i
          → f zero ≡ zero
        u f p = sym (_≅_.iso₁ (transpose-iso zero i) (f zero))
              · (ap (transpose zero i) p
              · transpose-β₂ zero i)

    fibre-zero-iso : classify ⁻¹ zero ≅ (Fin n ↣ Fin n)
    fibre-zero-iso = record
      { to = λ { (f , z) → fin-inj-remove₀ f z }
      ; from = λ { g → fin-inj-add g , refl }
      ; iso₁ = λ { (f , p)
                 → unapΣ (inj-eq-h2 (fin-set (suc n))
                         (funext (α f p ))
                         , h1⇒prop (fin-set (suc n) _ _) _ _) }
      ; iso₂ = λ g → inj-eq-h2 (fin-set n) refl }
        where
            α : (f : Fin (suc n) ↣ Fin (suc n))
              → (p : apply f zero ≡ zero)
              → (i : Fin (suc n))
              → apply (fin-inj-add (fin-inj-remove₀ f p)) i
              ≡ apply f i
            α _ p zero = sym p
            α (f , f-inj) p (suc i) = pred-β (f (suc i))
              (λ q → fin-disj _ (f-inj (p · sym q)))

fin-subsets : ∀ {n} → (Fin n → Bool) ≅ Fin (2 ^ n)
fin-subsets = trans≅ (Π-ap-iso refl≅ λ _ → fin2-bool) fin-exp

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base